Ω : Type u_1
ι : Type ?u.53841
m m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
t : Set Ω
h_indep : ↑↑μ (t ∩ t) = ↑↑μ t * ↑↑μ t
⊢ ↑↑μ t = 0 ∨ ↑↑μ t = 1 ∨ ↑↑μ t = ⊤
Ω : Type u_1
ι : Type ?u.53841
m m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
t : Set Ω
h_indep : IndepSet t t
⊢ ↑↑μ t = 0 ∨ ↑↑μ t = 1 ∨ ↑↑μ t = ⊤
specialize h_indep t t (measurableSet_generateFrom (Set.mem_singleton t))
  (measurableSet_generateFrom (Set.mem_singleton t))
case pos
Ω : Type u_1
ι : Type ?u.53841
m m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
t : Set Ω
h_indep : ↑↑μ (t ∩ t) = ↑↑μ t * ↑↑μ t
h0 : ↑↑μ t = 0
⊢ ↑↑μ t = 0 ∨ ↑↑μ t = 1 ∨ ↑↑μ t = ⊤

case neg
Ω : Type u_1
ι : Type ?u.53841
m m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
t : Set Ω
h_indep : ↑↑μ (t ∩ t) = ↑↑μ t * ↑↑μ t
h0 : ¬↑↑μ t = 0
⊢ ↑↑μ t = 0 ∨ ↑↑μ t = 1 ∨ ↑↑μ t = ⊤
Ω : Type u_1
ι : Type ?u.53841
m m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
t : Set Ω
h_indep : ↑↑μ (t ∩ t) = ↑↑μ t * ↑↑μ t
⊢ ↑↑μ t = 0 ∨ ↑↑μ t = 1 ∨ ↑↑μ t = ⊤
by_cases h0 : μ t = 0
case pos
Ω : Type u_1
ι : Type ?u.53841
m m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
t : Set Ω
h_indep : ↑↑μ (t ∩ t) = ↑↑μ t * ↑↑μ t
h0 : ¬↑↑μ t = 0
h_top : ↑↑μ t = ⊤
⊢ ↑↑μ t = 0 ∨ ↑↑μ t = 1 ∨ ↑↑μ t = ⊤

case neg
Ω : Type u_1
ι : Type ?u.53841
m m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
t : Set Ω
h_indep : ↑↑μ (t ∩ t) = ↑↑μ t * ↑↑μ t
h0 : ¬↑↑μ t = 0
h_top : ¬↑↑μ t = ⊤
⊢ ↑↑μ t = 0 ∨ ↑↑μ t = 1 ∨ ↑↑μ t = ⊤
case neg
Ω : Type u_1
ι : Type ?u.53841
m m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
t : Set Ω
h_indep : ↑↑μ (t ∩ t) = ↑↑μ t * ↑↑μ t
h0 : ¬↑↑μ t = 0
⊢ ↑↑μ t = 0 ∨ ↑↑μ t = 1 ∨ ↑↑μ t = ⊤
by_cases h_top : μ t = ∞
case neg
Ω : Type u_1
ι : Type ?u.53841
m m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
t : Set Ω
h_indep : 1 = ↑↑μ t
h0 : ¬↑↑μ t = 0
h_top : ¬↑↑μ t = ⊤
⊢ ↑↑μ t = 0 ∨ ↑↑μ t = 1 ∨ ↑↑μ t = ⊤
case neg
Ω : Type u_1
ι : Type ?u.53841
m m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
t : Set Ω
h_indep : ↑↑μ (t ∩ t) = ↑↑μ t * ↑↑μ t
h0 : ¬↑↑μ t = 0
h_top : ¬↑↑μ t = ⊤
⊢ ↑↑μ t = 0 ∨ ↑↑μ t = 1 ∨ ↑↑μ t = ⊤
rw [← one_mul (μ (t ∩ t)), Set.inter_self, ENNReal.mul_eq_mul_right h0 h_top] at h_indep
no goals
case neg
Ω : Type u_1
ι : Type ?u.53841
m m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
t : Set Ω
h_indep : 1 = ↑↑μ t
h0 : ¬↑↑μ t = 0
h_top : ¬↑↑μ t = ⊤
⊢ ↑↑μ t = 0 ∨ ↑↑μ t = 1 ∨ ↑↑μ t = ⊤
exact Or.inr (Or.inl h_indep.symm)
no goals
case pos
Ω : Type u_1
ι : Type ?u.53841
m m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
t : Set Ω
h_indep : ↑↑μ (t ∩ t) = ↑↑μ t * ↑↑μ t
h0 : ↑↑μ t = 0
⊢ ↑↑μ t = 0 ∨ ↑↑μ t = 1 ∨ ↑↑μ t = ⊤
exact Or.inl h0
no goals
case pos
Ω : Type u_1
ι : Type ?u.53841
m m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
t : Set Ω
h_indep : ↑↑μ (t ∩ t) = ↑↑μ t * ↑↑μ t
h0 : ¬↑↑μ t = 0
h_top : ↑↑μ t = ⊤
⊢ ↑↑μ t = 0 ∨ ↑↑μ t = 1 ∨ ↑↑μ t = ⊤
exact Or.inr (Or.inr h_top)