Language eq fin i Sup hmul omega Pow

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  apply mem_ext  intro xs  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    use ss 0, by grind only [NA.Run], t, h_acc    obtain ⟨f, h_mono, h_f⟩ := frequently_iff_strictMono.mp h_t    refine ⟨xs.take (f 0), ?_, xs.drop (f 0), ?_, by grind⟩    · have : na.MTr (ss 0) (xs.extract 0 (f 0)) (ss (f 0)) := by        grind only [LTS.OmegaExecution.extract_mTr, NA.Run]      grind [extract_eq_drop_take]    · simp only [omegaPow_seq_prop, LTS.mem_pairLang]      use (f · - f 0)      split_ands      · grind [Nat.base_zero_strictMono]      · simp      · intro n        have mono_f (k : ℕ) : f 0 ≤ f (n + k) := h_mono.monotone (by grind)        grind [extract_drop, mono_f 0,          LTS.OmegaExecution.extract_mTr h_run.trans <| h_mono.monotone (?_ : n ≤ n + 1)]  · rintro ⟨s, _, t, _, yl, h_yl, zs, h_zs, rfl⟩    obtain ⟨zls, rfl, h_zls⟩ := mem_omegaPow.mp h_zs    let ts := ωSequence.const t    have h_mtr (n : ℕ) : na.MTr (ts n) (zls n) (ts (n + 1)) := by      grind [Language.mem_sub_one, LTS.mem_pairLang]    have h_pos (n : ℕ) : (zls n).length > 0 := by      grind only [Language.mem_sub_one, List.eq_nil_iff_length_eq_zero]    obtain ⟨zss, h_zss, _⟩ := LTS.OmegaExecution.flatten_mTr h_mtr h_pos    have (n : ℕ) : zss (zls.cumLen n) = t := by grind    obtain ⟨xss, _, _, _, _⟩ := LTS.OmegaExecution.append h_yl h_zss      (by grind [cumLen_zero (ls := zls)])    use xss, by grind [NA.Run]    apply (drop_frequently_iff_frequently yl.length).mp    apply frequently_iff_strictMono.mpr    use zls.cumLen    grind [cumLen_strictMono]