Fix grind failures in Automata/NA/Concat.lean

Author: ctchou

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