ProbabilityTheory.iIndepFun.ae_eq

theorem iIndepFun.ae_eq {ι : Type*} {β : ι → Type*}    {m : ∀ i, MeasurableSpace (β i)} {f g : ∀ i, Ω → β i}    (hf_Indep : iIndepFun f μ) (hfg : ∀ i, f i =ᵐ[μ] g i) : iIndepFun g μ := by  rw [iIndepFun_iff_iIndep, iIndep_iff] at hf_Indep ⊢  intro s E H  have (i : ι) :      ∃ E' : Set Ω, i ∈ s → MeasurableSet[MeasurableSpace.comap (f i) (m i)] E' ∧ E' =ᵐ[μ] E i := by    by_cases hi: i ∈ s    · rcases H i hi with ⟨F, mF, hFE⟩      use (f i)⁻¹' F      simp only [hi, forall_const]      constructor      · use F      rw [← hFE]      exact Filter.EventuallyEq.preimage (hfg i) F    use ∅    tauto  classical  rcases Classical.axiomOfChoice this with ⟨E', hE'⟩  have hE'' : ∀ i ∈ s, MeasurableSet[MeasurableSpace.comap (f i) (m i)] (E' i) := by    intro i hi; exact (hE' i hi).1  have hE''' : ∀ i ∈ s, E' i =ᵐ[μ] E i := by    intro i hi; exact (hE' i hi).2  convert hf_Indep s hE'' using 1 with i  · apply measure_congr    apply EventuallyEq.finite_iInter    intro i hi    exact (hE''' i hi).symm  apply Finset.prod_congr rfl  intro i hi  exact measure_congr (hE''' i hi).symm