Ω : Type u_1
ι : Type ?u.972730
inst✝ : MeasurableSpace Ω
s₁ s₂ s' : Set (Set Ω)
μ : MeasureTheory.Measure Ω
h₁ : IndepSets s₁ s'
h₂ : IndepSets s₂ s'
t1 t2 : Set Ω
ht1 : t1 ∈ s₁ ∪ s₂
ht2 : t2 ∈ s'
⊢ ↑↑μ (t1 ∩ t2) = ↑↑μ t1 * ↑↑μ t2
Ω : Type u_1
ι : Type ?u.972730
inst✝ : MeasurableSpace Ω
s₁ s₂ s' : Set (Set Ω)
μ : MeasureTheory.Measure Ω
h₁ : IndepSets s₁ s'
h₂ : IndepSets s₂ s'
⊢ IndepSets (s₁ ∪ s₂) s'
intro t1 t2 ht1 ht2
case inl
Ω : Type u_1
ι : Type ?u.972730
inst✝ : MeasurableSpace Ω
s₁ s₂ s' : Set (Set Ω)
μ : MeasureTheory.Measure Ω
h₁ : IndepSets s₁ s'
h₂ : IndepSets s₂ s'
t1 t2 : Set Ω
ht1 : t1 ∈ s₁ ∪ s₂
ht2 : t2 ∈ s'
ht1₁ : t1 ∈ s₁
⊢ ↑↑μ (t1 ∩ t2) = ↑↑μ t1 * ↑↑μ t2

case inr
Ω : Type u_1
ι : Type ?u.972730
inst✝ : MeasurableSpace Ω
s₁ s₂ s' : Set (Set Ω)
μ : MeasureTheory.Measure Ω
h₁ : IndepSets s₁ s'
h₂ : IndepSets s₂ s'
t1 t2 : Set Ω
ht1 : t1 ∈ s₁ ∪ s₂
ht2 : t2 ∈ s'
ht1₂ : t1 ∈ s₂
⊢ ↑↑μ (t1 ∩ t2) = ↑↑μ t1 * ↑↑μ t2
Ω : Type u_1
ι : Type ?u.972730
inst✝ : MeasurableSpace Ω
s₁ s₂ s' : Set (Set Ω)
μ : MeasureTheory.Measure Ω
h₁ : IndepSets s₁ s'
h₂ : IndepSets s₂ s'
t1 t2 : Set Ω
ht1 : t1 ∈ s₁ ∪ s₂
ht2 : t2 ∈ s'
⊢ ↑↑μ (t1 ∩ t2) = ↑↑μ t1 * ↑↑μ t2
cases' (Set.mem_union _ _ _).mp ht1 with ht1₁ ht1₂
no goals
case inl
Ω : Type u_1
ι : Type ?u.972730
inst✝ : MeasurableSpace Ω
s₁ s₂ s' : Set (Set Ω)
μ : MeasureTheory.Measure Ω
h₁ : IndepSets s₁ s'
h₂ : IndepSets s₂ s'
t1 t2 : Set Ω
ht1 : t1 ∈ s₁ ∪ s₂
ht2 : t2 ∈ s'
ht1₁ : t1 ∈ s₁
⊢ ↑↑μ (t1 ∩ t2) = ↑↑μ t1 * ↑↑μ t2
exact h₁ t1 t2 ht1₁ ht2
no goals
case inr
Ω : Type u_1
ι : Type ?u.972730
inst✝ : MeasurableSpace Ω
s₁ s₂ s' : Set (Set Ω)
μ : MeasureTheory.Measure Ω
h₁ : IndepSets s₁ s'
h₂ : IndepSets s₂ s'
t1 t2 : Set Ω
ht1 : t1 ∈ s₁ ∪ s₂
ht2 : t2 ∈ s'
ht1₂ : t1 ∈ s₂
⊢ ↑↑μ (t1 ∩ t2) = ↑↑μ t1 * ↑↑μ t2
exact h₂ t1 t2 ht1₂ ht2