Omega reg lang iff finite union form

theorem omega_reg_lang_iff_finite_union_form [Inhabited A] {L : Set (Stream' A)} :    OmegaRegLang L ↔    ∃ n : ℕ, ∃ U V : Fin n → Set (List A),      (∀ i, RegLang (U i) ∧ RegLang (V i)) ∧ L = ⋃ i, (U i) * (V i)^ω := by  constructor  · rintro ⟨M, acc, h_fin, rfl⟩    rw [Automata.omega_reg_lang_finite_union_form]    have eq_init : Fin (Nat.card ↑M.init) ≃ ↑M.init := by exact (Finite.equivFin ↑Automata.NA.init).symm    have eq_acc : Fin (Nat.card ↑acc) ≃ ↑acc := by exact (Finite.equivFin ↑acc).symm    have eq_prod := Equiv.prodCongr eq_init eq_acc    have eq_fin_prod := (finProdFinEquiv (m := Nat.card ↑M.init) (n := Nat.card ↑acc)).symm    have eq := Equiv.trans eq_fin_prod eq_prod    use (Nat.card ↑M.init * Nat.card ↑acc)    use (fun i ↦ M.PairLang (eq i).1 (eq i).2)    use (fun i ↦ M.PairLang (eq i).2 (eq i).2)    constructor    · intro i ; constructor <;> exact Automata.pair_lang_regular    · ext as ; simp ; constructor      · rintro ⟨s0, h_s0, sa, h_sa, h_mem⟩        use (eq.invFun (⟨s0, h_s0⟩, ⟨sa, h_sa⟩))        simp [h_mem]      · rintro ⟨i, h_mem⟩        use (eq i).1 ; simp        use (eq i).2 ; simp [h_mem]  · rintro ⟨n, U, V, h_reg, rfl⟩    induction' n with n h_ind    · use { State := Unit, init := {}, next := fun _ _ ↦ {} }, {} ; constructor      · exact Finite.of_fintype Unit      ext as ; simp ; by_contra h_contra      obtain ⟨ss, h_run, _⟩ := h_contra      simp [Automata.NA.InfRun] at h_run    let U' := (fun i : Fin n ↦ U i.castSucc)    let V' := (fun i : Fin n ↦ V i.castSucc)    specialize h_ind U' V' (by intro i ; simp [U', V', h_reg i.castSucc])    have h : (⋃ i, (U i) * (V i)^ω)           = (⋃ i, (U' i) * (V' i)^ω) ∪ (U (Fin.last n)) * (V (Fin.last n))^ω := by      ext as ; simp ; constructor      · rintro ⟨i, h_i⟩        obtain (⟨i', rfl⟩ | rfl) := Fin.eq_castSucc_or_eq_last i        . left ; use i'        . right ; assumption      · rintro (⟨i, h_i⟩ | h_n)        · use i.castSucc        · use (Fin.last n)    rw [h]    apply omega_reg_lang_union h_ind    apply omega_reg_lang_concat    · exact (h_reg (Fin.last n)).1    · apply omega_reg_lang_omega_iter      exact (h_reg (Fin.last n)).2