Omega reg lang fin idx congr

theorem omega_reg_lang_fin_idx_congr [Inhabited A] {c : Congruence A} {L : Set (Stream' A)}    (h_fin : Finite (c.QuotType)) (h_amp : c.Ample) (h_sat : c.Saturates L) : OmegaRegLang L := by  rw [congruence_ample_saturates_union h_amp h_sat, omega_reg_lang_iff_finite_union_form]  have eq_quot : Fin (Nat.card c.QuotType) ≃ c.QuotType := by exact (Finite.equivFin c.QuotType).symm  have eq_prod := Equiv.prodCongr eq_quot eq_quot  have eq_fin_prod := (finProdFinEquiv (m := Nat.card c.QuotType) (n := Nat.card c.QuotType)).symm  have eq := Equiv.trans eq_fin_prod eq_prod  use (Nat.card c.QuotType * Nat.card c.QuotType)  use (fun i ↦ if (c.ConcatOmegaLang (eq i).1 (eq i).2 ∩ L).Nonempty then c.EqvCls (eq i).1 else ∅)  use (fun i ↦ c.EqvCls (eq i).2)  constructor  · intro i    have h_reg1 := reg_lang_fin_idx_congr h_fin (eq i).1    have h_reg2 := reg_lang_fin_idx_congr h_fin (eq i).2    rcases Classical.em ((c.ConcatOmegaLang (eq i).1 (eq i).2 ∩ L).Nonempty) with h | h    <;> simp [h, h_reg1, h_reg2, reg_lang_empty]  ext as ; simp ; constructor  · rintro ⟨s, t, h_ne, h_as⟩    use (eq.invFun (s, t)) ; simp [h_ne] ; exact h_as  · rintro ⟨i, h_as⟩    rcases Classical.em ((c.ConcatOmegaLang (eq i).1 (eq i).2 ∩ L).Nonempty) with h | h    <;> simp [h] at h_as    · use (eq i).1, (eq i).2 ; simpa [h]    · simp [empty_ConcatInf] at h_as