refine' iIndepSet.Indep_comap ((iIndepSet_iff_meas_iInter fun i ↦ _).2 _)
α : Type u_1
Ω : Type u_2
inst✝¹ : MeasurableSpace Ω
X Y : Ω → Set α
μ : Measure Ω
p q : ℝ≥0
hX : IsBernoulliSeq X p μ
hY : IsBernoulliSeq Y q μ
inst✝ : IsProbabilityMeasure μ
h : IndepFun X Y μ
⊢ iIndepFun inferInstance (fun a ω => a ∈ X ω ∩ Y ω) μ
case refine'_1
α : Type u_1
Ω : Type u_2
inst✝¹ : MeasurableSpace Ω
X Y : Ω → Set α
μ : Measure Ω
p q : ℝ≥0
hX : IsBernoulliSeq X p μ
hY : IsBernoulliSeq Y q μ
inst✝ : IsProbabilityMeasure μ
h : IndepFun X Y μ
i : α
⊢ MeasurableSet fun ω => (X ω ∩ Y ω) i

case refine'_2
α : Type u_1
Ω : Type u_2
inst✝¹ : MeasurableSpace Ω
X Y : Ω → Set α
μ : Measure Ω
p q : ℝ≥0
hX : IsBernoulliSeq X p μ
hY : IsBernoulliSeq Y q μ
inst✝ : IsProbabilityMeasure μ
h : IndepFun X Y μ
⊢ ∀ (t : Finset α), μ (⋂ i ∈ t, fun ω => (X ω ∩ Y ω) i) = ∏ i ∈ t, μ fun ω => (X ω ∩ Y ω) i