awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Basic (hypothesis)
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
⊢ (∀ᵐ (b : β) ∂((κ.fst : (a : α) → Measure β) a : Measure β),
      LE.le (α := ℝ≥0∞) ((((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞)
        (1 : ℝ≥0∞)) ∧
    ∀ᵐ (b : β) ∂((κ.fst : (a : α) → Measure β) a : Measure β),
      LE.le (α := ℝ≥0∞) (1 : ℝ≥0∞)
        ((((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞)
have 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
Tactic: have h_eq s (hs : MeasurableSet s) :
      ∫⁻ b, s.indicator (fun b ↦ κCond (a, b) Set.univ) b ∂κ.fst a = κ.fst a s := by
    conv_rhs => rw [← h]
    rw [fst_compProd_apply _ _ _ hs]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Basic (hypothesis)
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
⊢ (∀ᵐ (b : β) ∂((κ.fst : (a : α) → Measure β) a : Measure β),
      LE.le (α := ℝ≥0∞) ((((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞)
        (1 : ℝ≥0∞)) ∧
    ∀ᵐ (b : β) ∂((κ.fst : (a : α) → Measure β) a : Measure β),
      LE.le (α := ℝ≥0∞) (1 : ℝ≥0∞)
        ((((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞)
have h_meas : Measurable (β := ℝ≥0∞) fun (b : β) ↦ (((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ
Tactic: have h_meas : Measurable fun b ↦ κCond (a, b) Set.univ :=
    (κCond.measurable_coe MeasurableSet.univ).comp measurable_prodMk_left
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Basic (goal)
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
⊢ (∀ᵐ (b : β) ∂((κ.fst : (a : α) → Measure β) a : Measure β),
      LE.le (α := ℝ≥0∞) ((((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞)
        (1 : ℝ≥0∞)) ∧
    ∀ᵐ (b : β) ∂((κ.fst : (a : α) → Measure β) a : Measure β),
      LE.le (α := ℝ≥0∞) (1 : ℝ≥0∞)
        ((((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞)
have pos : ∀ᵐ (b : β) ∂((κ.fst : (a : α) → Measure β) a : Measure β),
  LE.le (α := ℝ≥0∞) ((((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞)
    (1 : ℝ≥0∞)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Basic (goal)
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 : β) ∂((κ.fst : (a : α) → Measure β) a : Measure β),
    LE.le (α := ℝ≥0∞) ((((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞)
      (1 : ℝ≥0∞)
⊢ (∀ᵐ (b : β) ∂((κ.fst : (a : α) → Measure β) a : Measure β),
      LE.le (α := ℝ≥0∞) ((((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞)
        (1 : ℝ≥0∞)) ∧
    ∀ᵐ (b : β) ∂((κ.fst : (a : α) → Measure β) a : Measure β),
      LE.le (α := ℝ≥0∞) (1 : ℝ≥0∞)
        ((((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞)
have pos₁ : ∀ᵐ (b : β) ∂((κ.fst : (a : α) → Measure β) a : Measure β),
  LE.le (α := ℝ≥0∞) (1 : ℝ≥0∞)
    ((((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Basic (goal)
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
⊢ ∀ᵐ (b : β) ∂((κ.fst : (a : α) → Measure β) a : Measure β),
    LE.le (α := ℝ≥0∞) ((((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞)
      (1 : ℝ≥0∞)
have pos : ∀ (b : ℝ≥0∞),
  1 < b →
    Eq (α := ℝ≥0∞)
      ((((κ.fst : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞)
          {x : β | b ≤ (((κCond : (a : α × β) → Measure Ω) (a, x) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ} :
        ℝ≥0∞)
      (0 : ℝ≥0∞)
Tactic: rw [ae_le_const_iff_forall_gt_measure_zero]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Basic (hypothesis)
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}
⊢ 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∞)
have hs : MeasurableSet s
Tactic: have hs : MeasurableSet s := h_meas measurableSet_Ici
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Basic (goal)
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
b : β
⊢ LE.le (α := (fun (x : β) ↦ ℝ≥0∞) b) (s.indicator (fun (x : β) ↦ r) b)
    (s.indicator (fun (b : β) ↦ (((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ) b)
have pos : ∀ (hbs : b ∈ s),
  LE.le (α := (fun (x : β) ↦ ℝ≥0∞) b) (s.indicator (fun (x : β) ↦ r) b)
    (s.indicator (fun (b : β) ↦ (((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ) b)
Tactic: by_cases hbs : b ∈ s
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Basic (goal)
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
b : β
pos :
  ∀ (hbs : b ∈ s),
    LE.le (α := (fun (x : β) ↦ ℝ≥0∞) b) (s.indicator (fun (x : β) ↦ r) b)
      (s.indicator (fun (b : β) ↦ (((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ) b)
⊢ LE.le (α := (fun (x : β) ↦ ℝ≥0∞) b) (s.indicator (fun (x : β) ↦ r) b)
    (s.indicator (fun (b : β) ↦ (((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ) b)
have neg : ∀ (hbs : b ∉ s),
  LE.le (α := (fun (x : β) ↦ ℝ≥0∞) b) (s.indicator (fun (x : β) ↦ r) b)
    (s.indicator (fun (b : β) ↦ (((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ) b)
Tactic: by_cases hbs : b ∈ s
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Basic (hypothesis)
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
⊢ 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∞)
have 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)
Tactic: have h_2_le : s.indicator (fun _ ↦ r) ≤ s.indicator (fun b ↦ (κCond (a, b)) Set.univ) := by
      intro b
      by_cases hbs : b ∈ s
      · simpa [hbs]
      · simp [hbs]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Basic (hypothesis)
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)
⊢ 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∞)
have this : ∫⁻ (b : β), s.indicator (fun (x : β) ↦ r) b ∂(κ.fst : (a : α) → Measure β) a ≤
  (((κ.fst : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s
Tactic: have : ∫⁻ b, s.indicator (fun _ ↦ r) b ∂(κ.fst a) ≤ κ.fst a s :=
      (lintegral_mono h_2_le).trans_eq (h_eq s hs)
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Basic (hypothesis)
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
⊢ 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∞)
have this₁ : 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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Basic (goal)
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
⊢ 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∞)
have 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∞)
Tactic: contrapose! this with h_ne_zero
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Basic (goal)
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∞)
| (((κ.fst : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s
have rw : HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞)
  ((((κ.fst : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [← one_mul (κ.fst a s)]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Basic (goal)
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∞)
⊢ (((κ.fst : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s <
    HMul.hMul (β := ℝ≥0∞) r ((((κ.fst : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
have 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∞)
Tactic: conv_lhs => rw [← one_mul (κ.fst a s)]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.Basic (goal)
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∞)
⊢ 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∞)
have pos : Ne (α := ℝ≥0∞) ((((κ.fst : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: gcongr