Theorem: ProbabilityTheory.IsBernoulliSeq.inter (LeanCamCombi/BernoulliSeq.lean)

State before:
α : 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 ω) μ
Tactic:
refine' iIndepSet.Indep_comap ((iIndepSet_iff_meas_iInter fun i ↦ _).2 _)
State after:
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

State before:
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
Tactic:
refine' MeasurableSet.inter _ _
State after:
case refine'_1.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 ω i

case refine'_1.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 μ
i : α
⊢ MeasurableSet fun ω => 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

State before:
case refine'_1.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 ω i

case refine'_1.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 μ
i : α
⊢ MeasurableSet fun ω => 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
Tactic:
sorry
State after:
case refine'_1.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 μ
i : α
⊢ MeasurableSet fun ω => 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

State before:
case refine'_1.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 μ
i : α
⊢ MeasurableSet fun ω => 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
Tactic:
sorry
State after:
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

State before:
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
Tactic:
refine' fun s ↦ _
State after:
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

State before:
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
Tactic:
change μ (⋂ i ∈ s, {ω | X ω i} ∩ {ω | Y ω i}) = s.prod fun i ↦ μ ({ω | X ω i} ∩ {ω | Y ω i})
State after:
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})

State before:
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})
Tactic:
simp_rw [iInter_inter_distrib]
State after:
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}) ∩ ⋂ i ∈ s, {ω | Y ω i}) = ∏ i ∈ s, μ ({ω | X ω i} ∩ {ω | Y ω i})

State before:
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}) ∩ ⋂ i ∈ s, {ω | Y ω i}) = ∏ i ∈ s, μ ({ω | X ω i} ∩ {ω | Y ω i})
Tactic:
rw [h.meas_inter, hX.iIndepFun.meas_biInter, hY.iIndepFun.meas_biInter,
  ← Finset.prod_mul_distrib]
State after:
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 α
⊢ ∏ x ∈ s, μ {ω | X ω x} * μ {ω | Y ω x} = ∏ i ∈ s, μ ({ω | 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, MeasurableSet {ω | 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, MeasurableSet {ω | X ω i}

case refine'_2.hs
α : 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 α
⊢ MeasurableSet (⋂ i ∈ s, {ω | X ω i})

case refine'_2.ht
α : 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 α
⊢ MeasurableSet (⋂ i ∈ s, {ω | Y ω i})

State before:
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 α
⊢ ∏ x ∈ s, μ {ω | X ω x} * μ {ω | Y ω x} = ∏ i ∈ s, μ ({ω | 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, MeasurableSet {ω | 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, MeasurableSet {ω | X ω i}

case refine'_2.hs
α : 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 α
⊢ MeasurableSet (⋂ i ∈ s, {ω | X ω i})

case refine'_2.ht
α : 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 α
⊢ MeasurableSet (⋂ i ∈ s, {ω | Y ω i})
Tactic:
refine' Finset.prod_congr rfl fun i hi ↦ (h.meas_inter _ _).symm
State after:
case refine'_2.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 μ
s : Finset α
i : α
hi : i ∈ s
⊢ MeasurableSet {ω | X ω i}

case refine'_2.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 : α
hi : i ∈ s
⊢ MeasurableSet {ω | 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, MeasurableSet {ω | 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, MeasurableSet {ω | X ω i}

case refine'_2.hs
α : 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 α
⊢ MeasurableSet (⋂ i ∈ s, {ω | X ω i})

case refine'_2.ht
α : 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 α
⊢ MeasurableSet (⋂ i ∈ s, {ω | Y ω i})

State before:
case refine'_2.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 μ
s : Finset α
i : α
hi : i ∈ s
⊢ MeasurableSet {ω | X ω i}

case refine'_2.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 : α
hi : i ∈ s
⊢ MeasurableSet {ω | 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, MeasurableSet {ω | 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, MeasurableSet {ω | X ω i}

case refine'_2.hs
α : 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 α
⊢ MeasurableSet (⋂ i ∈ s, {ω | X ω i})

case refine'_2.ht
α : 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 α
⊢ MeasurableSet (⋂ i ∈ s, {ω | Y ω i})
Tactic:
sorry
State after:
case refine'_2.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 : α
hi : i ∈ s
⊢ MeasurableSet {ω | 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, MeasurableSet {ω | 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, MeasurableSet {ω | X ω i}

case refine'_2.hs
α : 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 α
⊢ MeasurableSet (⋂ i ∈ s, {ω | X ω i})

case refine'_2.ht
α : 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 α
⊢ MeasurableSet (⋂ i ∈ s, {ω | Y ω i})

State before:
case refine'_2.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 : α
hi : i ∈ s
⊢ MeasurableSet {ω | 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, MeasurableSet {ω | 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, MeasurableSet {ω | X ω i}

case refine'_2.hs
α : 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 α
⊢ MeasurableSet (⋂ i ∈ s, {ω | X ω i})

case refine'_2.ht
α : 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 α
⊢ MeasurableSet (⋂ i ∈ s, {ω | Y ω i})
Tactic:
sorry
State after:
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, MeasurableSet {ω | 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, MeasurableSet {ω | X ω i}

case refine'_2.hs
α : 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 α
⊢ MeasurableSet (⋂ i ∈ s, {ω | X ω i})

case refine'_2.ht
α : 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 α
⊢ MeasurableSet (⋂ i ∈ s, {ω | Y ω i})

State before:
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, MeasurableSet {ω | 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, MeasurableSet {ω | X ω i}

case refine'_2.hs
α : 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 α
⊢ MeasurableSet (⋂ i ∈ s, {ω | X ω i})

case refine'_2.ht
α : 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 α
⊢ MeasurableSet (⋂ i ∈ s, {ω | Y ω i})
Tactic:
sorry
State after:
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, MeasurableSet {ω | X ω i}

case refine'_2.hs
α : 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 α
⊢ MeasurableSet (⋂ i ∈ s, {ω | X ω i})

case refine'_2.ht
α : 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 α
⊢ MeasurableSet (⋂ i ∈ s, {ω | Y ω i})

State before:
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, MeasurableSet {ω | X ω i}

case refine'_2.hs
α : 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 α
⊢ MeasurableSet (⋂ i ∈ s, {ω | X ω i})

case refine'_2.ht
α : 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 α
⊢ MeasurableSet (⋂ i ∈ s, {ω | Y ω i})
Tactic:
sorry
State after:
case refine'_2.hs
α : 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 α
⊢ MeasurableSet (⋂ i ∈ s, {ω | X ω i})

case refine'_2.ht
α : 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 α
⊢ MeasurableSet (⋂ i ∈ s, {ω | Y ω i})

State before:
case refine'_2.hs
α : 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 α
⊢ MeasurableSet (⋂ i ∈ s, {ω | X ω i})

case refine'_2.ht
α : 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 α
⊢ MeasurableSet (⋂ i ∈ s, {ω | Y ω i})
Tactic:
sorry
State after:
case refine'_2.ht
α : 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 α
⊢ MeasurableSet (⋂ i ∈ s, {ω | Y ω i})

State before:
case refine'_2.ht
α : 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 α
⊢ MeasurableSet (⋂ i ∈ s, {ω | Y ω i})
Tactic:
sorry
State after:
no goals