-- Mathlib/Probability/Independence/Kernel.lean
theorem indep_bot_right (m' : MeasurableSpace Ω) {_mΩ : MeasurableSpace Ω}
    {κ : Kernel α Ω} {μ : Measure α} [IsZeroOrMarkovKernel κ] :
    Indep m' ⊥ κ μ

Proof state:
case inl
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m' _mΩ : MeasurableSpace Ω
μ : Measure α
s t : Set Ω
a✝ : s ∈ {s | MeasurableSet s}
ht : t = ∅ ∨ t = univ
inst✝ : IsZeroOrMarkovKernel 0
⊢ ∀ᵐ (a : α) ∂μ, (0 a) (s ∩ t) = (0 a) s * (0 a) t

Tactic:
simp

Result:
no goals

Proof state:
case inr
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m' _mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst✝ : IsZeroOrMarkovKernel κ
s t : Set Ω
a✝ : s ∈ {s | MeasurableSet s}
ht : t = ∅ ∨ t = univ
h : IsMarkovKernel κ
a : α
⊢ (κ a) (s ∩ t) = (κ a) s * (κ a) t

Tactic:
rcases ht with ht | ht

Result:
case inr.inl
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m' _mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst✝ : IsZeroOrMarkovKernel κ
s t : Set Ω
a✝ : s ∈ {s | MeasurableSet s}
h : IsMarkovKernel κ
a : α
ht : t = ∅
⊢ (κ a) (s ∩ t) = (κ a) s * (κ a) t

case inr.inr
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m' _mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst✝ : IsZeroOrMarkovKernel κ
s t : Set Ω
a✝ : s ∈ {s | MeasurableSet s}
h : IsMarkovKernel κ
a : α
ht : t = univ
⊢ (κ a) (s ∩ t) = (κ a) s * (κ a) t

Proof state:
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m' _mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst✝ : IsZeroOrMarkovKernel κ
⊢ Indep m' ⊥ κ μ

Tactic:
intros s t _ ht

Result:
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m' _mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst✝ : IsZeroOrMarkovKernel κ
s t : Set Ω
a✝ : s ∈ {s | MeasurableSet s}
ht : t ∈ {s | MeasurableSet s}
⊢ ∀ᵐ (a : α) ∂μ, (κ a) (s ∩ t) = (κ a) s * (κ a) t

Proof state:
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m' _mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst✝ : IsZeroOrMarkovKernel κ
s t : Set Ω
a✝ : s ∈ {s | MeasurableSet s}
ht : t = ∅ ∨ t = univ
⊢ ∀ᵐ (a : α) ∂μ, (κ a) (s ∩ t) = (κ a) s * (κ a) t

Tactic:
rcases eq_zero_or_isMarkovKernel κ with rfl| h

Result:
case inl
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m' _mΩ : MeasurableSpace Ω
μ : Measure α
s t : Set Ω
a✝ : s ∈ {s | MeasurableSet s}
ht : t = ∅ ∨ t = univ
inst✝ : IsZeroOrMarkovKernel 0
⊢ ∀ᵐ (a : α) ∂μ, (0 a) (s ∩ t) = (0 a) s * (0 a) t

case inr
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m' _mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst✝ : IsZeroOrMarkovKernel κ
s t : Set Ω
a✝ : s ∈ {s | MeasurableSet s}
ht : t = ∅ ∨ t = univ
h : IsMarkovKernel κ
⊢ ∀ᵐ (a : α) ∂μ, (κ a) (s ∩ t) = (κ a) s * (κ a) t

Proof state:
case inr
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m' _mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst✝ : IsZeroOrMarkovKernel κ
s t : Set Ω
a✝ : s ∈ {s | MeasurableSet s}
ht : t = ∅ ∨ t = univ
h : IsMarkovKernel κ
⊢ ∀ᵐ (a : α) ∂μ, (κ a) (s ∩ t) = (κ a) s * (κ a) t

Tactic:
refine Filter.Eventually.of_forall (fun a ↦ ?_)

Result:
case inr
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m' _mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst✝ : IsZeroOrMarkovKernel κ
s t : Set Ω
a✝ : s ∈ {s | MeasurableSet s}
ht : t = ∅ ∨ t = univ
h : IsMarkovKernel κ
a : α
⊢ (κ a) (s ∩ t) = (κ a) s * (κ a) t

Proof state:
case inr.inr
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m' _mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst✝ : IsZeroOrMarkovKernel κ
s t : Set Ω
a✝ : s ∈ {s | MeasurableSet s}
h : IsMarkovKernel κ
a : α
ht : t = univ
⊢ (κ a) (s ∩ t) = (κ a) s * (κ a) t

Tactic:
rw [ht, Set.inter_univ, measure_univ, mul_one]

Result:
no goals

Proof state:
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m' _mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst✝ : IsZeroOrMarkovKernel κ
s t : Set Ω
a✝ : s ∈ {s | MeasurableSet s}
ht : t ∈ {s | MeasurableSet s}
⊢ ∀ᵐ (a : α) ∂μ, (κ a) (s ∩ t) = (κ a) s * (κ a) t

Tactic:
rw [Set.mem_setOf_eq, MeasurableSpace.measurableSet_bot_iff] at ht

Result:
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m' _mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst✝ : IsZeroOrMarkovKernel κ
s t : Set Ω
a✝ : s ∈ {s | MeasurableSet s}
ht : t = ∅ ∨ t = univ
⊢ ∀ᵐ (a : α) ∂μ, (κ a) (s ∩ t) = (κ a) s * (κ a) t

Proof state:
case inr.inl
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m' _mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst✝ : IsZeroOrMarkovKernel κ
s t : Set Ω
a✝ : s ∈ {s | MeasurableSet s}
h : IsMarkovKernel κ
a : α
ht : t = ∅
⊢ (κ a) (s ∩ t) = (κ a) s * (κ a) t

Tactic:
rw [ht, Set.inter_empty, measure_empty, mul_zero]

Result:
no goals