awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CDFToKernel (hypothesis)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction ℝ
inst : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a : α
s : Set (β × ℝ)
t₁ : Set β
ht₁ : MeasurableSet t₁
t₂ : Set ℝ
ht₂ : MeasurableSet t₂
⊢ ∫⁻ (x : β) in t₁,
        (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, x) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
          (Prod.mk x ⁻¹' (fun (x1 : Set β) (x2 : Set ℝ) ↦ x1 ×ˢ x2) t₁ t₂) ∂(ν : (a : α) → Measure β) a +
      ∫⁻ (x : β) in t₁ᶜ,
        (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, x) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
          (Prod.mk x ⁻¹' (fun (x1 : Set β) (x2 : Set ℝ) ↦ x1 ×ˢ x2) t₁ t₂) ∂(ν : (a : α) → Measure β) a =
    (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞)
      ((fun (x1 : Set β) (x2 : Set ℝ) ↦ x1 ×ˢ x2) t₁ t₂)
have h_eq1 : ∫⁻ (x : β) in t₁,
    (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, x) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
      (Prod.mk x ⁻¹' t₁ ×ˢ t₂) ∂(ν : (a : α) → Measure β) a =
  ∫⁻ (x : β) in t₁,
    (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, x) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
      t₂ ∂(ν : (a : α) → Measure β) a
Tactic: have h_eq1 : ∫⁻ x in t₁, hf.toKernel f (a, x) (Prod.mk x ⁻¹' t₁ ×ˢ t₂) ∂(ν a)
        = ∫⁻ x in t₁, hf.toKernel f (a, x) t₂ ∂(ν a) := by
      refine setLIntegral_congr_fun ht₁ (fun a ha ↦ ?_)
      rw [mk_preimage_prod_right ha]
-- 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 : α × β → StieltjesFunction ℝ
inst : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a : α
s : Set (β × ℝ)
t₁ : Set β
ht₁ : MeasurableSet t₁
t₂ : Set ℝ
ht₂ : MeasurableSet t₂
h_eq1 :
  ∫⁻ (x : β) in t₁,
      (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, x) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
        (Prod.mk x ⁻¹' t₁ ×ˢ t₂) ∂(ν : (a : α) → Measure β) a =
    ∫⁻ (x : β) in t₁,
      (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, x) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
        t₂ ∂(ν : (a : α) → Measure β) a
h_eq_zero :
  ∀ x ∈ t₁ᶜ,
    Eq (α := ℝ≥0∞)
      ((((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, x) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
          (Prod.mk x ⁻¹' t₁ ×ˢ t₂) :
        ℝ≥0∞)
      (0 : ℝ≥0∞)
⊢ ∫⁻ (x : β) in t₁ᶜ,
      (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, x) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
        (Prod.mk x ⁻¹' t₁ ×ˢ t₂) ∂(ν : (a : α) → Measure β) a =
    0
have rw : ∫⁻ (x : β) in t₁ᶜ, 0 ∂(ν : (a : α) → Measure β) a = 0
Tactic: rw [setLIntegral_congr_fun ht₁.compl h_eq_zero]
-- 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 : α × β → StieltjesFunction ℝ
inst : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a : α
s : Set (β × ℝ)
t₁ : Set β
ht₁ : MeasurableSet t₁
t₂ : Set ℝ
ht₂ : MeasurableSet t₂
h_eq1 :
  ∫⁻ (x : β) in t₁,
      (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, x) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
        (Prod.mk x ⁻¹' t₁ ×ˢ t₂) ∂(ν : (a : α) → Measure β) a =
    ∫⁻ (x : β) in t₁,
      (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, x) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
        t₂ ∂(ν : (a : α) → Measure β) a
⊢ ∫⁻ (x : β) in t₁ᶜ,
      (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, x) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
        (Prod.mk x ⁻¹' t₁ ×ˢ t₂) ∂(ν : (a : α) → Measure β) a =
    0
have suffices : ∀ x ∈ t₁ᶜ,
  Eq (α := ℝ≥0∞)
    ((((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, x) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
        (Prod.mk x ⁻¹' t₁ ×ˢ t₂) :
      ℝ≥0∞)
    (0 : ℝ≥0∞)
Tactic: suffices h_eq_zero :
          ∀ x ∈ t₁ᶜ, hf.toKernel f (a, x) (Prod.mk x ⁻¹' t₁ ×ˢ t₂) = 0 by
        rw [setLIntegral_congr_fun ht₁.compl h_eq_zero]
        simp only [lintegral_const, zero_mul]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CDFToKernel (hypothesis)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction ℝ
inst : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a_1 : α
s : Set (β × ℝ)
t₁ : Set β
ht₁ : MeasurableSet t₁
t₂ : Set ℝ
ht₂ : MeasurableSet t₂
h_eq1 :
  ∫⁻ (x : β) in t₁,
      (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a_1, x) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
        (Prod.mk x ⁻¹' t₁ ×ˢ t₂) ∂(ν : (a : α) → Measure β) a_1 =
    ∫⁻ (x : β) in t₁,
      (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a_1, x) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
        t₂ ∂(ν : (a : α) → Measure β) a_1
a : β
hat₁ : a ∈ t₁ᶜ
⊢ Eq (α := ℝ≥0∞)
    ((((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a_1, a) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
        (Prod.mk a ⁻¹' t₁ ×ˢ t₂) :
      ℝ≥0∞)
    (0 : ℝ≥0∞)
have hat₂ : a ∉ t₁
Tactic: rw [mem_compl_iff] at hat₁
Cleared hypotheses: hat₁
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CDFToKernel (hypothesis)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction ℝ
inst : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a : α
s : Set (β × ℝ)
t₁ : Set β
ht₁ : MeasurableSet t₁
t₂ : Set ℝ
ht₂ : MeasurableSet t₂
h_eq1 :
  ∫⁻ (x : β) in t₁,
      (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, x) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
        (Prod.mk x ⁻¹' t₁ ×ˢ t₂) ∂(ν : (a : α) → Measure β) a =
    ∫⁻ (x : β) in t₁,
      (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, x) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
        t₂ ∂(ν : (a : α) → Measure β) a
⊢ ∫⁻ (x : β) in t₁,
        (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, x) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
          (Prod.mk x ⁻¹' (fun (x1 : Set β) (x2 : Set ℝ) ↦ x1 ×ˢ x2) t₁ t₂) ∂(ν : (a : α) → Measure β) a +
      ∫⁻ (x : β) in t₁ᶜ,
        (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, x) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
          (Prod.mk x ⁻¹' (fun (x1 : Set β) (x2 : Set ℝ) ↦ x1 ×ˢ x2) t₁ t₂) ∂(ν : (a : α) → Measure β) a =
    (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞)
      ((fun (x1 : Set β) (x2 : Set ℝ) ↦ x1 ×ˢ x2) t₁ t₂)
have h_eq2 : ∫⁻ (x : β) in t₁ᶜ,
    (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, x) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
      (Prod.mk x ⁻¹' t₁ ×ˢ t₂) ∂(ν : (a : α) → Measure β) a =
  0
Tactic: have h_eq2 :
        ∫⁻ x in t₁ᶜ, hf.toKernel f (a, x) (Prod.mk x ⁻¹' t₁ ×ˢ t₂) ∂(ν a) = 0 := by
      suffices h_eq_zero :
          ∀ x ∈ t₁ᶜ, hf.toKernel f (a, x) (Prod.mk x ⁻¹' t₁ ×ˢ t₂) = 0 by
        rw [setLIntegral_congr_fun ht₁.compl h_eq_zero]
        simp only [lintegral_const, zero_mul]
      intro a hat₁
      rw [mem_compl_iff] at hat₁
      simp only [hat₁, not_false_eq_true, mk_preimage_prod_right_eq_empty, measure_empty]
-- 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 : α × β → StieltjesFunction ℝ
inst : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a : α
s : Set (β × ℝ)
t₁ : Set β
ht₁ : MeasurableSet t₁
t₂ : Set ℝ
ht₂ : MeasurableSet t₂
h_eq1 :
  ∫⁻ (x : β) in t₁,
      (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, x) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
        (Prod.mk x ⁻¹' t₁ ×ˢ t₂) ∂(ν : (a : α) → Measure β) a =
    ∫⁻ (x : β) in t₁,
      (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, x) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
        t₂ ∂(ν : (a : α) → Measure β) a
h_eq2 :
  ∫⁻ (x : β) in t₁ᶜ,
      (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, x) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
        (Prod.mk x ⁻¹' t₁ ×ˢ t₂) ∂(ν : (a : α) → Measure β) a =
    0
⊢ ∫⁻ (x : β) in t₁,
        (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, x) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
          (Prod.mk x ⁻¹' (fun (x1 : Set β) (x2 : Set ℝ) ↦ x1 ×ˢ x2) t₁ t₂) ∂(ν : (a : α) → Measure β) a +
      ∫⁻ (x : β) in t₁ᶜ,
        (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, x) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
          (Prod.mk x ⁻¹' (fun (x1 : Set β) (x2 : Set ℝ) ↦ x1 ×ˢ x2) t₁ t₂) ∂(ν : (a : α) → Measure β) a =
    (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞)
      ((fun (x1 : Set β) (x2 : Set ℝ) ↦ x1 ×ˢ x2) t₁ t₂)
have basic : ∫⁻ (x : β) in t₁,
    (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, x) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
      t₂ ∂(ν : (a : α) → Measure β) a =
  (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞)
    ((fun (x1 : Set β) (x2 : Set ℝ) ↦ x1 ×ˢ x2) t₁ t₂)
Tactic: rw [h_eq1, h_eq2, add_zero]
-- 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 : α × β → StieltjesFunction ℝ
inst : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a : α
s t : Set (β × ℝ)
ht : MeasurableSet t
ht_eq :
  ∫⁻ (b : β),
      (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, b) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
        (Prod.mk b ⁻¹' t) ∂(ν : (a : α) → Measure β) a =
    (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) t
⊢ ∫⁻ (b : β),
      (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, b) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
        (Prod.mk b ⁻¹' t)ᶜ ∂(ν : (a : α) → Measure β) a =
    ∫⁻ (b : β),
      HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞)
        ((((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, b) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) univ :
          ℝ≥0∞)
        ((((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, b) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
            (Prod.mk b ⁻¹' t) :
          ℝ≥0∞) ∂(ν : (a : α) → Measure β) a
have e_f : ∀ (x : β),
  (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, x) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
      (Prod.mk x ⁻¹' t)ᶜ =
    HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞)
      ((((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, x) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) univ :
        ℝ≥0∞)
      ((((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, x) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
          (Prod.mk x ⁻¹' t) :
        ℝ≥0∞)
Tactic: congr with x : 1
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CDFToKernel (hypothesis)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction ℝ
inst : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a : α
s t : Set (β × ℝ)
ht : MeasurableSet t
ht_eq :
  ∫⁻ (b : β),
      (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, b) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
        (Prod.mk b ⁻¹' t) ∂(ν : (a : α) → Measure β) a =
    (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) t
⊢ ∫⁻ (b : β),
      HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞)
        ((((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, b) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) univ :
          ℝ≥0∞)
        ((((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, b) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
            (Prod.mk b ⁻¹' t) :
          ℝ≥0∞) ∂(ν : (a : α) → Measure β) a =
    ∫⁻ (x : β),
        (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, x) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
          univ ∂(ν : (a : α) → Measure β) a -
      ∫⁻ (x : β),
        (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, x) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
          (Prod.mk x ⁻¹' t) ∂(ν : (a : α) → Measure β) a
have h_le : (ae (F := Measure β) ((ν : (a : α) → Measure β) a : Measure β)).EventuallyLE (β := ℝ≥0∞)
  (fun (x : β) ↦
    (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, x) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
      (Prod.mk x ⁻¹' t))
  fun (x : β) ↦
  (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, x) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) univ
Tactic: have h_le : (fun x ↦ hf.toKernel f (a, x) (Prod.mk x ⁻¹' t))
              ≤ᵐ[ν a] fun x ↦ hf.toKernel f (a, x) univ :=
          Eventually.of_forall fun _ ↦ measure_mono (subset_univ _)
-- 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 : α × β → StieltjesFunction ℝ
inst : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a : α
s t : Set (β × ℝ)
ht : MeasurableSet t
ht_eq :
  ∫⁻ (b : β),
      (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, b) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
        (Prod.mk b ⁻¹' t) ∂(ν : (a : α) → Measure β) a =
    (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) t
h_le :
  (ae (F := Measure β) ((ν : (a : α) → Measure β) a : Measure β)).EventuallyLE (β := ℝ≥0∞)
    (fun (x : β) ↦
      (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, x) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
        (Prod.mk x ⁻¹' t))
    fun (x : β) ↦
    (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, x) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) univ
⊢ ∫⁻ (b : β),
      HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞)
        ((((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, b) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) univ :
          ℝ≥0∞)
        ((((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, b) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
            (Prod.mk b ⁻¹' t) :
          ℝ≥0∞) ∂(ν : (a : α) → Measure β) a =
    ∫⁻ (x : β),
        (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, x) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
          univ ∂(ν : (a : α) → Measure β) a -
      ∫⁻ (x : β),
        (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, x) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
          (Prod.mk x ⁻¹' t) ∂(ν : (a : α) → Measure β) a
have rw : Measurable (β := ℝ≥0∞) fun (x : β) ↦
  (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, x) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
    (Prod.mk x ⁻¹' t)
Tactic: rw [lintegral_sub _ _ h_le]
-- 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 : α × β → StieltjesFunction ℝ
inst : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a : α
s t : Set (β × ℝ)
ht : MeasurableSet t
ht_eq :
  ∫⁻ (b : β),
      (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, b) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
        (Prod.mk b ⁻¹' t) ∂(ν : (a : α) → Measure β) a =
    (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) t
h_le :
  (ae (F := Measure β) ((ν : (a : α) → Measure β) a : Measure β)).EventuallyLE (β := ℝ≥0∞)
    (fun (x : β) ↦
      (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, x) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
        (Prod.mk x ⁻¹' t))
    fun (x : β) ↦
    (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, x) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) univ
rw :
  Measurable (β := ℝ≥0∞) fun (x : β) ↦
    (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, x) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
      (Prod.mk x ⁻¹' t)
⊢ ∫⁻ (b : β),
      HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞)
        ((((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, b) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) univ :
          ℝ≥0∞)
        ((((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, b) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
            (Prod.mk b ⁻¹' t) :
          ℝ≥0∞) ∂(ν : (a : α) → Measure β) a =
    ∫⁻ (x : β),
        (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, x) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
          univ ∂(ν : (a : α) → Measure β) a -
      ∫⁻ (x : β),
        (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, x) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
          (Prod.mk x ⁻¹' t) ∂(ν : (a : α) → Measure β) a
have rw₁ : ∫⁻ (a_1 : β),
    (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, a_1) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
      (Prod.mk a_1 ⁻¹' t) ∂(ν : (a : α) → Measure β) a ≠
  ∞
Tactic: rw [lintegral_sub _ _ h_le]
-- 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 : α × β → StieltjesFunction ℝ
inst : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a : α
s t : Set (β × ℝ)
ht : MeasurableSet t
ht_eq :
  ∫⁻ (b : β),
      (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, b) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
        (Prod.mk b ⁻¹' t) ∂(ν : (a : α) → Measure β) a =
    (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) t
h_le :
  (ae (F := Measure β) ((ν : (a : α) → Measure β) a : Measure β)).EventuallyLE (β := ℝ≥0∞)
    (fun (x : β) ↦
      (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, x) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
        (Prod.mk x ⁻¹' t))
    fun (x : β) ↦
    (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, x) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) univ
⊢ ∫⁻ (a_1 : β),
      (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, a_1) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
        (Prod.mk a_1 ⁻¹' t) ∂(ν : (a : α) → Measure β) a ≠
    ∞
have refine : ∫⁻ (a_1 : β),
    (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, a_1) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
      univ ∂(ν : (a : α) → Measure β) a <
  ∞
Tactic: refine ((lintegral_mono_ae h_le).trans_lt ?_).ne
-- 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 : α × β → StieltjesFunction ℝ
inst : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a : α
s t : Set (β × ℝ)
ht : MeasurableSet t
ht_eq :
  ∫⁻ (b : β),
      (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, b) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
        (Prod.mk b ⁻¹' t) ∂(ν : (a : α) → Measure β) a =
    (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) t
h_le :
  (ae (F := Measure β) ((ν : (a : α) → Measure β) a : Measure β)).EventuallyLE (β := ℝ≥0∞)
    (fun (x : β) ↦
      (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, x) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
        (Prod.mk x ⁻¹' t))
    fun (x : β) ↦
    (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, x) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) univ
⊢ ∫⁻ (a_1 : β),
      (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, a_1) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
        univ ∂(ν : (a : α) → Measure β) a <
    ∞
have rw : LT.lt (α := ℝ≥0∞) ((((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) univ : ℝ≥0∞)
  (∞ : ℝ≥0∞)
Tactic: rw [lintegral_toKernel_univ hf]
-- 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 : α × β → StieltjesFunction ℝ
inst : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a : α
s t : Set (β × ℝ)
ht : MeasurableSet t
ht_eq :
  ∫⁻ (b : β),
      (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, b) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
        (Prod.mk b ⁻¹' t) ∂(ν : (a : α) → Measure β) a =
    (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) t
⊢ ∫⁻ (x : β),
        (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, x) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
          univ ∂(ν : (a : α) → Measure β) a -
      ∫⁻ (x : β),
        (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, x) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
          (Prod.mk x ⁻¹' t) ∂(ν : (a : α) → Measure β) a =
    HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞)
      ((((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) univ : ℝ≥0∞)
      ((((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) t : ℝ≥0∞)
have rw : HSub.hSub (β := ℝ≥0∞)
    (∫⁻ (x : β),
      (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, x) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
        univ ∂(ν : (a : α) → Measure β) a)
    ((((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) t : ℝ≥0∞) =
  HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞)
    ((((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) univ : ℝ≥0∞)
    ((((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: rw [ht_eq, lintegral_toKernel_univ hf]
-- 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 : α × β → StieltjesFunction ℝ
inst : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a : α
s t : Set (β × ℝ)
ht : MeasurableSet t
ht_eq :
  ∫⁻ (b : β),
      (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, b) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
        (Prod.mk b ⁻¹' t) ∂(ν : (a : α) → Measure β) a =
    (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) t
rw :
  HSub.hSub (β := ℝ≥0∞)
      (∫⁻ (x : β),
        (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, x) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
          univ ∂(ν : (a : α) → Measure β) a)
      ((((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) t : ℝ≥0∞) =
    HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞)
      ((((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) univ : ℝ≥0∞)
      ((((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) t : ℝ≥0∞)
⊢ ∫⁻ (x : β),
        (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, x) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
          univ ∂(ν : (a : α) → Measure β) a -
      ∫⁻ (x : β),
        (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, x) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
          (Prod.mk x ⁻¹' t) ∂(ν : (a : α) → Measure β) a =
    HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞)
      ((((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) univ : ℝ≥0∞)
      ((((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) t : ℝ≥0∞)
have rw₁ : HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞)
    ((((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) univ : ℝ≥0∞)
    ((((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) t : ℝ≥0∞) =
  HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞)
    ((((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) univ : ℝ≥0∞)
    ((((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: rw [ht_eq, lintegral_toKernel_univ hf]