awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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∞) (1 : ℝ≥0∞)
      ((((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞)
have 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∞)
Tactic: rw [ae_const_le_iff_forall_lt_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 : r < 1
s : Set β := {b : β | (((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ ≤ r}
⊢ 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∞)
have hs : MeasurableSet s
Tactic: have hs : MeasurableSet s := h_meas measurableSet_Iic
-- 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 : r < 1
s : Set β := {b : β | (((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ ≤ r}
hs : MeasurableSet s
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)
have 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)
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 : 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)
⊢ 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)
have 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)
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 : r < 1
s : Set β := {b : β | (((κCond : (a : α × β) → Measure Ω) (a, b) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) univ ≤ r}
hs : MeasurableSet 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∞)
have 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)
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]
-- 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 : 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)
⊢ 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∞)
have this : (((κ.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)
-- 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 : 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
⊢ 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∞)
have this₁ : (((κ.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
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 : 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∞)
⊢ 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∞)
have 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
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 : 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)
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∞)
| (((κ.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 : 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)
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
have pos : HMul.hMul (β := ℝ≥0∞) r ((((κ.fst : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞) <
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞)
    ((((κ.fst : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: conv_rhs => 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 : 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)
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∞) <
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞)
      ((((κ.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
-- 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_1 : Kernel (α × β) Ω
inst : Countable α
κCond : α → Kernel β Ω
h_atom : ∀ (x y : α), x ∈ measurableAtom y → κCond x = κCond y
⊢ Measurable (β := Measure Ω) fun (p : α × β) ↦ (κCond p.1 : (a : β) → Measure Ω) p.2
have refine : ∀ (x y : α) (hx : β) (hy : y ∈ measurableAtom x),
  Eq.{u_3 + 1} (α := Measure Ω) ((κCond (y, hx).1 : (a : β) → Measure Ω) (y, hx).2 : Measure Ω)
    ((κCond (x, hx).1 : (a : β) → Measure Ω) (x, hx).2 : Measure Ω)
Tactic: refine measurable_from_prod_countable_right' (fun a ↦ (κCond a).measurable) fun x y hx hy ↦ ?_
-- 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 Ω
κ_1 : Kernel α (β × Ω)
κCond_1 : Kernel (α × β) Ω
inst : Countable α
κCond : α → Kernel β Ω
inst_1 : ∀ (a : α), IsMarkovKernel (κCond a)
h_atom : ∀ (x y : α), x ∈ measurableAtom y → κCond x = κCond y
κ : Kernel α (β × Ω)
inst_2 : IsSFiniteKernel κ
inst_3 : ∀ (a : α), Measure.IsCondKernel ((κ : (a : α) → Measure (β × Ω)) a) (κCond a)
⊢ κ.IsCondKernel (condKernelCountable κCond h_atom)
have disintegrate : κ.fst ⊗ₖ condKernelCountable κCond h_atom = κ
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 Ω
κ_1 : Kernel α (β × Ω)
κCond_1 : Kernel (α × β) Ω
inst : Countable α
κCond : α → Kernel β Ω
inst_1 : ∀ (a : α), IsMarkovKernel (κCond a)
h_atom : ∀ (x y : α), x ∈ measurableAtom y → κCond x = κCond y
κ : Kernel α (β × Ω)
inst_2 : IsSFiniteKernel κ
inst_3 : ∀ (a : α), Measure.IsCondKernel ((κ : (a : α) → Measure (β × Ω)) a) (κCond a)
⊢ κ.fst ⊗ₖ condKernelCountable κCond h_atom = κ
have disintegrate : ∀ (a : α) (s : Set (β × Ω)) (hs : MeasurableSet s),
  Eq (α := ℝ≥0∞)
    ((((κ.fst ⊗ₖ condKernelCountable κCond h_atom : (a : α) → Measure (β × Ω)) a : Measure (β × Ω)) :
          (a : Set (β × Ω)) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    ((((κ : (a : α) → Measure (β × Ω)) a : Measure (β × Ω)) : (a : Set (β × Ω)) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext a s hs
-- 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 Ω
κ_1 : Kernel α (β × Ω)
κCond_1 : Kernel (α × β) Ω
inst : Countable α
κCond : α → Kernel β Ω
inst_1 : ∀ (a : α), IsMarkovKernel (κCond a)
h_atom : ∀ (x y : α), x ∈ measurableAtom y → κCond x = κCond y
κ : Kernel α (β × Ω)
inst_2 : IsSFiniteKernel κ
inst_3 : ∀ (a : α), Measure.IsCondKernel ((κ : (a : α) → Measure (β × Ω)) a) (κCond a)
a : α
s : Set (β × Ω)
hs : MeasurableSet s
| ((((κ : (a : α) → Measure (β × Ω)) a : Measure (β × Ω)) : (a : Set (β × Ω)) → ℝ≥0∞) s : ℝ≥0∞)
have rw : ((Measure.fst.{u_2, u_3} (β := Ω) ((κ : (a : α) → Measure (β × Ω)) a) ⊗ₘ κCond a : (a : Set (β × Ω)) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [← (κ a).disintegrate (κCond a)]
-- 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 Ω
κ_1 : Kernel α (β × Ω)
κCond_1 : Kernel (α × β) Ω
inst : Countable α
κCond : α → Kernel β Ω
inst_1 : ∀ (a : α), IsMarkovKernel (κCond a)
h_atom : ∀ (x y : α), x ∈ measurableAtom y → κCond x = κCond y
κ : Kernel α (β × Ω)
inst_2 : IsSFiniteKernel κ
inst_3 : ∀ (a : α), Measure.IsCondKernel ((κ : (a : α) → Measure (β × Ω)) a) (κCond a)
a : α
s : Set (β × Ω)
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞)
    ((((κ.fst ⊗ₖ condKernelCountable κCond h_atom : (a : α) → Measure (β × Ω)) a : Measure (β × Ω)) :
          (a : Set (β × Ω)) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    ((((κ : (a : α) → Measure (β × Ω)) a : Measure (β × Ω)) : (a : Set (β × Ω)) → ℝ≥0∞) s : ℝ≥0∞)
have disintegrate : Eq (α := ℝ≥0∞)
  ((((κ.fst ⊗ₖ condKernelCountable κCond h_atom : (a : α) → Measure (β × Ω)) a : Measure (β × Ω)) :
        (a : Set (β × Ω)) → ℝ≥0∞)
      s :
    ℝ≥0∞)
  ((Measure.fst.{u_2, u_3} (β := Ω) ((κ : (a : α) → Measure (β × Ω)) a) ⊗ₘ κCond a : (a : Set (β × Ω)) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: conv_rhs => rw [← (κ a).disintegrate (κCond a)]
-- 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 Ω
κ_1 : Kernel α (β × Ω)
κCond_1 : Kernel (α × β) Ω
inst : Countable α
κCond : α → Kernel β Ω
inst_1 : ∀ (a : α), IsMarkovKernel (κCond a)
h_atom : ∀ (x y : α), x ∈ measurableAtom y → κCond x = κCond y
κ : Kernel α (β × Ω)
inst_2 : IsSFiniteKernel κ
inst_3 : ∀ (a : α), Measure.IsCondKernel ((κ : (a : α) → Measure (β × Ω)) a) (κCond a)
a : α
s : Set (β × Ω)
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞)
    ((((κ.fst ⊗ₖ condKernelCountable κCond h_atom : (a : α) → Measure (β × Ω)) a : Measure (β × Ω)) :
          (a : Set (β × Ω)) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    ((Measure.fst.{u_2, u_3} (β := Ω) ((κ : (a : α) → Measure (β × Ω)) a) ⊗ₘ κCond a : (a : Set (β × Ω)) → ℝ≥0∞) s :
      ℝ≥0∞)
have disintegrate : ∫⁻ (b : β),
    (((κCond a : (a : β) → Measure Ω) b : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
      (Prod.mk b ⁻¹' s) ∂(κ.fst : (a : α) → Measure β) a =
  ∫⁻ (b : β),
    (((κCond a : (a : β) → Measure Ω) b : Measure Ω) : (a : Set Ω) → ℝ≥0∞)
      (Prod.mk b ⁻¹' s) ∂Measure.fst.{u_2, u_3} (β := Ω) ((κ : (a : α) → Measure (β × Ω)) a)
Tactic: simp_rw [compProd_apply hs, condKernelCountable_apply, Measure.compProd_apply hs]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CDFToKernel (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDF f κ ν
a : α
⊢ ∀ᵐ (b : β) ∂((ν : (a : α) → Measure β) a : Measure β), Monotone (f (a, b))
have h : ∀ (a_1 : β),
  Membership.mem (γ := Set β)
    {x : β |
      Membership.mem (γ := Set β) {x : β | (fun (b : β) ↦ IsRatStieltjesPoint f (a, b)) x} x →
        Membership.mem (γ := Set β) {x : β | (fun (b : β) ↦ Monotone (f (a, b))) x} x}
    a_1
Tactic: filter_upwards [hf.isRatStieltjesPoint_ae a] with b hb using hb.mono