Loop language eq

theorem loop_language_eq [Inhabited Symbol] (h : ¬ language na = 0) :    language (FinAcc.mk na.finLoop {inl ()}) = (language na)∗ := by  rw [Language.kstar_iff_mul_add]  ext xl; constructor  · rintro ⟨s, _, t, h_acc, h_mtr⟩    by_cases h_xl : xl = []    · grind [mem_add, mem_one]    · have : Nonempty na.start := by        obtain ⟨_, s0, _, _⟩ := nonempty_iff_ne_empty.mpr h        use s0      obtain ⟨xs, ss, h_ωtr, rfl, rfl⟩ := LTS.Total.extend_omegaExecution h_mtr      have h_run : na.finLoop.Run (xl ++ω xs) ss := by grind [Run]      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_take, h_drop, h_ωtr'⟩ := loop_run_one_iter h_run h1 h2      left; refine ⟨xl.take n, ?_, xl.drop n, ?_, ?_⟩      · #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          grind [extract_eq_take, drop_append_of_le_length, take_append_of_le_length]        grind [finLoop]      · exact xl.take_append_drop n  · rintro (h | h)    · obtain ⟨xl1, ⟨h_xl1, _⟩, xl2, h_xl2, rfl⟩ := h      rw [← totalize_language_eq] at h_xl1      have := loop_fin_run_mtr h_xl1      obtain ⟨s1, _, s2, _, _⟩ := h_xl2      obtain ⟨rfl⟩ : s1 = inl () := by grind [finLoop, loop]      obtain ⟨rfl⟩ : s2 = inl () := by grind [finLoop, loop]      refine ⟨inl (), ?_, inl (), ?_, LTS.MTr.comp _ this ?_⟩ <;> assumption    · obtain ⟨rfl⟩ := (Language.mem_one xl).mp h      refine ⟨inl (), ?_, inl (), ?_, ?_⟩ <;> grind [finLoop, loop]