Acc omega lang concat

theorem acc_omega_lang_concat :    (M0.Concat acc0 M1).AcceptedOmegaLang (inr '' acc1) =    (M0.AcceptedLang acc0) * (M1.AcceptedOmegaLang acc1) := by  ext as ; constructor  · rintro ⟨ss, h_run, h_acc⟩    obtain ⟨n, s1, h_s1_acc, h_s1⟩ := Frequently.exists h_acc    have h_s1_ex : ∃ n s1, ss n = inr s1 := by use n, s1 ; simp [h_s1]    obtain ⟨n, ⟨ss0, h_run0, h_acc0, h_ss0⟩, ⟨ss1, h_run1, h_ss1⟩⟩ := na_concat_inf_run.mp ⟨h_run, h_s1_ex⟩    use (as.extract 0 n), (as.drop n) ; simp [append_extract_drop] ; constructor    · use n, as ; constructor      · use ss0      · rfl    · use ss1 ; simp [h_run1]      have h_ss1_ev : ∀ᶠ k in atTop, ss k = inr (ss1 (k - n)) := by        simp only [eventually_atTop] ; use (n + 1)      have h_ss1_acc := Frequently.and_eventually h_acc h_ss1_ev      simp [frequently_atTop] at h_ss1_acc ⊢      intro k ; obtain ⟨j, h_j, ⟨t1, h_t1_acc, h_t1⟩, h_j_ss1⟩ := h_ss1_acc (n + k)      use (j - n) ; rw [← h_t1, inr.inj_iff] at h_j_ss1      simpa [(by omega : k ≤ j - n), ← h_j_ss1]  · rintro ⟨al0, as1, ⟨n, as0, ⟨ss0, ⟨h_init0, h_next0⟩, h_acc0⟩, rfl⟩, ⟨ss1, h_run1, h_acc1⟩, h_as⟩    let ss := fun k ↦ if k < n + 1 then inl (ss0 k) else inr (ss1 (k - n))    use ss  ; constructor    · suffices (M0.Concat acc0 M1).InfRun as ss ∧ (∃ n s1, ss n = inr s1) by tauto      apply na_concat_inf_run.mpr      use n ; constructor      · use ss0 ; simp [ss, h_acc0] ; constructor        · exact h_init0        · intro k h_k          have h1 : k < (as0.extract 0 n).length := by simp [length_extract, h_k]          simp (disch := omega) [← h_as, get_append_left' h1, get_extract', h_next0 k h_k]      · use ss1 ; simp [ss]        have h1 : (as0.extract 0 n).length = n := by simp [length_extract]        rw [← h1] ; simp [← h_as, drop_append_stream, h_run1]    · have h_ss1_ev : ∀ᶠ k in atTop, ss (k + n) = inr (ss1 k) := by        simp only [eventually_atTop]        use (n + 1) ; intro k h_k ; simp [ss] ; omega      have h_ss1_acc := Frequently.and_eventually h_acc1 h_ss1_ev      simp [frequently_atTop] at h_ss1_acc ⊢      intro k ; obtain ⟨j, h_j, h_j_acc, h_j_ss1⟩ := h_ss1_acc (n + k)      use (j + n) ; simp [(by omega : k ≤ j + n)]      use (ss1 j) ; simp [h_j_acc, h_j_ss1]