internlm/Lean-Github huggingface dataset:
Theorem: ProbabilityTheory.IsBernoulliSeq.meas
Proof 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 μ
inst✝ : Fintype α
s : Finset α
⊢ ∀ a ∈ s, μ {x | a ∈ {a | a ∈ X x} ↔ a ∈ ↑s} = ↑p
Tactic:
rintro a hi
Proof state after:
α : 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 μ
inst✝ : Fintype α
s : Finset α
a : α
hi : a ∈ s
⊢ μ {x | a ∈ {a | a ∈ X x} ↔ a ∈ ↑s} = ↑p
Theorem: ProbabilityTheory.IsBernoulliSeq.meas
Proof 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 μ
inst✝ : Fintype α
s : Finset α
a : α
hi : a ∈ s
⊢ μ {x | a ∈ {a | a ∈ X x} ↔ a ∈ ↑s} = ↑p
Tactic:
simp only [hi, mem_setOf_eq, Finset.mem_coe, iff_true_iff, hX.meas_apply]
Proof state after:
no goals
Theorem: ProbabilityTheory.IsBernoulliSeq.meas
Proof state before:
case pos
α : 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 μ
inst✝ : Fintype α
s : Finset α
a : α
h✝ : a ∈ s
⊢ MeasurableSet {x | a ∈ {a | a ∈ X x} ↔ a ∈ ↑s}
Tactic:
simp only [mem_setOf_eq, Finset.mem_coe, iff_true_iff, *]
Proof state after:
case pos
α : 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 μ
inst✝ : Fintype α
s : Finset α
a : α
h✝ : a ∈ s
⊢ MeasurableSet {x | a ∈ X x}
Theorem: ProbabilityTheory.IsBernoulliSeq.meas
Proof state before:
case pos
α : 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 μ
inst✝ : Fintype α
s : Finset α
a : α
h✝ : a ∈ s
⊢ MeasurableSet {x | a ∈ X x}
Tactic:
exact ⟨{True}, trivial, by ext; simp⟩
Proof state after:
no goals
Theorem: ProbabilityTheory.IsBernoulliSeq.meas
Proof 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 μ
inst✝ : Fintype α
s : Finset α
a : α
h✝ : a ∈ s
⊢ (fun ω => a ∈ X ω) ⁻¹' {True} = {x | a ∈ X x}
Tactic:
ext
Proof state after:
case h
α : 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 μ
inst✝ : Fintype α
s : Finset α
a : α
h✝ : a ∈ s
x✝ : Ω
⊢ x✝ ∈ (fun ω => a ∈ X ω) ⁻¹' {True} ↔ x✝ ∈ {x | a ∈ X x}
Theorem: ProbabilityTheory.IsBernoulliSeq.meas
Proof state before:
case h
α : 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 μ
inst✝ : Fintype α
s : Finset α
a : α
h✝ : a ∈ s
x✝ : Ω
⊢ x✝ ∈ (fun ω => a ∈ X ω) ⁻¹' {True} ↔ x✝ ∈ {x | a ∈ X x}
Tactic:
simp
Proof state after:
no goals
Theorem: ProbabilityTheory.IsBernoulliSeq.meas
Proof state before:
case neg
α : 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 μ
inst✝ : Fintype α
s : Finset α
a : α
h✝ : a ∉ s
⊢ MeasurableSet {x | a ∈ {a | a ∈ X x} ↔ a ∈ ↑s}
Tactic:
simp only [mem_setOf_eq, Finset.mem_coe, iff_false_iff, *]
Proof state after:
case neg
α : 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 μ
inst✝ : Fintype α
s : Finset α
a : α
h✝ : a ∉ s
⊢ MeasurableSet {x | a ∉ X x}
Theorem: ProbabilityTheory.IsBernoulliSeq.meas
Proof state before:
case neg
α : 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 μ
inst✝ : Fintype α
s : Finset α
a : α
h✝ : a ∉ s
⊢ MeasurableSet {x | a ∉ X x}
Tactic:
exact ⟨{False}, trivial, by ext; simp⟩
Proof state after:
no goals
Theorem: ProbabilityTheory.IsBernoulliSeq.meas
Proof 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 μ
inst✝ : Fintype α
s : Finset α
a : α
h✝ : a ∉ s
⊢ (fun ω => a ∈ X ω) ⁻¹' {False} = {x | a ∉ X x}
Tactic:
ext
Proof state after:
case h
α : 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 μ
inst✝ : Fintype α
s : Finset α
a : α
h✝ : a ∉ s
x✝ : Ω
⊢ x✝ ∈ (fun ω => a ∈ X ω) ⁻¹' {False} ↔ x✝ ∈ {x | a ∉ X x}
Theorem: ProbabilityTheory.IsBernoulliSeq.meas
Proof state before:
case h
α : 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 μ
inst✝ : Fintype α
s : Finset α
a : α
h✝ : a ∉ s
x✝ : Ω
⊢ x✝ ∈ (fun ω => a ∈ X ω) ⁻¹' {False} ↔ x✝ ∈ {x | a ∉ X x}
Tactic:
simp
Proof state after:
no goals
Theorem: ProbabilityTheory.IsBernoulliSeq.compl
Proof 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 μ
⊢ iIndepFun inferInstance (fun a ω => a ∈ (X ω)ᶜ) μ
Tactic:
simp only [iIndepFun_iff, mem_compl_iff, MeasurableSpace.comap_not]
Proof state after:
α : 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 μ
⊢ ∀ (s : Finset α) {f' : α → Set Ω}, (∀ i ∈ s, MeasurableSet (f' i)) → μ (⋂ i ∈ s, f' i) = ∏ i ∈ s, μ (f' i)
Theorem: ProbabilityTheory.IsBernoulliSeq.compl
Proof 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 μ
⊢ ∀ (s : Finset α) {f' : α → Set Ω}, (∀ i ∈ s, MeasurableSet (f' i)) → μ (⋂ i ∈ s, f' i) = ∏ i ∈ s, μ (f' i)
Tactic:
exact (iIndepFun_iff _ _ _).1 hX.iIndepFun
Proof state after:
no goals
Theorem: ProbabilityTheory.IsBernoulliSeq.compl
Proof 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 μ
a : α
⊢ Measure.map (fun ω => a ∈ (X ω)ᶜ) μ = (PMF.bernoulli' (1 - p) ⋯).toMeasure
Tactic:
have : Measurable Not := fun _ _ ↦ trivial
Proof state after:
α : 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 μ
a : α
this : Measurable Not
⊢ Measure.map (fun ω => a ∈ (X ω)ᶜ) μ = (PMF.bernoulli' (1 - p) ⋯).toMeasure
Theorem: ProbabilityTheory.IsBernoulliSeq.compl
Proof 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 μ
a : α
this : Measurable Not
⊢ Measure.map (fun ω => a ∈ (X ω)ᶜ) μ = (PMF.bernoulli' (1 - p) ⋯).toMeasure
Tactic:
refine' (this.aemeasurable.map_map_of_aemeasurable (hX.aemeasurable _)).symm.trans _
Proof state after:
α : 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 μ
a : α
this : Measurable Not
⊢ Measure.map Not (Measure.map (fun ω => a ∈ X ω) μ) = (PMF.bernoulli' (1 - p) ⋯).toMeasure
Theorem: ProbabilityTheory.IsBernoulliSeq.compl
Proof 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 μ
a : α
this : Measurable Not
⊢ Measure.map Not (Measure.map (fun ω => a ∈ X ω) μ) = (PMF.bernoulli' (1 - p) ⋯).toMeasure
Tactic:
rw [hX.map, PMF.map_toMeasure _ this, PMF.map_not_bernoulli']
Proof state after:
no goals
Theorem: ProbabilityTheory.IsBernoulliSeq.inter
Proof 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 _)
Proof 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
Theorem: ProbabilityTheory.IsBernoulliSeq.inter
Proof 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 _ _
Proof 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
Theorem: ProbabilityTheory.IsBernoulliSeq.inter
Proof 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
Proof 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
Theorem: ProbabilityTheory.IsBernoulliSeq.inter
Proof 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
Proof 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
Theorem: ProbabilityTheory.IsBernoulliSeq.inter
Proof 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 ↦ _
Proof 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
Theorem: ProbabilityTheory.IsBernoulliSeq.inter
Proof 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})
Proof 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})
Theorem: ProbabilityTheory.IsBernoulliSeq.inter
Proof 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]
Proof 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})
Theorem: ProbabilityTheory.IsBernoulliSeq.inter
Proof 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]
Proof 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})
Theorem: ProbabilityTheory.IsBernoulliSeq.inter
Proof 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
Proof 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})
Theorem: ProbabilityTheory.IsBernoulliSeq.inter
Proof 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
Proof 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})