awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Kernel.Disintegration.Basic
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
κ : Kernel α (β × Ω)
κCond : Kernel (α × β) Ω
inst : IsFiniteKernel κ.fst
inst_1 : κ.IsCondKernel κCond
a : α
h : κ.fst ⊗ₖ κCond = κ
h_sfin : IsSFiniteKernel κCond
h_eq :
  ∀ (s : Set β) (hs : MeasurableSet s),
    ∫⁻ (b : β),
        s.indicator (fun (b : β) ↦ (((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ)
          b ∂(κ.fst : (a : α) → Measure β) a =
      (((κ.fst : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s
h_meas :
  Measurable (β := ℝ≥0∞) fun (b : β) ↦
    (((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ
r : ℝ≥0∞
hr : 1 < r
s : Set β := {b : β | r ≤ (((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ}
hs : MeasurableSet s
h_2_le :
  LE.le (α := (x : β) → ℝ≥0∞) (s.indicator fun (x : β) ↦ r)
    (s.indicator fun (b : β) ↦ (((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ)
this :
  ∫⁻ (b : β), s.indicator (fun (x : β) ↦ r) b ∂(κ.fst : (a : α) → Measure β) a ≤
    (((κ.fst : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s
⊢ HMul.hMul (β := ℝ≥0∞) r ((((κ.fst : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞) ≤
    (((κ.fst : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s

Tactic:
rw [lintegral_indicator_const hs] at this

Premises used: MeasureTheory.lintegral_indicator_const
-- Module: Mathlib.Probability.Kernel.Disintegration.Basic
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
κ : Kernel α (β × Ω)
κCond : Kernel (α × β) Ω
inst : IsFiniteKernel κ.fst
inst_1 : κ.IsCondKernel κCond
a : α
h : κ.fst ⊗ₖ κCond = κ
h_sfin : IsSFiniteKernel κCond
h_eq :
  ∀ (s : Set β) (hs : MeasurableSet s),
    ∫⁻ (b : β),
        s.indicator (fun (b : β) ↦ (((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ)
          b ∂(κ.fst : (a : α) → Measure β) a =
      (((κ.fst : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s
h_meas :
  Measurable (β := ℝ≥0∞) fun (b : β) ↦
    (((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ
r : ℝ≥0∞
hr : 1 < r
s : Set β := {b : β | r ≤ (((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ}
hs : MeasurableSet s
h_2_le :
  LE.le (α := (x : β) → ℝ≥0∞) (s.indicator fun (x : β) ↦ r)
    (s.indicator fun (b : β) ↦ (((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ)
this :
  HMul.hMul (β := ℝ≥0∞) r ((((κ.fst : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞) ≤
    (((κ.fst : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s
pos :
  ∀
    (h_ne_zero :
      Ne (α := ℝ≥0∞)
        ((((κ.fst : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞)
            {x : β | r ≤ (((κCond : (a : α × β) → Measure Ω) (a, x) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ} :
          ℝ≥0∞)
        (0 : ℝ≥0∞)),
    (((κ.fst : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s <
      HMul.hMul (β := ℝ≥0∞) r ((((κ.fst : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    ((((κ.fst : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞)
        {x : β | r ≤ (((κCond : (a : α × β) → Measure Ω) (a, x) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ} :
      ℝ≥0∞)
    (0 : ℝ≥0∞)

Tactic:
contrapose! this with h_ne_zero
-- Module: Mathlib.Probability.Kernel.Disintegration.Basic
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
κ : Kernel α (β × Ω)
κCond : Kernel (α × β) Ω
inst : IsFiniteKernel κ.fst
inst_1 : κ.IsCondKernel κCond
a : α
h : κ.fst ⊗ₖ κCond = κ
h_sfin : IsSFiniteKernel κCond
h_eq :
  ∀ (s : Set β) (hs : MeasurableSet s),
    ∫⁻ (b : β),
        s.indicator (fun (b : β) ↦ (((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ)
          b ∂(κ.fst : (a : α) → Measure β) a =
      (((κ.fst : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s
h_meas :
  Measurable (β := ℝ≥0∞) fun (b : β) ↦
    (((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ
r : ℝ≥0∞
hr : 1 < r
s : Set β := {b : β | r ≤ (((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ}
hs : MeasurableSet s
h_2_le :
  LE.le (α := (x : β) → ℝ≥0∞) (s.indicator fun (x : β) ↦ r)
    (s.indicator fun (b : β) ↦ (((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ)
h_ne_zero :
  Ne (α := ℝ≥0∞)
    ((((κ.fst : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞)
        {x : β | r ≤ (((κCond : (a : α × β) → Measure Ω) (a, x) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ} :
      ℝ≥0∞)
    (0 : ℝ≥0∞)
rw :
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞)
    ((((κ.fst : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
| (((κ.fst : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s

Tactic:
rw [← one_mul (κ.fst a s)]

Premises used: DFunLike.coe, ProbabilityTheory.Kernel.fst, one_mul
-- Module: Mathlib.Probability.Kernel.Disintegration.Basic
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
κ : Kernel α (β × Ω)
κCond : Kernel (α × β) Ω
inst : IsFiniteKernel κ.fst
inst_1 : κ.IsCondKernel κCond
a : α
h : κ.fst ⊗ₖ κCond = κ
h_sfin : IsSFiniteKernel κCond
h_eq :
  ∀ (s : Set β) (hs : MeasurableSet s),
    ∫⁻ (b : β),
        s.indicator (fun (b : β) ↦ (((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ)
          b ∂(κ.fst : (a : α) → Measure β) a =
      (((κ.fst : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s
h_meas :
  Measurable (β := ℝ≥0∞) fun (b : β) ↦
    (((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ
r : ℝ≥0∞
hr : 1 < r
s : Set β := {b : β | r ≤ (((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ}
hs : MeasurableSet s
h_2_le :
  LE.le (α := (x : β) → ℝ≥0∞) (s.indicator fun (x : β) ↦ r)
    (s.indicator fun (b : β) ↦ (((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ)
h_ne_zero :
  Ne (α := ℝ≥0∞)
    ((((κ.fst : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞)
        {x : β | r ≤ (((κCond : (a : α × β) → Measure Ω) (a, x) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ} :
      ℝ≥0∞)
    (0 : ℝ≥0∞)
pos :
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞)
      ((((κ.fst : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞) <
    HMul.hMul (β := ℝ≥0∞) r ((((κ.fst : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
⊢ (((κ.fst : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s <
    HMul.hMul (β := ℝ≥0∞) r ((((κ.fst : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
conv_lhs => rw [← one_mul (κ.fst a s)]

Premises used: DFunLike.coe, ProbabilityTheory.Kernel.fst, one_mul
-- Module: Mathlib.Probability.Kernel.Disintegration.Basic
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
κ : Kernel α (β × Ω)
κCond : Kernel (α × β) Ω
inst : IsFiniteKernel κ.fst
inst_1 : κ.IsCondKernel κCond
a : α
h : κ.fst ⊗ₖ κCond = κ
h_sfin : IsSFiniteKernel κCond
h_eq :
  ∀ (s : Set β) (hs : MeasurableSet s),
    ∫⁻ (b : β),
        s.indicator (fun (b : β) ↦ (((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ)
          b ∂(κ.fst : (a : α) → Measure β) a =
      (((κ.fst : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s
h_meas :
  Measurable (β := ℝ≥0∞) fun (b : β) ↦
    (((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ
r : ℝ≥0∞
hr : 1 < r
s : Set β := {b : β | r ≤ (((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ}
hs : MeasurableSet s
h_2_le :
  LE.le (α := (x : β) → ℝ≥0∞) (s.indicator fun (x : β) ↦ r)
    (s.indicator fun (b : β) ↦ (((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ)
h_ne_zero :
  Ne (α := ℝ≥0∞)
    ((((κ.fst : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞)
        {x : β | r ≤ (((κCond : (a : α × β) → Measure Ω) (a, x) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ} :
      ℝ≥0∞)
    (0 : ℝ≥0∞)
pos : Ne (α := ℝ≥0∞) ((((κ.fst : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞)
      ((((κ.fst : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞) <
    HMul.hMul (β := ℝ≥0∞) r ((((κ.fst : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
gcongr
-- Module: Mathlib.Probability.Kernel.Disintegration.Basic
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
κ : Kernel α (β × Ω)
κCond : Kernel (α × β) Ω
inst : IsFiniteKernel κ.fst
inst_1 : κ.IsCondKernel κCond
a : α
h : κ.fst ⊗ₖ κCond = κ
h_sfin : IsSFiniteKernel κCond
h_eq :
  ∀ (s : Set β) (hs : MeasurableSet s),
    ∫⁻ (b : β),
        s.indicator (fun (b : β) ↦ (((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ)
          b ∂(κ.fst : (a : α) → Measure β) a =
      (((κ.fst : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s
h_meas :
  Measurable (β := ℝ≥0∞) fun (b : β) ↦
    (((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ
r : ℝ≥0∞
hr : 1 < r
s : Set β := {b : β | r ≤ (((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ}
hs : MeasurableSet s
h_2_le :
  LE.le (α := (x : β) → ℝ≥0∞) (s.indicator fun (x : β) ↦ r)
    (s.indicator fun (b : β) ↦ (((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ)
h_ne_zero :
  Ne (α := ℝ≥0∞)
    ((((κ.fst : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞)
        {x : β | r ≤ (((κCond : (a : α × β) → Measure Ω) (a, x) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ} :
      ℝ≥0∞)
    (0 : ℝ≥0∞)
⊢ Ne (α := ℝ≥0∞) ((((κ.fst : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
finiteness
-- Module: Mathlib.Probability.Kernel.Disintegration.Basic
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
κ : Kernel α (β × Ω)
κCond : Kernel (α × β) Ω
inst : IsFiniteKernel κ.fst
inst_1 : κ.IsCondKernel κCond
a : α
h : κ.fst ⊗ₖ κCond = κ
h_sfin : IsSFiniteKernel κCond
h_eq :
  ∀ (s : Set β) (hs : MeasurableSet s),
    ∫⁻ (b : β),
        s.indicator (fun (b : β) ↦ (((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ)
          b ∂(κ.fst : (a : α) → Measure β) a =
      (((κ.fst : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s
h_meas :
  Measurable (β := ℝ≥0∞) fun (b : β) ↦
    (((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ
pos :
  ∀ b < 1,
    Eq (α := ℝ≥0∞)
      ((((κ.fst : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞)
          {x : β | (((κCond : (a : α × β) → Measure Ω) (a, x) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ ≤ b} :
        ℝ≥0∞)
      (0 : ℝ≥0∞)
⊢ ∀ᵐ (b : β) ∂((κ.fst : (a : α) → Measure β) a : Measure β),
    LE.le (α := ℝ≥0∞) (1 : ℝ≥0∞)
      ((((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞)

Tactic:
rw [ae_const_le_iff_forall_lt_measure_zero]

Premises used: MeasureTheory.ae_const_le_iff_forall_lt_measure_zero
-- Module: Mathlib.Probability.Kernel.Disintegration.Basic
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
κ : Kernel α (β × Ω)
κCond : Kernel (α × β) Ω
inst : IsFiniteKernel κ.fst
inst_1 : κ.IsCondKernel κCond
a : α
h : κ.fst ⊗ₖ κCond = κ
h_sfin : IsSFiniteKernel κCond
h_eq :
  ∀ (s : Set β) (hs : MeasurableSet s),
    ∫⁻ (b : β),
        s.indicator (fun (b : β) ↦ (((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ)
          b ∂(κ.fst : (a : α) → Measure β) a =
      (((κ.fst : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s
h_meas :
  Measurable (β := ℝ≥0∞) fun (b : β) ↦
    (((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ
r : ℝ≥0∞
hr : r < 1
s : Set β := {b : β | (((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ ≤ r}
⊢ MeasurableSet s

Tactic:
have hs : MeasurableSet s := h_meas measurableSet_Iic
-- Module: Mathlib.Probability.Kernel.Disintegration.Basic
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
κ : Kernel α (β × Ω)
κCond : Kernel (α × β) Ω
inst : IsFiniteKernel κ.fst
inst_1 : κ.IsCondKernel κCond
a : α
h : κ.fst ⊗ₖ κCond = κ
h_sfin : IsSFiniteKernel κCond
h_eq :
  ∀ (s : Set β) (hs : MeasurableSet s),
    ∫⁻ (b : β),
        s.indicator (fun (b : β) ↦ (((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ)
          b ∂(κ.fst : (a : α) → Measure β) a =
      (((κ.fst : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s
h_meas :
  Measurable (β := ℝ≥0∞) fun (b : β) ↦
    (((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ
r : ℝ≥0∞
hr : r < 1
s : Set β := {b : β | (((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ ≤ r}
hs : MeasurableSet s
b : β
pos :
  ∀ (hbs : b ∈ s),
    LE.le (α := (fun (x : β) ↦ ℝ≥0∞) b)
      (s.indicator (fun (b : β) ↦ (((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ) b)
      (s.indicator (fun (x : β) ↦ r) b)
neg :
  ∀ (hbs : b ∉ s),
    LE.le (α := (fun (x : β) ↦ ℝ≥0∞) b)
      (s.indicator (fun (b : β) ↦ (((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ) b)
      (s.indicator (fun (x : β) ↦ r) b)
⊢ LE.le (α := (fun (x : β) ↦ ℝ≥0∞) b)
    (s.indicator (fun (b : β) ↦ (((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ) b)
    (s.indicator (fun (x : β) ↦ r) b)

Tactic:
by_cases hbs : b ∈ s
-- Module: Mathlib.Probability.Kernel.Disintegration.Basic
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
κ : Kernel α (β × Ω)
κCond : Kernel (α × β) Ω
inst : IsFiniteKernel κ.fst
inst_1 : κ.IsCondKernel κCond
a : α
h : κ.fst ⊗ₖ κCond = κ
h_sfin : IsSFiniteKernel κCond
h_eq :
  ∀ (s : Set β) (hs : MeasurableSet s),
    ∫⁻ (b : β),
        s.indicator (fun (b : β) ↦ (((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ)
          b ∂(κ.fst : (a : α) → Measure β) a =
      (((κ.fst : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s
h_meas :
  Measurable (β := ℝ≥0∞) fun (b : β) ↦
    (((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ
r : ℝ≥0∞
hr : r < 1
s : Set β := {b : β | (((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ ≤ r}
hs : MeasurableSet s
b : β
hbs : b ∈ s
⊢ LE.le (α := (fun (x : β) ↦ ℝ≥0∞) b)
    (s.indicator (fun (b : β) ↦ (((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ) b)
    (s.indicator (fun (x : β) ↦ r) b)

Tactic:
simpa [hbs]
-- Module: Mathlib.Probability.Kernel.Disintegration.Basic
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
κ : Kernel α (β × Ω)
κCond : Kernel (α × β) Ω
inst : IsFiniteKernel κ.fst
inst_1 : κ.IsCondKernel κCond
a : α
h : κ.fst ⊗ₖ κCond = κ
h_sfin : IsSFiniteKernel κCond
h_eq :
  ∀ (s : Set β) (hs : MeasurableSet s),
    ∫⁻ (b : β),
        s.indicator (fun (b : β) ↦ (((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ)
          b ∂(κ.fst : (a : α) → Measure β) a =
      (((κ.fst : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s
h_meas :
  Measurable (β := ℝ≥0∞) fun (b : β) ↦
    (((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ
r : ℝ≥0∞
hr : r < 1
s : Set β := {b : β | (((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ ≤ r}
hs : MeasurableSet s
b : β
hbs : b ∉ s
⊢ LE.le (α := (fun (x : β) ↦ ℝ≥0∞) b)
    (s.indicator (fun (b : β) ↦ (((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ) b)
    (s.indicator (fun (x : β) ↦ r) b)

Tactic:
simp [hbs]
-- Module: Mathlib.Probability.Kernel.Disintegration.Basic
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
κ : Kernel α (β × Ω)
κCond : Kernel (α × β) Ω
inst : IsFiniteKernel κ.fst
inst_1 : κ.IsCondKernel κCond
a : α
h : κ.fst ⊗ₖ κCond = κ
h_sfin : IsSFiniteKernel κCond
h_eq :
  ∀ (s : Set β) (hs : MeasurableSet s),
    ∫⁻ (b : β),
        s.indicator (fun (b : β) ↦ (((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ)
          b ∂(κ.fst : (a : α) → Measure β) a =
      (((κ.fst : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s
h_meas :
  Measurable (β := ℝ≥0∞) fun (b : β) ↦
    (((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ
r : ℝ≥0∞
hr : r < 1
s : Set β := {b : β | (((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ ≤ r}
hs : MeasurableSet s
⊢ LE.le (α := (x : β) → ℝ≥0∞)
    (s.indicator fun (b : β) ↦ (((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ)
    (s.indicator fun (x : β) ↦ r)

Tactic:
have h_2_le : s.indicator (fun b ↦ (κCond (a, b)) Set.univ) ≤ s.indicator (fun _ ↦ r) := by
      intro b
      by_cases hbs : b ∈ s
      · simpa [hbs]
      · simp [hbs]
-- Module: Mathlib.Probability.Kernel.Disintegration.Basic
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
κ : Kernel α (β × Ω)
κCond : Kernel (α × β) Ω
inst : IsFiniteKernel κ.fst
inst_1 : κ.IsCondKernel κCond
a : α
h : κ.fst ⊗ₖ κCond = κ
h_sfin : IsSFiniteKernel κCond
h_eq :
  ∀ (s : Set β) (hs : MeasurableSet s),
    ∫⁻ (b : β),
        s.indicator (fun (b : β) ↦ (((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ)
          b ∂(κ.fst : (a : α) → Measure β) a =
      (((κ.fst : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s
h_meas :
  Measurable (β := ℝ≥0∞) fun (b : β) ↦
    (((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ
r : ℝ≥0∞
hr : r < 1
s : Set β := {b : β | (((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ ≤ r}
hs : MeasurableSet s
h_2_le :
  LE.le (α := (x : β) → ℝ≥0∞)
    (s.indicator fun (b : β) ↦ (((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ)
    (s.indicator fun (x : β) ↦ r)
⊢ (((κ.fst : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s ≤
    ∫⁻ (b : β), s.indicator (fun (x : β) ↦ r) b ∂(κ.fst : (a : α) → Measure β) a

Tactic:
have : κ.fst a s ≤ ∫⁻ b, s.indicator (fun _ ↦ r) b ∂(κ.fst a) :=
      (h_eq s hs).symm.trans_le (lintegral_mono h_2_le)
-- Module: Mathlib.Probability.Kernel.Disintegration.Basic
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
κ : Kernel α (β × Ω)
κCond : Kernel (α × β) Ω
inst : IsFiniteKernel κ.fst
inst_1 : κ.IsCondKernel κCond
a : α
h : κ.fst ⊗ₖ κCond = κ
h_sfin : IsSFiniteKernel κCond
h_eq :
  ∀ (s : Set β) (hs : MeasurableSet s),
    ∫⁻ (b : β),
        s.indicator (fun (b : β) ↦ (((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ)
          b ∂(κ.fst : (a : α) → Measure β) a =
      (((κ.fst : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s
h_meas :
  Measurable (β := ℝ≥0∞) fun (b : β) ↦
    (((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ
r : ℝ≥0∞
hr : r < 1
s : Set β := {b : β | (((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ ≤ r}
hs : MeasurableSet s
h_2_le :
  LE.le (α := (x : β) → ℝ≥0∞)
    (s.indicator fun (b : β) ↦ (((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ)
    (s.indicator fun (x : β) ↦ r)
this :
  (((κ.fst : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s ≤
    ∫⁻ (b : β), s.indicator (fun (x : β) ↦ r) b ∂(κ.fst : (a : α) → Measure β) a
⊢ (((κ.fst : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s ≤
    HMul.hMul (β := ℝ≥0∞) r ((((κ.fst : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [lintegral_indicator_const hs] at this

Premises used: MeasureTheory.lintegral_indicator_const
-- Module: Mathlib.Probability.Kernel.Disintegration.Basic
Goal:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
κ : Kernel α (β × Ω)
κCond : Kernel (α × β) Ω
inst : IsFiniteKernel κ.fst
inst_1 : κ.IsCondKernel κCond
a : α
h : κ.fst ⊗ₖ κCond = κ
h_sfin : IsSFiniteKernel κCond
h_eq :
  ∀ (s : Set β) (hs : MeasurableSet s),
    ∫⁻ (b : β),
        s.indicator (fun (b : β) ↦ (((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ)
          b ∂(κ.fst : (a : α) → Measure β) a =
      (((κ.fst : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s
h_meas :
  Measurable (β := ℝ≥0∞) fun (b : β) ↦
    (((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ
r : ℝ≥0∞
hr : r < 1
s : Set β := {b : β | (((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ ≤ r}
hs : MeasurableSet s
h_2_le :
  LE.le (α := (x : β) → ℝ≥0∞)
    (s.indicator fun (b : β) ↦ (((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ)
    (s.indicator fun (x : β) ↦ r)
this :
  (((κ.fst : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s ≤
    HMul.hMul (β := ℝ≥0∞) r ((((κ.fst : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
pos :
  ∀
    (h_ne_zero :
      Ne (α := ℝ≥0∞)
        ((((κ.fst : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞)
            {x : β | (((κCond : (a : α × β) → Measure Ω) (a, x) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ ≤ r} :
          ℝ≥0∞)
        (0 : ℝ≥0∞)),
    HMul.hMul (β := ℝ≥0∞) r ((((κ.fst : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞) <
      (((κ.fst : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s
⊢ Eq (α := ℝ≥0∞)
    ((((κ.fst : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞)
        {x : β | (((κCond : (a : α × β) → Measure Ω) (a, x) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ ≤ r} :
      ℝ≥0∞)
    (0 : ℝ≥0∞)

Tactic:
contrapose! this with h_ne_zero