-- Mathlib/Probability/Kernel/Disintegration/Basic.lean
/-- A conditional kernel is almost everywhere a probability measure. -/
lemma IsCondKernel.isProbabilityMeasure_ae [IsFiniteKernel κ.fst] [κ.IsCondKernel κCond] (a : α) :
    ∀ᵐ b ∂(κ.fst a), IsProbabilityMeasure (κCond (a, b))

Proof state:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
κ : Kernel α (β × Ω)
κCond : Kernel (α × β) Ω
inst✝¹ : IsFiniteKernel κ.fst
inst✝ : κ.IsCondKernel κCond
a : α
h : κ.fst ⊗ₖ κCond = κ
h_sfin : IsSFiniteKernel κCond
s : Set β
hs : MeasurableSet s
⊢ ∫⁻ (b : β), s.indicator (fun b => (κCond (a, b)) univ) b ∂κ.fst a = (κ.fst a) s

Tactic:
conv_rhs => rw [← h]

Result:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
κ : Kernel α (β × Ω)
κCond : Kernel (α × β) Ω
inst✝¹ : IsFiniteKernel κ.fst
inst✝ : κ.IsCondKernel κCond
a : α
h : κ.fst ⊗ₖ κCond = κ
h_sfin : IsSFiniteKernel κCond
s : Set β
hs : MeasurableSet s
⊢ ∫⁻ (b : β), s.indicator (fun b => (κCond (a, b)) univ) b ∂κ.fst a = ((κ.fst ⊗ₖ κCond).fst a) s

Proof state:
case pos.left
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
κ : Kernel α (β × Ω)
κCond : Kernel (α × β) Ω
inst✝¹ : IsFiniteKernel κ.fst
inst✝ : κ.IsCondKernel κCond
a : α
h : κ.fst ⊗ₖ κCond = κ
h_sfin : IsSFiniteKernel κCond
h_eq : ∀ (s : Set β), MeasurableSet s → ∫⁻ (b : β), s.indicator (fun b => (κCond (a, b)) univ) b ∂κ.fst a = (κ.fst a) s
h_meas : Measurable fun b => (κCond (a, b)) univ
r : ℝ≥0∞
hr : 1 < r
s : Set β := {b | r ≤ (κCond (a, b)) univ}
hs : MeasurableSet s
h_2_le : (s.indicator fun x => r) ≤ s.indicator fun b => (κCond (a, b)) univ
this : ¬(κ.fst a) s < r * (κ.fst a) s
h_ne_zero : ¬(κ.fst a) {x | r ≤ (κCond (a, x)) univ} = 0
⊢ False

Tactic:
refine this ?_

Result:
case pos.left
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
κ : Kernel α (β × Ω)
κCond : Kernel (α × β) Ω
inst✝¹ : IsFiniteKernel κ.fst
inst✝ : κ.IsCondKernel κCond
a : α
h : κ.fst ⊗ₖ κCond = κ
h_sfin : IsSFiniteKernel κCond
h_eq : ∀ (s : Set β), MeasurableSet s → ∫⁻ (b : β), s.indicator (fun b => (κCond (a, b)) univ) b ∂κ.fst a = (κ.fst a) s
h_meas : Measurable fun b => (κCond (a, b)) univ
r : ℝ≥0∞
hr : 1 < r
s : Set β := {b | r ≤ (κCond (a, b)) univ}
hs : MeasurableSet s
h_2_le : (s.indicator fun x => r) ≤ s.indicator fun b => (κCond (a, b)) univ
this : ¬(κ.fst a) s < r * (κ.fst a) s
h_ne_zero : ¬(κ.fst a) {x | r ≤ (κCond (a, x)) univ} = 0
⊢ (κ.fst a) s < r * (κ.fst a) s

Proof state:
case pos.right
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
κ : Kernel α (β × Ω)
κCond : Kernel (α × β) Ω
inst✝¹ : IsFiniteKernel κ.fst
inst✝ : κ.IsCondKernel κCond
a : α
h : κ.fst ⊗ₖ κCond = κ
h_sfin : IsSFiniteKernel κCond
h_eq : ∀ (s : Set β), MeasurableSet s → ∫⁻ (b : β), s.indicator (fun b => (κCond (a, b)) univ) b ∂κ.fst a = (κ.fst a) s
h_meas : Measurable fun b => (κCond (a, b)) univ
r : ℝ≥0∞
hr : r < 1
s : Set β := {b | (κCond (a, b)) univ ≤ r}
⊢ (κ.fst a) {x | (κCond (a, x)) univ ≤ r} = 0

Tactic:
have hs : MeasurableSet s := h_meas measurableSet_Iic

Result:
case pos.right
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
κ : Kernel α (β × Ω)
κCond : Kernel (α × β) Ω
inst✝¹ : IsFiniteKernel κ.fst
inst✝ : κ.IsCondKernel κCond
a : α
h : κ.fst ⊗ₖ κCond = κ
h_sfin : IsSFiniteKernel κCond
h_eq : ∀ (s : Set β), MeasurableSet s → ∫⁻ (b : β), s.indicator (fun b => (κCond (a, b)) univ) b ∂κ.fst a = (κ.fst a) s
h_meas : Measurable fun b => (κCond (a, b)) univ
r : ℝ≥0∞
hr : r < 1
s : Set β := {b | (κCond (a, b)) univ ≤ r}
hs : MeasurableSet s
⊢ (κ.fst a) {x | (κCond (a, x)) univ ≤ r} = 0

