change μ (⋂ i ∈ s, {ω | X ω i} ∩ {ω | Y ω i}) = s.prod fun i ↦ μ ({ω | X ω i} ∩ {ω | 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 μ
s : Finset α
⊢ μ (⋂ i ∈ s, fun ω => (X ω ∩ Y ω) i) = ∏ i ∈ s, μ 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 μ
s : Finset α
⊢ μ (⋂ i ∈ s, {ω | X ω i} ∩ {ω | Y ω i}) = ∏ i ∈ s, μ ({ω | X ω i} ∩ {ω | Y ω i})