chore: bump toolchain to v4.29.0-rc1 (#344)

Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: Chris Henson <chrishenson.net@gmail.com>
Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com>
Co-authored-by: leanprover-community-mathlib4-bot <129911861+leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: Ching-Tsun Chou <chingtsun.chou@gmail.com>
Co-authored-by: Chris Henson <46805207+chenson2018@users.noreply.github.com>
Co-authored-by: Alexandre Rademaker <arademaker@gmail.com>
Co-authored-by: mathlib-nightly-testing[bot] <mathlib-nightly-testing[bot]@users.noreply.github.com>
Co-authored-by: mathlib-nightly-testing[bot] <258991302+mathlib-nightly-testing[bot]@users.noreply.github.com>
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>

Author: 9 people

Cslib/Computability/Automata/DA/Buchi.lean

@@ -29,6 +29,6 @@ of the language accepted by the same automaton.
 theorem buchi_eq_finAcc_omegaLim {da : DA State Symbol} {acc : Set State} :
     language (Buchi.mk da acc) = (language (FinAcc.mk da acc))↗ω := by
   ext xs
-  simp
+  simp +instances
 
 end Cslib.Automata.DA

Cslib/Computability/Automata/NA/BuchiInter.lean

@@ -93,6 +93,8 @@ lemma inter_freq_comp_acc_freq_acc {xs : ωSequence Symbol} {ss : ωSequence ((
   apply leadsTo_cases_or (q := {⟨_, b⟩ | b = false}) <;>
   grind [until_frequently_leadsTo_and, univ_inter]
 
+-- TODO: fix proof to work with backward.isDefEq.respectTransparency
+set_option backward.isDefEq.respectTransparency false in
 /-- The language accepted by the intersection automaton is the intersection of
 the languages accepted by the two component automata. -/
 @[simp, scoped grind =]

Cslib/Computability/Automata/NA/Loop.lean

@@ -92,6 +92,7 @@ theorem loop_run_one_iter {xs : ωSequence Symbol} {ss : ωSequence (Unit ⊕ St
     exact neq.imp (congrArg List.length)
   · grind [loop_run_from_left]
 
+open List in
 /-- For any finite word in `language na`, there is a corresponding finite run of `na.loop`. -/
 theorem loop_fin_run_exists {xl : List Symbol} (h : xl ∈ language na) :
     ∃ sl : List (Unit ⊕ State), ∃ _ : sl.length = xl.length + 1,
@@ -103,7 +104,11 @@ theorem loop_fin_run_exists {xl : List Symbol} (h : xl ∈ language na) :
   · use [inl ()]
     grind
   · use [inl ()] ++ (sl.extract 1 xl.length).map inr ++ [inl ()]
-    grind [FinAcc.loop, → LTS.tr_setImage]
+    #adaptation_note
+    /-- This squeeze was required moving to nightly-2026-01-28 -/
+    grind only [= length_append, = length_cons, = length_nil, = length_map, = List.length_take,
+      = length_drop, = min_def, = getElem_append, = getElem_cons, = List.take_zero, FinAcc.loop,
+      = map_nil, = getElem_map, = getElem_take, = getElem_drop]
 
 /-- For any finite word in `language na`, there is a corresponding multistep transition
 of `na.loop`. -/

Cslib/Computability/Automata/NA/Pair.lean

@@ -35,7 +35,7 @@ theorem LTS.pairLang_regular [Finite State] {lts : LTS State Symbol} {s t : Stat
   rw [IsRegular.iff_nfa]
   use State, inferInstance, (NA.FinAcc.mk ⟨lts, {s}⟩ {t})
   ext
-  simp
+  simp +instances
 
 /-- `LTS.pairViaLang via s t` is the language of finite words that can take the LTS
 from state `s` to state `t` via a state in `via`. -/
@@ -108,8 +108,7 @@ theorem language_eq_fin_iSup_hmul_omegaPow
     [Inhabited Symbol] [Finite State] (na : Buchi State Symbol) :
     language na = ⨆ s ∈ na.start, ⨆ t ∈ na.accept, (na.pairLang s t) * (na.pairLang t t)^ω := by
   ext xs
-  simp only [Buchi.instωAcceptor, ωAcceptor.mem_language,
-    ωLanguage.mem_iSup, ωLanguage.mem_hmul, LTS.mem_pairLang]
+  simp only [ωAcceptor.mem_language, ωLanguage.mem_iSup, ωLanguage.mem_hmul, LTS.mem_pairLang]
   constructor
   · rintro ⟨ss, h_run, h_inf⟩
     obtain ⟨t, h_acc, h_t⟩ := frequently_in_finite_type.mp h_inf

Cslib/Computability/Automata/NA/Sum.lean

@@ -58,6 +58,8 @@ namespace Buchi
 
 open ωAcceptor
 
+-- TODO: fix proof to work with backward.isDefEq.respectTransparency
+set_option backward.isDefEq.respectTransparency false in
 /-- The ω-language accepted by the Buchi sum automata is the union of the ω-languages accepted
 by its component automata. -/
 @[simp]

Cslib/Computability/Automata/NA/Total.lean

@@ -54,7 +54,7 @@ as long as the accepting states are also lifted in the obvious way. -/
 theorem totalize_language_eq {na : FinAcc State Symbol} :
     language (FinAcc.mk na.totalize (inl '' na.accept)) = language na := by
   ext xl
-  simp [totalize]
+  simp +instances [totalize]
 
 end FinAcc
 

Cslib/Computability/Languages/Language.lean

@@ -54,10 +54,9 @@ theorem reverse_sub (l m : Language α) : (l - m).reverse = l.reverse - m.revers
 theorem sub_one_mul : (l - 1) * l = l * l - 1 := by
   ext x; constructor
   · rintro ⟨u, h_u, v, h_v, rfl⟩
-    rw [mem_sub, mem_one] at h_u ⊢
     constructor
     · refine ⟨u, ?_, v, ?_⟩ <;> grind
-    · grind [append_eq_nil_iff]
+    · grind [append_eq_nil_iff, mem_one]
   · rintro ⟨⟨u, h_u, v, h_v, rfl⟩, h_x⟩
     rcases eq_or_ne u [] with (rfl | h_u')
     · refine ⟨v, ?_, [], ?_⟩ <;> grind [mem_sub, mem_one]

Cslib/Computability/Languages/OmegaRegularLanguage.lean

@@ -85,7 +85,7 @@ theorem IsRegular.bot : (⊥ : ωLanguage Symbol).IsRegular := by
     accept := ∅ }
   use Unit, inferInstance, na
   ext xs
-  simp [na]
+  simp +instances [na]
 
 /-- The language of all ω-sequences is ω-regular. -/
 @[simp]
@@ -96,11 +96,13 @@ theorem IsRegular.top : (⊤ : ωLanguage Symbol).IsRegular := by
     accept := univ }
   use Unit, inferInstance, na
   ext xs
-  simp only [na, NA.Buchi.instωAcceptor, mem_language, mem_univ, frequently_true_iff_neBot,
-    atTop_neBot, and_true, mem_top, iff_true]
+  simp +instances only [na, NA.Buchi.instωAcceptor, mem_language, mem_univ,
+    frequently_true_iff_neBot, atTop_neBot, and_true, mem_top, iff_true]
   use const ()
   grind [NA.Run]
 
+-- TODO: fix proof to work with backward.isDefEq.respectTransparency
+set_option backward.isDefEq.respectTransparency false in
 /-- The union of two ω-regular languages is ω-regular. -/
 @[simp]
 theorem IsRegular.sup {p1 p2 : ωLanguage Symbol}
@@ -120,6 +122,8 @@ theorem IsRegular.sup {p1 p2 : ωLanguage Symbol}
   rw [mem_iUnion, Fin.exists_fin_two]
   grind
 
+-- TODO: fix proof to work with backward.isDefEq.respectTransparency
+set_option backward.isDefEq.respectTransparency false in
 open NA.Buchi in
 /-- The intersection of two ω-regular languages is ω-regular. -/
 @[simp]
@@ -185,6 +189,8 @@ theorem IsRegular.omegaPow [Inhabited Symbol] {l : Language Symbol}
   use Unit ⊕ State, inferInstance, ⟨na.loop, {inl ()}⟩
   exact NA.Buchi.loop_language_eq
 
+-- TODO: fix proof to work with backward.isDefEq.respectTransparency
+set_option backward.isDefEq.respectTransparency false in
 /-- An ω-language is regular iff it is the finite union of ω-languages of the form `L * M^ω`,
 where all `L`s and `M`s are regular languages. -/
 theorem IsRegular.eq_fin_iSup_hmul_omegaPow [Inhabited Symbol] (p : ωLanguage Symbol) :

Cslib/Computability/Languages/RegularLanguage.lean

@@ -149,6 +149,8 @@ theorem IsRegular.mul [Inhabited Symbol] {l1 l2 : Language Symbol}
     ⟨finConcat nfa1 nfa2, inr '' (inl '' nfa2.accept)⟩
   exact finConcat_language_eq
 
+-- TODO: fix proof to work with backward.isDefEq.respectTransparency
+set_option backward.isDefEq.respectTransparency false in
 open NA.FinAcc Sum in
 /-- The Kleene star of a regular language is regular. -/
 @[simp]

Cslib/Foundations/Lint/Basic.lean

@@ -7,7 +7,7 @@ Authors: Chris Henson
 module
 
 public import Batteries.Tactic.Lint.Basic
-public meta import Lean.Meta.GlobalInstances
+public meta import Lean.Meta.Instances
 
 namespace Cslib.Lint
 
@@ -21,7 +21,7 @@ public meta def topNamespace : Batteries.Tactic.Lint.Linter where
   test declName := do
     if ← isAutoDecl declName then return none
     let env ← getEnv
-    if isGlobalInstance env declName then return none
+    if ← isInstanceReducible declName then return none
     let nss := env.getNamespaceSet
     let top := nss.fold (init := (∅ : NameSet)) fun tot n =>
       match n.components with