Is Regular eq fin i Sup hmul omega Pow

theorem IsRegular.eq_fin_iSup_hmul_omegaPow [Inhabited Symbol] (p : ωLanguage Symbol) :    p.IsRegular ↔ ∃ n : ℕ, ∃ l m : Fin n → Language Symbol,      (∀ i, (l i).IsRegular ∧ (m i).IsRegular) ∧ p = ⨆ i, (l i) * (m i)^ω := by  constructor  · rintro ⟨State, _, na, rfl⟩    rw [NA.Buchi.language_eq_fin_iSup_hmul_omegaPow na]    have eq_start := Finite.equivFin ↑na.start    have eq_accept := Finite.equivFin ↑na.accept    have eq_prod := eq_start.prodCongr eq_accept    have eq := (eq_prod.trans finProdFinEquiv).symm    refine ⟨Nat.card ↑na.start * Nat.card ↑na.accept,      fun i ↦ na.pairLang (eq i).1 (eq i).2,      fun i ↦ na.pairLang (eq i).2 (eq i).2,      by grind [LTS.pairLang_regular], ?_⟩    apply mem_ext    intro xs    simp only [mem_iSup]    refine ⟨?_, by grind⟩    rintro ⟨s, h_s, t, h_t, h_mem⟩    use eq.invFun (⟨s, h_s⟩, ⟨t, h_t⟩)    have := Equiv.apply_symm_apply eq    simp_all  · rintro ⟨n, l, m, _, rfl⟩    rw [← iSup_univ]    apply IsRegular.iSup    grind [IsRegular.hmul, IsRegular.omegaPow]