Acc omega lang loop

theorem acc_omega_lang_loop :    (M.Loop acc).AcceptedOmegaLang {inl ()} = (M.AcceptedLang acc)^ω := by  ext as ; constructor  · rintro ⟨ss, h_run, h_acc⟩ ; simp at h_acc    let φ m := Nat.nth (fun k ↦ ss k = inl ()) m    have h_inf : {k | ss k = inl ()}.Infinite := by simpa [← Nat.frequently_atTop_iff_infinite]    have h_mono : StrictMono φ := by exact Nat.nth_strictMono h_inf    use φ ; simp [h_mono] ; constructor    · have h_init := h_run.1      simp [NA.Loop] at h_init      apply Nat.nth_zero_of_zero h_init    · intro m      use (φ (m + 1) - φ m), (as.drop (φ m)) ; constructor      · have h_mono_m : φ (m + 1) - φ m > 0 := by have := h_mono (show m < m + 1 by omega) ; omega        let ss1 := ss.drop (φ m)        have h_run1 : (M.Loop acc).FinRun (φ (m + 1) - φ m) (as.drop (φ m)) ss1 := by          constructor          · simp [ss1, get_drop', NA.Loop]            apply Nat.nth_mem_of_infinite (p := fun k ↦ ss k = inl ()) h_inf          intro k h_k          simp [ss1, get_drop', ← add_assoc, h_run.2 (φ m + k)]        have h_inl : ss1 (φ (m + 1) - φ m) = inl () := by          simp [ss1, get_drop', (show φ m + (φ (m + 1) - φ m) = φ (m + 1) by omega)]          apply Nat.nth_mem_of_infinite (p := fun k ↦ ss k = inl ()) h_inf        have h_inr : ∀ k < φ (m + 1) - φ m, k > 0 → ss1 k ∈ range inr := by          intro k h_k1 h_k0          obtain ⟨s', h_s'⟩ := not_inl_unit.mp <| nth_succ_gap h_inf m k h_k1 h_k0          use s' ; rw [add_comm] at h_s'          simp [φ, ss1, ← h_s', get_drop']        obtain ⟨ss', h_run', h_acc', _⟩ := (na_loop_fin_run h_mono_m).mp ⟨h_run1, h_inl, h_inr⟩        use ss'      · have := h_mono (show m < m + 1 by omega)        simp [extract_drop, (show φ m + (φ (m + 1) - φ m) = φ (m + 1) by omega)]  · rintro ⟨φ, h_mono, h_0, h_acc⟩    choose len as' h_acc h_as' using h_acc    choose ss' h_run h_acc using h_acc    let seg k := Segment φ k    let ss : Stream' (Unit ⊕ NA.State A) := fun k ↦ if k ∈ range φ then inl () else inr (ss' (seg k) (k - φ (seg k)))    use ss ; constructor <;> [constructor ; skip]    · have h_0' : ∃ k, φ k = 0 := by use 0      simp [ss, h_0', NA.Loop]    · intro k      have h_seg_k : φ (seg k) ≤ k := by exact segment_lower_bound h_mono h_0 k      have h_seg_k1 : k < φ (seg k + 1) := by exact segment_upper_bound h_mono h_0 k      have h_mono_k : φ (seg k + 1) - φ (seg k) > 0 := by omega      suffices h_lhs :          (M.Loop acc).FinRun (φ (seg k + 1) - φ (seg k)) (as.drop (φ (seg k))) (ss.drop (φ (seg k))) ∧          (ss.drop (φ (seg k))) (φ (seg k + 1) - φ (seg k)) = inl () ∧          (∀ j < φ (seg k + 1) - φ (seg k), j > 0 → (ss.drop (φ (seg k))) j ∈ range inr) by        have h_run_k := h_lhs.1.2 (k - φ (seg k)) (show k - φ (seg k) < φ (seg k + 1) - φ (seg k) by omega)        simp [get_drop', (show φ (seg k) + (k - φ (seg k)) = k by omega),          (show φ (seg k) + (k - φ (seg k) + 1) = k + 1 by omega)] at h_run_k        exact h_run_k      apply (na_loop_fin_run h_mono_k).mpr      use (ss' (seg k))      obtain ⟨h_len_k, h_as'_k⟩ := extract_eq_extract <| h_as' (seg k)      simp at h_len_k h_as'_k      simp [← h_len_k, get_drop']      constructorm* _ ∧ _      · apply na_FinRun_modulo (n := len (seg k)) (as := as' (seg k)) (ss := ss' (seg k)) (hr := h_run (seg k))        · intro j h_j ; simp [get_drop', h_as'_k j h_j, add_comm]        · simp      · exact h_acc (seg k)      · simp [ss]      · simp [ss, (show φ (seg k) + len (seg k) = φ (seg k + 1) by omega)]      · intro j h_j_1 h_j_0        have h_j_2 : ¬ ∃ m, φ m = φ (seg k) + j := by          exact segment_range_gap h_mono (show φ (seg k) < φ (seg k) + j by omega) (show φ (seg k) + j < φ (seg k + 1) by omega)        have h_j_3 : seg (φ (seg k) + j) = seg k := by          exact segment_range_val h_mono (show φ (seg k) ≤ φ (seg k) + j by omega) (show φ (seg k) + j < φ (seg k + 1) by omega)        simp [ss, h_j_2, h_j_3]    · have h_uset : {k | ss k = inl ()} = range φ := by ext k ; simp [ss]      simp [Nat.frequently_atTop_iff_infinite, h_uset]      exact strict_mono_infinite h_mono