Proof state:
case pos.right
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
κ : Kernel α (β × Ω)
κCond : Kernel (α × β) Ω
inst✝¹ : IsFiniteKernel κ.fst
inst✝ : κ.IsCondKernel κCond
a : α
h : κ.fst ⊗ₖ κCond = κ
h_sfin : IsSFiniteKernel κCond
h_eq : ∀ (s : Set β), MeasurableSet s → ∫⁻ (b : β), s.indicator (fun b => (κCond (a, b)) univ) b ∂κ.fst a = (κ.fst a) s
h_meas : Measurable fun b => (κCond (a, b)) univ
r : ℝ≥0∞
hr : r < 1
s : Set β := {b | (κCond (a, b)) univ ≤ r}
hs : MeasurableSet s
h_2_le : (s.indicator fun b => (κCond (a, b)) univ) ≤ s.indicator fun x => r
this : (κ.fst a) s ≤ r * (κ.fst a) s
h_ne_zero : ¬(κ.fst a) {x | (κCond (a, x)) univ ≤ r} = 0
⊢ False

Tactic:
rw [← not_lt] at this

Result:
case pos.right
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
κ : Kernel α (β × Ω)
κCond : Kernel (α × β) Ω
inst✝¹ : IsFiniteKernel κ.fst
inst✝ : κ.IsCondKernel κCond
a : α
h : κ.fst ⊗ₖ κCond = κ
h_sfin : IsSFiniteKernel κCond
h_eq : ∀ (s : Set β), MeasurableSet s → ∫⁻ (b : β), s.indicator (fun b => (κCond (a, b)) univ) b ∂κ.fst a = (κ.fst a) s
h_meas : Measurable fun b => (κCond (a, b)) univ
r : ℝ≥0∞
hr : r < 1
s : Set β := {b | (κCond (a, b)) univ ≤ r}
hs : MeasurableSet s
h_2_le : (s.indicator fun b => (κCond (a, b)) univ) ≤ s.indicator fun x => r
this : ¬r * (κ.fst a) s < (κ.fst a) s
h_ne_zero : ¬(κ.fst a) {x | (κCond (a, x)) univ ≤ r} = 0
⊢ False

Proof state:
case h.e'_2.h.a
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
κ : Kernel α (β × Ω)
κCond : Kernel (α × β) Ω
inst✝¹ : IsFiniteKernel κ.fst
inst✝ : κ.IsCondKernel κCond
a : α
h : κ.fst ⊗ₖ κCond = κ
h_sfin : IsSFiniteKernel κCond
this : ∀ᵐ (b : β) ∂κ.fst a, (κCond (a, b)) univ = 1
b : β
⊢ IsProbabilityMeasure (κCond (a, b)) ↔ (κCond (a, b)) univ = 1

Tactic:
exact ⟨fun _ ↦ measure_univ, fun h ↦ ⟨h⟩⟩

Result:
no goals

Proof state:
case pos.left
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
κ : Kernel α (β × Ω)
κCond : Kernel (α × β) Ω
inst✝¹ : IsFiniteKernel κ.fst
inst✝ : κ.IsCondKernel κCond
a : α
h : κ.fst ⊗ₖ κCond = κ
h_sfin : IsSFiniteKernel κCond
h_eq : ∀ (s : Set β), MeasurableSet s → ∫⁻ (b : β), s.indicator (fun b => (κCond (a, b)) univ) b ∂κ.fst a = (κ.fst a) s
h_meas : Measurable fun b => (κCond (a, b)) univ
r : ℝ≥0∞
hr : 1 < r
s : Set β := {b | r ≤ (κCond (a, b)) univ}
hs : MeasurableSet s
h_2_le : (s.indicator fun x => r) ≤ s.indicator fun b => (κCond (a, b)) univ
⊢ (κ.fst a) {x | r ≤ (κCond (a, x)) univ} = 0

Tactic:
have : ∫⁻ b, s.indicator (fun _ ↦ r) b ∂(κ.fst a) ≤ κ.fst a s :=
  (lintegral_mono h_2_le).trans_eq (h_eq s hs)

Result:
case pos.left
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
κ : Kernel α (β × Ω)
κCond : Kernel (α × β) Ω
inst✝¹ : IsFiniteKernel κ.fst
inst✝ : κ.IsCondKernel κCond
a : α
h : κ.fst ⊗ₖ κCond = κ
h_sfin : IsSFiniteKernel κCond
h_eq : ∀ (s : Set β), MeasurableSet s → ∫⁻ (b : β), s.indicator (fun b => (κCond (a, b)) univ) b ∂κ.fst a = (κ.fst a) s
h_meas : Measurable fun b => (κCond (a, b)) univ
r : ℝ≥0∞
hr : 1 < r
s : Set β := {b | r ≤ (κCond (a, b)) univ}
hs : MeasurableSet s
h_2_le : (s.indicator fun x => r) ≤ s.indicator fun b => (κCond (a, b)) univ
this : ∫⁻ (b : β), s.indicator (fun x => r) b ∂κ.fst a ≤ (κ.fst a) s
⊢ (κ.fst a) {x | r ≤ (κCond (a, x)) univ} = 0