chore: bump toolchain to v4.30.0-rc1 (#469)

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: Kim Morrison <kim@tqft.net>
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: Chris Henson <46805207+chenson2018@users.noreply.github.com>
Co-authored-by: Kim Morrison <477956+kim-em@users.noreply.github.com>
Co-authored-by: Ching-Tsun Chou <chingtsun.chou@gmail.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>

Author: 9 people

Cslib/Computability/Automata/DA/Congr.lean

@@ -58,7 +58,11 @@ the equivalence class corresponding to `s`. -/
 @[simp]
 theorem congr_language_eq {a : Quotient c.eq} : language (FinAcc.mk c.toDA {a}) = eqvCls a := by
   ext
-  grind
+  #adaptation_note
+  /-- A grind regression found moving to nightly-2026-03-31 (changes from lean#13166) -/
+  constructor <;>
+  · intro h
+    simpa [mem_language, Accepts, congr_mtr_eq] using h
 
 end FinAcc
 

Cslib/Computability/Automata/DA/ToNA.lean

@@ -54,11 +54,13 @@ open scoped FLTS NA.FinAcc in
 theorem toNAFinAcc_language_eq {a : DA.FinAcc State Symbol} :
     language a.toNAFinAcc = language a := by
   ext xs
+  #adaptation_note
+  /-- A grind regression found moving to nightly-2026-03-31 (changes from lean#13166) -/
   constructor
-  · grind
+  · simp_all [mem_language a xs, Accepts, toNAFinAcc, toNA, FLTS.toLTS_mtr]
   · intro _
     use a.start
-    grind
+    simp_all [Accepts, toNAFinAcc, toNA, FLTS.toLTS_mtr]
 
 end FinAcc
 
@@ -70,16 +72,19 @@ def toNABuchi (a : DA.Buchi State Symbol) : NA.Buchi State Symbol :=
   { a.toNA with accept := a.accept }
 
 open ωAcceptor in
-open scoped NA.Buchi in
 /-- The `NA.Buchi` constructed from a `DA.Buchi` has the same ω-language. -/
 @[simp, scoped grind _=_]
 theorem toNABuchi_language_eq {a : DA.Buchi State Symbol} :
     language a.toNABuchi = language a := by
   ext xs; constructor
-  · grind
-  · intro _
+  #adaptation_note
+  /-- A grind regression found moving to nightly-2026-03-31 (changes from lean#13166) -/
+  · simp_all [Accepts, language, toNABuchi]
+  · intro h
     use (a.run xs)
-    grind
+    split_ands
+    · grind
+    · exact Filter.frequently_map.mp h
 
 end Buchi
 

Cslib/Computability/Automata/EpsilonNA/ToNA.lean

@@ -52,7 +52,9 @@ theorem toNAFinAcc_language_eq {ena : εNA.FinAcc State Symbol} :
   ext xs
   have : ∀ s s', ena.saturate.MTr s (xs.map some) s' = ena.saturate.noε.MTr s xs s' := by
     simp [LTS.noε_saturate_mTr]
-  grind
+  #adaptation_note
+  /-- A grind regression found moving to nightly-2026-03-31 (changes from lean#13166) -/
+  grind [Accepts]
 
 end Automata.εNA.FinAcc
 

Cslib/Computability/Automata/NA/BuchiEquiv.lean

@@ -60,7 +60,10 @@ theorem reindex_language_eq {f : State ≃ State'} {nba : Buchi State Symbol} :
   ext xs
   constructor
   · rintro ⟨ss', h_run', h_acc'⟩
-    grind [reindex_run_iff]
+    #adaptation_note
+    /-- A grind regression found moving to nightly-2026-03-31 (changes from lean#13166) -/
+    simp only [mem_language, Accepts]
+    exact frequently_principal.mp (· (reindex_run_iff.mp h_run') h_acc')
   · rintro ⟨ss, h_run, h_acc⟩
     use ss.map f
     constructor <;> grind [reindex_run_iff']

Cslib/Computability/Automata/NA/Concat.lean

@@ -159,22 +159,31 @@ theorem finConcat_language_eq [Inhabited Symbol] :
     obtain ⟨xs, ss, h_ωtr, rfl, rfl⟩ := LTS.Total.extend_omegaExecution h_mtr
     have hc : (finConcat na1 na2).Run (xl ++ω xs) ss := by grind [Run]
     have hr : (ss xl.length).isRight := by grind
-    obtain ⟨n, _⟩ := concat_run_proj hc hr
+    obtain ⟨n, _, _, ss2, h_run2, _⟩ := concat_run_proj hc hr
     refine ⟨xl.take n, ?_, xl.drop n, ?_, ?_⟩
     · grind [totalize_language_eq, take_append_of_le_length]
     · have : ss xl.length = (ss.drop n) (xl.length - n) := by grind
-      grind [drop_append_of_le_length, take_append_of_le_length, totalize_run_mtr]
+      #adaptation_note
+      /-- A grind regression found moving to nightly-2026-03-31 (changes from lean#13166) -/
+      have : ss xl.length = inr (ss2 (xl.length - n)) := by grind
+      have hl : (ss2 (xl.length - n)).isLeft := by grind
+      obtain ⟨s2, t2, h_mtr2, _, _, _⟩ := totalize_run_mtr h_run2 hl
+      refine ⟨s2, ?_, t2, ?_, ?_⟩ <;> grind [drop_append_of_le_length, take_append_of_le_length]
     · exact xl.take_append_drop n
   · rintro ⟨xl1, h_xl1, xl2, h_xl2, rfl⟩
     rw [← totalize_language_eq] at h_xl1
     obtain ⟨_, h_s2, _, _, h_mtr2⟩ := h_xl2
-    obtain ⟨_, _, h_run2, _, _⟩ := totalize_mtr_run h_s2 h_mtr2
+    obtain ⟨_, ss2, h_run2, _, _⟩ := totalize_mtr_run h_s2 h_mtr2
     obtain ⟨ss, ⟨_, h_ωtr⟩, _⟩ := concat_run_exists h_xl1 h_run2
-    grind [
-      finConcat, List.length_append, take_append_of_le_length,
-      extract_eq_drop_take, =_ append_append_ωSequence, get_drop xl2.length xl1.length ss,
-      LTS.OmegaExecution.extract_mTr h_ωtr (zero_le (xl1.length + xl2.length))
-    ]
+    #adaptation_note
+    /-- A grind regression found moving to nightly-2026-03-31 (changes from lean#13166) -/
+    have h_mtr := LTS.OmegaExecution.extract_mTr h_ωtr (zero_le (xl1.length + xl2.length))
+    simp [← append_append_ωSequence, extract_eq_drop_take,
+      take_append_of_le_length, ← List.length_append] at h_mtr
+    have : ss (xl1.length + xl2.length) = (ss.drop xl1.length) xl2.length := by grind
+    have : ss (xl1.length + xl2.length) = inr (ss2 xl2.length) := by grind
+    refine ⟨ss 0, ?_, ss (xl1.length + xl2.length), ?_, ?_⟩ <;>
+      grind [finConcat, List.length_append]
 
 end FinAcc
 

Cslib/Computability/Automata/NA/Loop.lean

@@ -145,8 +145,10 @@ theorem loop_language_eq [Inhabited Symbol] :
     rintro xs ⟨ss, h_run, h_acc⟩
     obtain ⟨k, h1, h2⟩ : ∃ k > 0, (ss k).isLeft :=
       by grind [FinAcc.loop, frequently_atTop'.mp h_acc 0]
-    obtain ⟨n, _⟩ := loop_run_one_iter h_run h1 h2
-    refine ⟨xs.take n, by grind, xs.drop n, ?_, by simp⟩
+    #adaptation_note
+    /-- A grind regression found moving to nightly-2026-03-31 (changes from lean#13166) -/
+    obtain ⟨n, _, h, _⟩ := loop_run_one_iter h_run h1 h2
+    refine ⟨xs.take n, h, xs.drop n, ?_, by simp⟩
     refine ⟨ss.drop n, by grind, ?_⟩
     apply (drop_frequently_iff_frequently n).mpr
     grind
@@ -191,10 +193,13 @@ theorem loop_language_eq [Inhabited Symbol] (h : ¬ language na = 0) :
       obtain ⟨h1, h2⟩ : 0 < xl.length ∧ (ss xl.length).isLeft := by
         simp only [mem_singleton_iff] at h_acc
         grind
-      obtain ⟨n, h_n, _, _, h_ωtr'⟩ := loop_run_one_iter h_run h1 h2
+      obtain ⟨n, h_n, h_take, h_drop, h_ωtr'⟩ := loop_run_one_iter h_run h1 h2
       left; refine ⟨xl.take n, ?_, xl.drop n, ?_, ?_⟩
-      · grind [totalize_language_eq, take_append_of_le_length]
-      · refine ⟨ss n, by grind, ss xl.length, by grind, ?_⟩
+      · #adaptation_note
+        /-- A grind regression found moving to nightly-2026-03-31 (changes from lean#13166) -/
+        change List.take n xl ∈ language na - 1 -- canonicalize membership instance
+        grind [totalize_language_eq, take_append_of_le_length]
+      · refine ⟨ss n, by aesop, ss xl.length, by grind, ?_⟩
         have := LTS.OmegaExecution.extract_mTr h_ωtr' (show 0 ≤ xl.length - n by grind)
         have : n + (xl.length - n) = xl.length := by grind
         have : ((xl ++ω xs).drop n).extract 0 (xl.length - n) = xl.drop n := by

Cslib/Computability/Automata/NA/Sum.lean

@@ -71,7 +71,9 @@ theorem iSum_language_eq {na : (i : I) → NA (State i) Symbol} {acc : (i : I) 
   constructor
   · rintro ⟨ss, h_run, h_acc⟩
     simp only [mem_iUnion] at h_acc
-    grind
+    #adaptation_note
+    /-- A grind regression found moving to nightly-2026-03-31 (changes from lean#13166) -/
+    grind [Accepts]
   · rintro ⟨i, ss_i, _⟩
     use ss_i.map (Sigma.mk i)
     simp only [mem_iUnion]

Cslib/Computability/Automata/NA/ToDA.lean

@@ -42,7 +42,9 @@ open scoped DA.FinAcc LTS in
 theorem toDAFinAcc_language_eq {na : NA.FinAcc State Symbol} :
   language na.toDAFinAcc = language na := by
   ext xs
-  grind
+  #adaptation_note
+  /-- A grind regression found moving to nightly-2026-03-31 (changes from lean#13166) -/
+  grind [Accepts]
 
 end FinAcc
 

Cslib/Computability/Languages/Congruences/BuchiCongruence.lean

@@ -84,6 +84,10 @@ lemma buchiCongruence_transfer
       ( xl ∈ na.pairViaLang na.accept s t → ∃ r ∈ na.accept, r ∈ sl ) := by
   have h_eq : na.BuchiCongruence.eq xl yl := by
     apply Quotient.exact
+    #adaptation_note
+    /-- A grind regression found moving to nightly-2026-03-31 (changes from lean#13166) -/
+    have : ⟦xl⟧ = a := mem_singleton_iff.mp <| mem_preimage.mp hc
+    have : ⟦yl⟧ = a := mem_singleton_iff.mp <| mem_preimage.mp hc'
     grind
   have := h_eq s t
   have h_yl : yl ∈ na.pairLang s t := by grind
@@ -121,14 +125,26 @@ theorem buchiFamily_cover [Inhabited Symbol] [Finite State] :
   use ⟦ xs.take (f 0) ⟧, b
   apply mem_buchiFamily.mpr
   use xs.take (f 0), xs.drop (f 0) |>.toSegs (f · - f 0)
+  #adaptation_note
+  /-- A grind regression found moving to nightly-2026-03-31 (changes from lean#13166) -/
   split_ands
-  · grind
+  · rfl
   · intro k
     specialize h_color {f k, f (k + 1)}
     have := @h_mono 0 k
     have := @h_mono k (k + 1)
-    grind [extract_drop, Finset.insert_nonempty, Finset.singleton_nonempty, min'_insert,
-      min'_singleton, max'_insert, max'_singleton, toSegs_def, Language.mem_sub_one]
+    simp only [Language.mem_sub_one, toSegs_def]
+    split_ands
+    · have : b = color {f k, f (k + 1)} := by grind
+      simp_all only [extract_drop, color]
+      split_ifs with h
+      · have : f k ≤ f (k + 1) := by lia
+        have : f 0 + (f k - f 0) = f k := by lia
+        have : f 0 + (f (k + 1) - f 0) = f (k + 1) := by lia
+        simp_all
+        rfl
+      · simp at h
+    · grind
   · grind [Nat.base_zero_strictMono h_mono]
 
 -- This intermediate result is split out of the proof of `buchiCongruence_saturation` below

Cslib/Computability/Languages/Language.lean

@@ -30,14 +30,13 @@ theorem mem_biInf {I : Type*} (s : Set I) (l : I → Language α) (x : List α)
     (x ∈ ⨅ i ∈ s, l i) ↔ ∀ i ∈ s, x ∈ l i :=
   mem_iInter₂
 
+#adaptation_note
+/-- A grind regression found moving to nightly-2026-03-31 (changes from lean#13166) -/
 @[simp]
 theorem mem_biSup {I : Type*} (s : Set I) (l : I → Language α) (x : List α) :
-    (x ∈ ⨆ i ∈ s, l i) ↔ ∃ i ∈ s, x ∈ l i := by
-  constructor <;> intro h
-  · have := mem_iUnion₂.mp h
-    grind
-  · apply mem_iUnion₂.mpr
-    grind
+    (x ∈ ⨆ i ∈ s, l i) ↔ ∃ i ∈ s, x ∈ l i where
+  mp h := bex_def.mp (mem_iUnion₂.mp h)
+  mpr h :=  mem_iUnion₂.mpr (bex_def.mpr h)
 
 theorem le_one_iff_eq : l ≤ 1 ↔ l = 0 ∨ l = 1 :=
   subset_singleton_iff_eq
@@ -50,17 +49,23 @@ theorem mem_sub_one (x : List α) : x ∈ (l - 1) ↔ x ∈ l ∧ x ≠ [] :=
 theorem reverse_sub (l m : Language α) : (l - m).reverse = l.reverse - m.reverse := by
   ext x; simp [mem_sub]
 
+#adaptation_note
+/-- A grind regression found moving to nightly-2026-03-31 (changes from lean#13166) -/
 @[scoped grind =]
 theorem sub_one_mul : (l - 1) * l = l * l - 1 := by
   ext x; constructor
   · rintro ⟨u, h_u, v, h_v, rfl⟩
     constructor
-    · refine ⟨u, ?_, v, ?_⟩ <;> grind
-    · grind [append_eq_nil_iff, mem_one]
+    · exact ⟨u, Set.mem_of_mem_inter_left h_u, v, h_v, rfl⟩
+    · by_contra h
+      have := mem_sub_one u |>.mp h_u
+      have := mem_one (u ++ v) |>.mp h
+      grind [append_eq_nil_iff]
   · 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]
-    · refine ⟨u, ?_, v, ?_⟩ <;> grind
+    · use v, (mem_sub l 1 v |>.mpr) ⟨h_v, Not.intro h_x⟩, []
+      grind [mem_sub, mem_one]
+    · use u, (mem_sub_one u).mpr ⟨h_u, h_u'⟩, v
 
 @[scoped grind =]
 theorem mul_sub_one : l * (l - 1) = l * l - 1 := by
@@ -70,15 +75,17 @@ theorem mul_sub_one : l * (l - 1) = l * l - 1 := by
     _ = (l.reverse * l.reverse - 1).reverse := by rw [sub_one_mul]
     _ = _ := by rw [reverse_sub, reverse_one, reverse_mul, reverse_reverse]
 
+#adaptation_note
+/-- A grind regression found moving to nightly-2026-03-31 (changes from lean#13166) -/
 @[scoped grind =]
 theorem kstar_sub_one : l∗ - 1 = (l - 1) * l∗ := by
   ext x; constructor
   · rintro ⟨h1, h2⟩
     obtain ⟨xl, rfl, h_xl⟩ := kstar_def_nonempty l ▸ h1
     have h3 : ¬ xl = [] := by grind [one_def]
     obtain ⟨x, xl', h_xl'⟩ := exists_cons_of_ne_nil h3
-    have := h_xl x
-    refine ⟨x, ?_, xl'.flatten, ?_, ?_⟩ <;> grind [join_mem_kstar]
+    subst h_xl'
+    refine ⟨x, mem_preimage.mp (h_xl x ?_), xl'.flatten, join_mem_kstar ?_, ?_⟩ <;> grind
   · rintro ⟨y, ⟨h_y, h_1⟩, z, h_z, rfl⟩
     refine ⟨?_, ?_⟩
     · apply (show l * l∗ ≤ l∗ by exact mul_kstar_le_kstar)