Da concat to muller accept

theorem da_concat_to_muller_accept (as : Stream' A) (n : ℕ)    (h1 : M1.toNA.FinAccept acc1 n as) (h2 : M2.MullerAccept accSet2 (as.drop n)) :    (M1.Concat acc1 M2).MullerAccept (DA.MullerAcc_Concat M1 acc1 M2 accSet2) as := by  obtain ⟨ss, h_run1, h_acc1⟩ := h1  rw [da_fin_run_unique h_run1 n (by omega)] at h_acc1  obtain ⟨i, m, h_m, h_i⟩ := da_concat_ptr2_eventually M1 acc1 M2 as n h_acc1  have h_suffix : ∀ k ≥ m, ((M1.Concat acc1 M2).DetRun as k).2 i = some (M2.DetRun (as.drop n) (k - n)) := by    intro k h_k    have h_p := da_concat_ptr2_det_run M1 acc1 M2 as n h_acc1 (k - n - 1)    simp [h_i k h_k, (show n + (k - n - 1) + 1 = k by omega), (show k - n - 1 + 1 = k - n by omega)] at h_p    exact h_p  use i ; constructor  · suffices h_inf : {s2 | ∃ s ∈ InfOcc ((M1.Concat acc1 M2).DetRun as), s.2 i = some s2} = InfOcc (M2.DetRun (as.drop n)) by      simpa [h_inf]    ext s2 ; constructor    · rintro ⟨s, h_inf, h_s⟩      apply frequently_atTop.mpr ; intro l      obtain ⟨k, h_k, rfl⟩ := frequently_atTop.mp h_inf (m + l)      simp [h_suffix k (by omega)] at h_s      use (k - n) ; simp [h_s] ; omega    · intro h_inf      obtain ⟨l, h_l⟩ := eventually_atTop.mp <| inf_occ_eventually ((M1.Concat acc1 M2).DetRun as)      obtain ⟨k, h_k, rfl⟩ := frequently_atTop.mp h_inf (l + m - n)      use ((M1.Concat acc1 M2).DetRun as (k + n)) ; constructor      · exact h_l (k + n) (by omega)      · simp [h_suffix (k + n) (by omega)]  · intro s h_s    obtain ⟨k, h_k, rfl⟩ := frequently_atTop.mp h_s m    simp [h_suffix k h_k]