Inf occ pair

theorem inf_occ_pair {X1 X2 : Type*} [Finite X1] [Finite X2] (xs : Stream' (X1 × X2)) :    fst '' (InfOcc xs) = InfOcc (fst ∘ xs) ∧    snd '' (InfOcc xs) = InfOcc (snd ∘ xs) := by  constructor  · ext x1 ; simp ; constructor    · rintro ⟨x2, h_inf⟩      obtain ⟨φ, h_mono, h_x⟩ := frequently_iff_strict_mono.mp h_inf      apply frequently_iff_strict_mono.mpr      aesop    · intro h_inf      let s := { x : X1 × X2 | x.1 = x1 }      have h_inf' : ∃ᶠ k in atTop, xs k ∈ s := by exact h_inf      obtain ⟨x, h_x, h_inf''⟩ := frequently_in_finite_set.mp h_inf'      aesop  · ext x2 ; simp ; constructor    · rintro ⟨x1, h_inf⟩      obtain ⟨φ, h_mono, h_x⟩ := frequently_iff_strict_mono.mp h_inf      apply frequently_iff_strict_mono.mpr      aesop    · intro h_inf      let s := { x : X1 × X2 | x.2 = x2 }      have h_inf' : ∃ᶠ k in atTop, xs k ∈ s := by exact h_inf      obtain ⟨x, h_x, h_inf''⟩ := frequently_in_finite_set.mp h_inf'      aesop