Pair acc lang frequently from run

theorem pair_acc_lang_frequently_from_run {as : Stream' A} {ss : Stream' M.State} {φ : Stream' ℕ}    (h_next : ∀ k, ss (k + 1) ∈ M.next (ss k) (as k)) (h_acc : ∃ᶠ k in Filter.atTop, ss k ∈ acc) (h_mono : StrictMono φ) :    ∃ᶠ m in Filter.atTop, as.extract (φ m) (φ (m + 1)) ∈ M.PairAccLang acc (ss (φ m)) (ss (φ (m + 1))) := by  have h_acc' := frequently_atTop.mp h_acc  have h_mono' := frequently_atTop.mp <| Nat.frequently_atTop_iff_infinite.mpr <| strict_mono_infinite h_mono  apply frequently_atTop.mpr ; intro m  obtain ⟨k, h_k, h_k_acc⟩ := h_acc' (φ m)  let n := Segment' φ k  use n ; constructor  · exact segment'_lower_val h_mono h_k  · use (fun k ↦ ss (k + φ n)) ; constructor    · have : φ n < φ (n + 1) := h_mono (show n < n + 1 by omega)      simp (disch := omega) [NA.PairPath, length_extract, get_extract', (show φ (n + 1) - φ n + φ n = φ (n + 1) by omega)]      intro j h_j ; have := h_next (j + φ n)      simpa [(show j + 1 + φ n = j + φ n + 1 by omega), (show φ n + j = j + φ n by omega)]    · have : φ 0 ≤ φ m := by simp [StrictMono.le_iff_le h_mono]      have h1 : φ 0 ≤ k := by omega      have : φ n ≤ k := by exact segment'_lower_bound h_mono h1      use (k - φ n)      simp [h_k_acc, length_extract, (show k - φ n + φ n = k by omega)]      have : k < φ (n + 1) := by exact segment'_upper_bound h_mono h1      omega