-- Mathlib/Probability/Independence/ZeroOne.lean
theorem Kernel.measure_eq_zero_or_one_or_top_of_indepSet_self {t : Set Ω}
    (h_indep : Kernel.IndepSet t t κ μα) :
    ∀ᵐ a ∂μα, κ a t = 0 ∨ κ a t = 1 ∨ κ a t = ∞

Proof state:
case neg
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
t : Set Ω
h_indep : ∀ᵐ (a : α) ∂μα, (κ a) (t ∩ t) = (κ a) t * (κ a) t
a : α
ha : (κ a) (t ∩ t) = (κ a) t * (κ a) t
h0 : ¬(κ a) t = 0
h_top : ¬(κ a) t = ⊤
⊢ (κ a) t = 0 ∨ (κ a) t = 1 ∨ (κ a) t = ⊤

Tactic:
rw [← one_mul (κ a (t ∩ t)), Set.inter_self, ENNReal.mul_left_inj h0 h_top] at ha

Result:
case neg
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
t : Set Ω
h_indep : ∀ᵐ (a : α) ∂μα, (κ a) (t ∩ t) = (κ a) t * (κ a) t
a : α
ha : 1 = (κ a) t
h0 : ¬(κ a) t = 0
h_top : ¬(κ a) t = ⊤
⊢ (κ a) t = 0 ∨ (κ a) t = 1 ∨ (κ a) t = ⊤

Proof state:
case neg
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
t : Set Ω
h_indep : ∀ᵐ (a : α) ∂μα, (κ a) (t ∩ t) = (κ a) t * (κ a) t
a : α
ha : (κ a) (t ∩ t) = (κ a) t * (κ a) t
h0 : ¬(κ a) t = 0
⊢ (κ a) t = 0 ∨ (κ a) t = 1 ∨ (κ a) t = ⊤

Tactic:
by_cases h_top : κ a t = ∞

Result:
case pos
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
t : Set Ω
h_indep : ∀ᵐ (a : α) ∂μα, (κ a) (t ∩ t) = (κ a) t * (κ a) t
a : α
ha : (κ a) (t ∩ t) = (κ a) t * (κ a) t
h0 : ¬(κ a) t = 0
h_top : (κ a) t = ⊤
⊢ (κ a) t = 0 ∨ (κ a) t = 1 ∨ (κ a) t = ⊤

case neg
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
t : Set Ω
h_indep : ∀ᵐ (a : α) ∂μα, (κ a) (t ∩ t) = (κ a) t * (κ a) t
a : α
ha : (κ a) (t ∩ t) = (κ a) t * (κ a) t
h0 : ¬(κ a) t = 0
h_top : ¬(κ a) t = ⊤
⊢ (κ a) t = 0 ∨ (κ a) t = 1 ∨ (κ a) t = ⊤

Proof state:
case pos
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
t : Set Ω
h_indep : ∀ᵐ (a : α) ∂μα, (κ a) (t ∩ t) = (κ a) t * (κ a) t
a : α
ha : (κ a) (t ∩ t) = (κ a) t * (κ a) t
h0 : ¬(κ a) t = 0
h_top : (κ a) t = ⊤
⊢ (κ a) t = 0 ∨ (κ a) t = 1 ∨ (κ a) t = ⊤

Tactic:
exact Or.inr (Or.inr h_top)

Result:
no goals

Proof state:
case pos
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
t : Set Ω
h_indep : ∀ᵐ (a : α) ∂μα, (κ a) (t ∩ t) = (κ a) t * (κ a) t
a : α
ha : (κ a) (t ∩ t) = (κ a) t * (κ a) t
h0 : (κ a) t = 0
⊢ (κ a) t = 0 ∨ (κ a) t = 1 ∨ (κ a) t = ⊤

Tactic:
exact Or.inl h0

Result:
no goals

Proof state:
case h
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
t : Set Ω
h_indep : ∀ᵐ (a : α) ∂μα, (κ a) (t ∩ t) = (κ a) t * (κ a) t
a : α
ha : (κ a) (t ∩ t) = (κ a) t * (κ a) t
⊢ (κ a) t = 0 ∨ (κ a) t = 1 ∨ (κ a) t = ⊤

Tactic:
by_cases h0 : κ a t = 0

Result:
case pos
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
t : Set Ω
h_indep : ∀ᵐ (a : α) ∂μα, (κ a) (t ∩ t) = (κ a) t * (κ a) t
a : α
ha : (κ a) (t ∩ t) = (κ a) t * (κ a) t
h0 : (κ a) t = 0
⊢ (κ a) t = 0 ∨ (κ a) t = 1 ∨ (κ a) t = ⊤

case neg
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
t : Set Ω
h_indep : ∀ᵐ (a : α) ∂μα, (κ a) (t ∩ t) = (κ a) t * (κ a) t
a : α
ha : (κ a) (t ∩ t) = (κ a) t * (κ a) t
h0 : ¬(κ a) t = 0
⊢ (κ a) t = 0 ∨ (κ a) t = 1 ∨ (κ a) t = ⊤

Proof state:
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
t : Set Ω
h_indep : IndepSet t t κ μα
⊢ ∀ᵐ (a : α) ∂μα, (κ a) t = 0 ∨ (κ a) t = 1 ∨ (κ a) t = ⊤

Tactic:
specialize h_indep t t (measurableSet_generateFrom (Set.mem_singleton t))
  (measurableSet_generateFrom (Set.mem_singleton t))

Result:
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
t : Set Ω
h_indep : ∀ᵐ (a : α) ∂μα, (κ a) (t ∩ t) = (κ a) t * (κ a) t
⊢ ∀ᵐ (a : α) ∂μα, (κ a) t = 0 ∨ (κ a) t = 1 ∨ (κ a) t = ⊤

Proof state:
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
t : Set Ω
h_indep : ∀ᵐ (a : α) ∂μα, (κ a) (t ∩ t) = (κ a) t * (κ a) t
⊢ ∀ᵐ (a : α) ∂μα, (κ a) t = 0 ∨ (κ a) t = 1 ∨ (κ a) t = ⊤

Tactic:
filter_upwards [h_indep] with a ha

Result:
case h
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
t : Set Ω
h_indep : ∀ᵐ (a : α) ∂μα, (κ a) (t ∩ t) = (κ a) t * (κ a) t
a : α
ha : (κ a) (t ∩ t) = (κ a) t * (κ a) t
⊢ (κ a) t = 0 ∨ (κ a) t = 1 ∨ (κ a) t = ⊤

Proof state:
case neg
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
t : Set Ω
h_indep : ∀ᵐ (a : α) ∂μα, (κ a) (t ∩ t) = (κ a) t * (κ a) t
a : α
ha : 1 = (κ a) t
h0 : ¬(κ a) t = 0
h_top : ¬(κ a) t = ⊤
⊢ (κ a) t = 0 ∨ (κ a) t = 1 ∨ (κ a) t = ⊤

Tactic:
exact Or.inr (Or.inl ha.symm)

Result:
no goals