Choueka lang omega limit subset omega power

theorem choueka_lang_omega_limit_subset_omega_power [Inhabited A] {M : DA A} {acc : Set M.State} :    (M.ChouekaLang acc)↗ω ⊆ (M.toNA.AcceptedLang acc)^ω := by  intro as ; simp [instOmegaLimit, OmegaLimit, frequently_iff_strict_mono]  intro φ h_φ_mono h_prefix  have h_m_ex : ∀ n, ∃ m, 0 < m ∧ m < φ n ∧      M.RunOn (as.extract 0 m) ∈ acc ∧ M.RunOn (as.extract m (φ n)) = M.RunOn (as.extract 0 (φ n)) ∧      ∀ k, m < k → k < φ n → M.RunOn (as.extract m k) ≠ M.RunOn (as.extract 0 k) := by    intro n    obtain ⟨m, h_m0, h_m1, h_acc, h_run, h_run'⟩ := h_prefix n    simp [length_extract] at h_m1    simp [-List.extract_eq_drop_take, extract_extract2 (show m ≤ φ n by omega)] at h_acc    simp [-List.extract_eq_drop_take, extract_extract1] at h_run    use m ; simp [h_m0, h_m1, h_acc, h_run]    intro k h_k h_k'    specialize h_run' k h_k (by simp [length_extract, h_k'])    simp [-List.extract_eq_drop_take, extract_extract2 (show k ≤ φ n by omega)] at h_run'    exact h_run'  choose φ' h_φ'_0 h_φ'_n h_acc h_run h_run' using h_m_ex  have h_inj : Injective φ' := by    intro n1 n2 h_φ' ; by_contra h_contra    wlog h : n1 < n2 generalizing n1 n2 with h'    · exact h' h_φ'.symm (by omega) (by omega)    have := h_φ_mono h ; have := h_φ'_n n1 ; have := h_run n1    have := h_run' n2 (φ n1) (by omega) (by omega)    simp_all  obtain ⟨σ, h_σ_mono, h_φ_φ'⟩ := greater_subseq_lemma φ φ' h_inj  use (fun k ↦ if k = 0 then 0 else φ' (σ (k - 1))) ; simp ; constructor  · apply strictMono_nat_of_lt_succ ; intro n    rcases (show n = 0 ∨ ¬ n = 0 by omega) with h_n | h_n <;> simp [h_n]    · exact h_φ'_0 (σ 0)    have := h_φ'_n (σ (n - 1))    have := h_φ_φ' (n - 1)    grind  · intro n    simp [da_acc_lang_iff_run_acc]    rcases (show n = 0 ∨ ¬ n = 0 by omega) with h_n | h_n <;> simp [h_n]    · exact h_acc (σ 0)    have h1 := h_φ'_n (σ (n - 1))    have h2 := h_φ_φ' (n - 1) ; simp [show n - 1 + 1 = n by omega] at h2    have h3 := append_extract_extract (xs := as) (show φ' (σ (n - 1)) ≤ φ (σ (n - 1)) by omega)      (show φ (σ (n - 1)) ≤ φ' (σ n) by omega)    have h4 := h_run (σ (n - 1)) ; simp [DA.RunOn] at h4    simp [← h3, DA.RunOn, da_run_from_on_append, h4]    have h5 := append_extract_extract (xs := as) (show 0 ≤ φ (σ (n - 1)) by omega)      (show φ (σ (n - 1)) ≤ φ' (σ n) by omega)    simp [← da_run_from_on_append, h5]    exact h_acc (σ n)