ProbabilityTheory.iIndepFun_iff'

lemma iIndepFun_iff' [MeasurableSpace Ω] {β : ι → Type*}    (m : ∀ i, MeasurableSpace (β i)) (f : ∀ i, Ω → β i) (μ : Measure Ω) :    iIndepFun f μ ↔ ∀ (s : Finset ι) ⦃f' : ι → Set Ω⦄      (_hf' : ∀ i, MeasurableSet[(m i).comap (f i)] (f' i)),      μ (⋂ i ∈ s, f' i) = ∏ i ∈ s, μ (f' i) := by  classical  rw [iIndepFun_iff]  refine forall_congr' fun s ↦ ⟨fun h f hf ↦ h fun i _ ↦ hf _, fun h f hf ↦ ?_⟩  let g (i : ι) : Set Ω := if i ∈ s then f i else univ  have (i : ι) (hi : i ∈ s) : f i = g i := (if_pos hi).symm  convert @h g _ using 2  · exact iInter₂_congr this  · rw [this _ ‹_›]  · rintro i    by_cases hi : i ∈ s <;> simp [g, hi, hf]