awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : α × β → ℚ → ℝ
inst : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
x : ℝ
s : Set β
hs : MeasurableSet s
hρ_zero : Eq (α := Measure β) (Measure.restrict ((ν : (a : α) → Measure β) a) s) 0
q : ℚ
hq : x < (↑q : ℝ)
⊢ Eq (α := ℝ≥0∞) (0 : ℝ≥0∞)
    ((((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) (s ×ˢ Iic x) : ℝ≥0∞)
have pos : Eq (α := ℝ≥0∞)
  ((((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞)
      (SProd.sprod (β := Set ℝ) s (Iic (↑q : ℝ))) :
    ℝ≥0∞)
  (0 : ℝ≥0∞)
Tactic: suffices κ a (s ×ˢ Iic (q : ℝ)) = 0 by
      symm
      refine measure_mono_null (fun p ↦ ?_) this
      simp only [mem_prod, mem_Iic, and_imp]
      exact fun h1 h2 ↦ ⟨h1, h2.trans hq.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 : α × β → ℚ → ℝ
inst : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
x : ℝ
s : Set β
hs : MeasurableSet s
hρ_zero : Eq (α := Measure β) (Measure.restrict ((ν : (a : α) → Measure β) a) s) 0
q : ℚ
hq : x < (↑q : ℝ)
⊢ Eq (α := ℝ≥0∞)
    ((((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞)
        (SProd.sprod (β := Set ℝ) s (Iic (↑q : ℝ))) :
      ℝ≥0∞)
    (0 : ℝ≥0∞)
have pos : Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (β × ℝ)) a)
    (SProd.sprod (β := Set ℝ) s (Iic (↑q : ℝ))) =
  0
Tactic: suffices (κ a).real (s ×ˢ Iic (q : ℝ)) = 0 by
      rw [measureReal_eq_zero_iff] at this
      simpa [measure_ne_top] using this
-- 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 : α × β → ℚ → ℝ
inst : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
x : ℝ
s : Set β
hs : MeasurableSet s
hρ_zero : Eq (α := Measure β) (Measure.restrict ((ν : (a : α) → Measure β) a) s) 0
q : ℚ
hq : x < (↑q : ℝ)
⊢ Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (β × ℝ)) a)
      (SProd.sprod (β := Set ℝ) s (Iic (↑q : ℝ))) =
    0
have pos : Eq (α := ℝ) (@integral _ _ _ _ mβ (Measure.restrict ((ν : (a : α) → Measure β) a) s) fun (b : β) ↦ f (a, b) q) 0
Tactic: rw [← hf.setIntegral a hs q]
-- 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 : α × β → ℚ → ℝ
inst : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
x : ℝ
s : Set β
hs : MeasurableSet s
hρ_zero : ¬Eq (α := Measure β) (Measure.restrict ((ν : (a : α) → Measure β) a) s) 0
⊢ ∫⁻ (b : β) in s, ENNReal.ofReal ((↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) x) ∂(ν : (a : α) → Measure β) a =
    ∫⁻ (b : β) in s,
      ⨅ (r : { r' : ℚ // x < (↑r' : ℝ) }),
        ENNReal.ofReal ((↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) (↑(↑r : ℚ) : ℝ)) ∂(ν : (a : α) → Measure β) a
have e_f : ∀ (b : β),
  ENNReal.ofReal ((↑(stieltjesOfMeasurableRat f sorry (a, b)) : ℝ → ℝ) x) =
    ⨅ (r : { r' : ℚ // x < (↑r' : ℝ) }),
      ENNReal.ofReal ((↑(stieltjesOfMeasurableRat f sorry (a, b)) : ℝ → ℝ) (↑(↑r : ℚ) : ℝ))
Tactic: congr with b : 1
-- 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 : α × β → ℚ → ℝ
inst : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
x : ℝ
s : Set β
hs : MeasurableSet s
hρ_zero : ¬Eq (α := Measure β) (Measure.restrict ((ν : (a : α) → Measure β) a) s) 0
b : β
⊢ ENNReal.ofReal ((↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) x) =
    ⨅ (r : { r' : ℚ // x < (↑r' : ℝ) }),
      ENNReal.ofReal ((↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) (↑(↑r : ℚ) : ℝ))
have e_f : Eq (α := ℝ≥0∞) (((stieltjesOfMeasurableRat f sorry (a, b)).measure : (a : Set ℝ) → ℝ≥0∞) (Iic x) : ℝ≥0∞)
  (⨅ (r : { r' : ℚ // x < (↑r' : ℝ) }),
      ((stieltjesOfMeasurableRat f sorry (a, b)).measure : (a : Set ℝ) → ℝ≥0∞) (Iic (↑(↑r : ℚ) : ℝ)) :
    ℝ≥0∞)
Tactic: simp_rw [← measure_stieltjesOfMeasurableRat_Iic]
-- 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 : α × β → ℚ → ℝ
inst : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
x : ℝ
s : Set β
hs : MeasurableSet s
hρ_zero : ¬Eq (α := Measure β) (Measure.restrict ((ν : (a : α) → Measure β) a) s) 0
b : β
⊢ Eq (α := ℝ≥0∞) (((stieltjesOfMeasurableRat f ⋯ (a, b)).measure : (a : Set ℝ) → ℝ≥0∞) (Iic x) : ℝ≥0∞)
    (⨅ (r : { r' : ℚ // x < (↑r' : ℝ) }),
        ((stieltjesOfMeasurableRat f ⋯ (a, b)).measure : (a : Set ℝ) → ℝ≥0∞) (Iic (↑(↑r : ℚ) : ℝ)) :
      ℝ≥0∞)
have e_f : Eq (α := ℝ≥0∞) (((stieltjesOfMeasurableRat f sorry (a, b)).measure : (a : Set ℝ) → ℝ≥0∞) (Iic x) : ℝ≥0∞)
  (((stieltjesOfMeasurableRat f sorry (a, b)).measure : (a : Set ℝ) → ℝ≥0∞)
      (⋂ (i : { r' : ℚ // x < (↑r' : ℝ) }), Iic (↑(↑i : ℚ) : ℝ)) :
    ℝ≥0∞)
Tactic: rw [← Monotone.measure_iInter]
-- 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 : α × β → ℚ → ℝ
inst : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
x : ℝ
s : Set β
hs : MeasurableSet s
hρ_zero : ¬Eq (α := Measure β) (Measure.restrict ((ν : (a : α) → Measure β) a) s) 0
b : β
e_f :
  Eq (α := ℝ≥0∞) (((stieltjesOfMeasurableRat f ⋯ (a, b)).measure : (a : Set ℝ) → ℝ≥0∞) (Iic x) : ℝ≥0∞)
    (((stieltjesOfMeasurableRat f ⋯ (a, b)).measure : (a : Set ℝ) → ℝ≥0∞)
        (⋂ (i : { r' : ℚ // x < (↑r' : ℝ) }), Iic (↑(↑i : ℚ) : ℝ)) :
      ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((stieltjesOfMeasurableRat f ⋯ (a, b)).measure : (a : Set ℝ) → ℝ≥0∞) (Iic x) : ℝ≥0∞)
    (⨅ (r : { r' : ℚ // x < (↑r' : ℝ) }),
        ((stieltjesOfMeasurableRat f ⋯ (a, b)).measure : (a : Set ℝ) → ℝ≥0∞) (Iic (↑(↑r : ℚ) : ℝ)) :
      ℝ≥0∞)
have e_f₁ : Monotone (β := Set ℝ) fun (r : { r' : ℚ // x < (↑r' : ℝ) }) ↦ Iic (↑(↑r : ℚ) : ℝ)
Tactic: rw [← Monotone.measure_iInter]
-- 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 : α × β → ℚ → ℝ
inst : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
x : ℝ
s : Set β
hs : MeasurableSet s
hρ_zero : ¬Eq (α := Measure β) (Measure.restrict ((ν : (a : α) → Measure β) a) s) 0
b : β
e_f :
  Eq (α := ℝ≥0∞) (((stieltjesOfMeasurableRat f ⋯ (a, b)).measure : (a : Set ℝ) → ℝ≥0∞) (Iic x) : ℝ≥0∞)
    (((stieltjesOfMeasurableRat f ⋯ (a, b)).measure : (a : Set ℝ) → ℝ≥0∞)
        (⋂ (i : { r' : ℚ // x < (↑r' : ℝ) }), Iic (↑(↑i : ℚ) : ℝ)) :
      ℝ≥0∞)
e_f₁ : Monotone (β := Set ℝ) fun (r : { r' : ℚ // x < (↑r' : ℝ) }) ↦ Iic (↑(↑r : ℚ) : ℝ)
⊢ Eq (α := ℝ≥0∞) (((stieltjesOfMeasurableRat f ⋯ (a, b)).measure : (a : Set ℝ) → ℝ≥0∞) (Iic x) : ℝ≥0∞)
    (⨅ (r : { r' : ℚ // x < (↑r' : ℝ) }),
        ((stieltjesOfMeasurableRat f ⋯ (a, b)).measure : (a : Set ℝ) → ℝ≥0∞) (Iic (↑(↑r : ℚ) : ℝ)) :
      ℝ≥0∞)
have e_f₂ : ∀ (i : { r' : ℚ // x < (↑r' : ℝ) }),
  NullMeasurableSet (Iic (↑(↑i : ℚ) : ℝ)) (stieltjesOfMeasurableRat f sorry (a, b)).measure
Tactic: rw [← Monotone.measure_iInter]
-- 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 : α × β → ℚ → ℝ
inst : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
x : ℝ
s : Set β
hs : MeasurableSet s
hρ_zero : ¬Eq (α := Measure β) (Measure.restrict ((ν : (a : α) → Measure β) a) s) 0
b : β
e_f :
  Eq (α := ℝ≥0∞) (((stieltjesOfMeasurableRat f ⋯ (a, b)).measure : (a : Set ℝ) → ℝ≥0∞) (Iic x) : ℝ≥0∞)
    (((stieltjesOfMeasurableRat f ⋯ (a, b)).measure : (a : Set ℝ) → ℝ≥0∞)
        (⋂ (i : { r' : ℚ // x < (↑r' : ℝ) }), Iic (↑(↑i : ℚ) : ℝ)) :
      ℝ≥0∞)
e_f₁ : Monotone (β := Set ℝ) fun (r : { r' : ℚ // x < (↑r' : ℝ) }) ↦ Iic (↑(↑r : ℚ) : ℝ)
e_f₂ :
  ∀ (i : { r' : ℚ // x < (↑r' : ℝ) }),
    NullMeasurableSet (Iic (↑(↑i : ℚ) : ℝ)) (stieltjesOfMeasurableRat f ⋯ (a, b)).measure
⊢ Eq (α := ℝ≥0∞) (((stieltjesOfMeasurableRat f ⋯ (a, b)).measure : (a : Set ℝ) → ℝ≥0∞) (Iic x) : ℝ≥0∞)
    (⨅ (r : { r' : ℚ // x < (↑r' : ℝ) }),
        ((stieltjesOfMeasurableRat f ⋯ (a, b)).measure : (a : Set ℝ) → ℝ≥0∞) (Iic (↑(↑r : ℚ) : ℝ)) :
      ℝ≥0∞)
have e_f₃ : ∃ (i : { r' : ℚ // x < (↑r' : ℝ) }),
  Ne (α := ℝ≥0∞) (((stieltjesOfMeasurableRat f sorry (a, b)).measure : (a : Set ℝ) → ℝ≥0∞) (Iic (↑(↑i : ℚ) : ℝ)) : ℝ≥0∞)
    (∞ : ℝ≥0∞)
Tactic: rw [← Monotone.measure_iInter]
-- 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 : α × β → ℚ → ℝ
inst : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
x : ℝ
s : Set β
hs : MeasurableSet s
hρ_zero : ¬Eq (α := Measure β) (Measure.restrict ((ν : (a : α) → Measure β) a) s) 0
b : β
⊢ Eq (α := ℝ≥0∞) (((stieltjesOfMeasurableRat f ⋯ (a, b)).measure : (a : Set ℝ) → ℝ≥0∞) (Iic x) : ℝ≥0∞)
    (((stieltjesOfMeasurableRat f ⋯ (a, b)).measure : (a : Set ℝ) → ℝ≥0∞)
        (⋂ (i : { r' : ℚ // x < (↑r' : ℝ) }), Iic (↑(↑i : ℚ) : ℝ)) :
      ℝ≥0∞)
have e_f : ∀ (y : ℝ), y ∈ Iic x ↔ Membership.mem (γ := Set ℝ) (⋂ (i : { r' : ℚ // x < (↑r' : ℝ) }), Iic (↑(↑i : ℚ) : ℝ)) y
Tactic: congr with y : 1
-- 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 : α × β → ℚ → ℝ
inst : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
x : ℝ
s : Set β
hs : MeasurableSet s
hρ_zero : ¬Eq (α := Measure β) (Measure.restrict ((ν : (a : α) → Measure β) a) s) 0
b : β
y : ℝ
⊢ y ∈ Iic x ↔ Membership.mem (γ := Set ℝ) (⋂ (i : { r' : ℚ // x < (↑r' : ℝ) }), Iic (↑(↑i : ℚ) : ℝ)) y
have e_f : y ≤ x ↔ ∀ (a : ℚ) (b : x < (↑a : ℝ)), y ≤ (↑a : ℝ)
Tactic: simp only [mem_Iic, mem_iInter, Subtype.forall]
-- 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 : α × β → ℚ → ℝ
inst : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
x : ℝ
s : Set β
hs : MeasurableSet s
hρ_zero : ¬Eq (α := Measure β) (Measure.restrict ((ν : (a : α) → Measure β) a) s) 0
b : β
⊢ ∃ (i : { r' : ℚ // x < (↑r' : ℝ) }),
    Ne (α := ℝ≥0∞) (((stieltjesOfMeasurableRat f ⋯ (a, b)).measure : (a : Set ℝ) → ℝ≥0∞) (Iic (↑(↑i : ℚ) : ℝ)) : ℝ≥0∞)
      (∞ : ℝ≥0∞)
have e_f : ∀ (q : ℚ) (hq : x < (↑q : ℝ)),
  ∃ (i : { r' : ℚ // x < (↑r' : ℝ) }),
    Ne (α := ℝ≥0∞) (((stieltjesOfMeasurableRat f sorry (a, b)).measure : (a : Set ℝ) → ℝ≥0∞) (Iic (↑(↑i : ℚ) : ℝ)) : ℝ≥0∞)
      (∞ : ℝ≥0∞)
Tactic: obtain ⟨q, hq⟩ := exists_rat_gt x
-- 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 : α × β → ℚ → ℝ
inst : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
x : ℝ
s : Set β
hs : MeasurableSet s
hρ_zero : ¬Eq (α := Measure β) (Measure.restrict ((ν : (a : α) → Measure β) a) s) 0
⊢ ∫⁻ (b : β) in s, ENNReal.ofReal ((↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) x) ∂(ν : (a : α) → Measure β) a =
    (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) (s ×ˢ Iic x)
have h : ∫⁻ (b : β) in s, ENNReal.ofReal ((↑(stieltjesOfMeasurableRat f sorry (a, b)) : ℝ → ℝ) x) ∂(ν : (a : α) → Measure β) a =
  ∫⁻ (b : β) in s,
    ⨅ (r : { r' : ℚ // x < (↑r' : ℝ) }),
      ENNReal.ofReal ((↑(stieltjesOfMeasurableRat f sorry (a, b)) : ℝ → ℝ) (↑(↑r : ℚ) : ℝ)) ∂(ν : (a : α) → Measure β) a
Tactic: have h : ∫⁻ b in s, ENNReal.ofReal (stieltjesOfMeasurableRat f hf.measurable (a, b) x) ∂(ν a)
      = ∫⁻ b in s, ⨅ r : { r' : ℚ // x < r' },
        ENNReal.ofReal (stieltjesOfMeasurableRat f hf.measurable (a, b) r) ∂(ν a) := by
    congr with b : 1
    simp_rw [← measure_stieltjesOfMeasurableRat_Iic]
    rw [← Monotone.measure_iInter]
    · congr with y : 1
      simp only [mem_Iic, mem_iInter, Subtype.forall]
      exact le_iff_forall_lt_rat_imp_le
    · exact fun r r' hrr' ↦ Iic_subset_Iic.mpr <| mod_cast hrr'
    · exact fun _ ↦ nullMeasurableSet_Iic
    · obtain ⟨q, hq⟩ := exists_rat_gt x
      exact ⟨⟨q, hq⟩, measure_ne_top _ _⟩
-- 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 : α × β → ℚ → ℝ
inst : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
x : ℝ
s : Set β
hs : MeasurableSet s
hρ_zero : ¬Eq (α := Measure β) (Measure.restrict ((ν : (a : α) → Measure β) a) s) 0
h :
  ∫⁻ (b : β) in s, ENNReal.ofReal ((↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) x) ∂(ν : (a : α) → Measure β) a =
    ∫⁻ (b : β) in s,
      ⨅ (r : { r' : ℚ // x < (↑r' : ℝ) }),
        ENNReal.ofReal ((↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) (↑(↑r : ℚ) : ℝ)) ∂(ν : (a : α) → Measure β) a
⊢ Nonempty { r' : ℚ // x < (↑r' : ℝ) }
have obtain : ∀ (r : ℚ) (hrx : x < (↑r : ℝ)), Nonempty { r' : ℚ // x < (↑r' : ℝ) }
Tactic: obtain ⟨r, hrx⟩ := exists_rat_gt x
-- 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 : α × β → ℚ → ℝ
inst : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
x : ℝ
s : Set β
hs : MeasurableSet s
hρ_zero : ¬Eq (α := Measure β) (Measure.restrict ((ν : (a : α) → Measure β) a) s) 0
h :
  ∫⁻ (b : β) in s, ENNReal.ofReal ((↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) x) ∂(ν : (a : α) → Measure β) a =
    ∫⁻ (b : β) in s,
      ⨅ (r : { r' : ℚ // x < (↑r' : ℝ) }),
        ENNReal.ofReal ((↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) (↑(↑r : ℚ) : ℝ)) ∂(ν : (a : α) → Measure β) a
⊢ ∫⁻ (b : β) in s, ENNReal.ofReal ((↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) x) ∂(ν : (a : α) → Measure β) a =
    (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) (s ×ˢ Iic x)
have h_nonempty : Nonempty { r' : ℚ // x < (↑r' : ℝ) }
Tactic: have h_nonempty : Nonempty { r' : ℚ // x < ↑r' } := by
    obtain ⟨r, hrx⟩ := exists_rat_gt x
    exact ⟨⟨r, hrx⟩⟩
-- 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 : α × β → ℚ → ℝ
inst : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
x : ℝ
s : Set β
hs : MeasurableSet s
hρ_zero : ¬Eq (α := Measure β) (Measure.restrict ((ν : (a : α) → Measure β) a) s) 0
h :
  ∫⁻ (b : β) in s, ENNReal.ofReal ((↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) x) ∂(ν : (a : α) → Measure β) a =
    ∫⁻ (b : β) in s,
      ⨅ (r : { r' : ℚ // x < (↑r' : ℝ) }),
        ENNReal.ofReal ((↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) (↑(↑r : ℚ) : ℝ)) ∂(ν : (a : α) → Measure β) a
h_nonempty : Nonempty { r' : ℚ // x < (↑r' : ℝ) }
⊢ ∫⁻ (b : β) in s, ENNReal.ofReal ((↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) x) ∂(ν : (a : α) → Measure β) a =
    (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) (s ×ˢ Iic x)
have neg : Eq (α := ℝ≥0∞)
  (⨅ (b : { r' : ℚ // x < (↑r' : ℝ) }),
      ∫⁻ (a_1 : β) in s,
        ENNReal.ofReal
          ((↑(stieltjesOfMeasurableRat f sorry (a, a_1)) : ℝ → ℝ) (↑(↑b : ℚ) : ℝ)) ∂(ν : (a : α) → Measure β) a :
    ℝ≥0∞)
  ((((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) (s ×ˢ Iic x) : ℝ≥0∞)
Tactic: rw [h, lintegral_iInf_directed_of_measurable hρ_zero fun q : { r' : ℚ // x < ↑r' } ↦ ?_]
-- 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 : α × β → ℚ → ℝ
inst : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
x : ℝ
s : Set β
hs : MeasurableSet s
hρ_zero : ¬Eq (α := Measure β) (Measure.restrict ((ν : (a : α) → Measure β) a) s) 0
h :
  ∫⁻ (b : β) in s, ENNReal.ofReal ((↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) x) ∂(ν : (a : α) → Measure β) a =
    ∫⁻ (b : β) in s,
      ⨅ (r : { r' : ℚ // x < (↑r' : ℝ) }),
        ENNReal.ofReal ((↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) (↑(↑r : ℚ) : ℝ)) ∂(ν : (a : α) → Measure β) a
h_nonempty : Nonempty { r' : ℚ // x < (↑r' : ℝ) }
neg :
  Eq (α := ℝ≥0∞)
    (⨅ (b : { r' : ℚ // x < (↑r' : ℝ) }),
        ∫⁻ (a_1 : β) in s,
          ENNReal.ofReal
            ((↑(stieltjesOfMeasurableRat f ⋯ (a, a_1)) : ℝ → ℝ) (↑(↑b : ℚ) : ℝ)) ∂(ν : (a : α) → Measure β) a :
      ℝ≥0∞)
    ((((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) (s ×ˢ Iic x) : ℝ≥0∞)
⊢ ∫⁻ (b : β) in s, ENNReal.ofReal ((↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) x) ∂(ν : (a : α) → Measure β) a =
    (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) (s ×ˢ Iic x)
have neg₁ : ∀ (b : { r' : ℚ // x < (↑r' : ℝ) }),
  ∫⁻ (a_1 : β) in s,
      ENNReal.ofReal ((↑(stieltjesOfMeasurableRat f sorry (a, a_1)) : ℝ → ℝ) (↑(↑b : ℚ) : ℝ)) ∂(ν : (a : α) → Measure β) a ≠
    ∞
Tactic: rw [h, lintegral_iInf_directed_of_measurable hρ_zero fun q : { r' : ℚ // x < ↑r' } ↦ ?_]
-- 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 : α × β → ℚ → ℝ
inst : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
x : ℝ
s : Set β
hs : MeasurableSet s
hρ_zero : ¬Eq (α := Measure β) (Measure.restrict ((ν : (a : α) → Measure β) a) s) 0
h :
  ∫⁻ (b : β) in s, ENNReal.ofReal ((↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) x) ∂(ν : (a : α) → Measure β) a =
    ∫⁻ (b : β) in s,
      ⨅ (r : { r' : ℚ // x < (↑r' : ℝ) }),
        ENNReal.ofReal ((↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) (↑(↑r : ℚ) : ℝ)) ∂(ν : (a : α) → Measure β) a
h_nonempty : Nonempty { r' : ℚ // x < (↑r' : ℝ) }
neg :
  Eq (α := ℝ≥0∞)
    (⨅ (b : { r' : ℚ // x < (↑r' : ℝ) }),
        ∫⁻ (a_1 : β) in s,
          ENNReal.ofReal
            ((↑(stieltjesOfMeasurableRat f ⋯ (a, a_1)) : ℝ → ℝ) (↑(↑b : ℚ) : ℝ)) ∂(ν : (a : α) → Measure β) a :
      ℝ≥0∞)
    ((((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) (s ×ˢ Iic x) : ℝ≥0∞)
neg₁ :
  ∀ (b : { r' : ℚ // x < (↑r' : ℝ) }),
    ∫⁻ (a_1 : β) in s,
        ENNReal.ofReal
          ((↑(stieltjesOfMeasurableRat f ⋯ (a, a_1)) : ℝ → ℝ) (↑(↑b : ℚ) : ℝ)) ∂(ν : (a : α) → Measure β) a ≠
      ∞
⊢ ∫⁻ (b : β) in s, ENNReal.ofReal ((↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) x) ∂(ν : (a : α) → Measure β) a =
    (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) (s ×ˢ Iic x)
have neg₂ : Directed (fun (x1 x2 : β → ℝ≥0∞) ↦ x1 ≥ x2) fun (r : { r' : ℚ // x < (↑r' : ℝ) }) (b : β) ↦
  ENNReal.ofReal ((↑(stieltjesOfMeasurableRat f sorry (a, b)) : ℝ → ℝ) (↑(↑r : ℚ) : ℝ))
Tactic: rw [h, lintegral_iInf_directed_of_measurable hρ_zero fun q : { r' : ℚ // x < ↑r' } ↦ ?_]
-- 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 : α × β → ℚ → ℝ
inst : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
x : ℝ
s : Set β
hs : MeasurableSet s
hρ_zero : ¬Eq (α := Measure β) (Measure.restrict ((ν : (a : α) → Measure β) a) s) 0
h :
  ∫⁻ (b : β) in s, ENNReal.ofReal ((↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) x) ∂(ν : (a : α) → Measure β) a =
    ∫⁻ (b : β) in s,
      ⨅ (r : { r' : ℚ // x < (↑r' : ℝ) }),
        ENNReal.ofReal ((↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) (↑(↑r : ℚ) : ℝ)) ∂(ν : (a : α) → Measure β) a
h_nonempty : Nonempty { r' : ℚ // x < (↑r' : ℝ) }
neg :
  Eq (α := ℝ≥0∞)
    (⨅ (b : { r' : ℚ // x < (↑r' : ℝ) }),
        ∫⁻ (a_1 : β) in s,
          ENNReal.ofReal
            ((↑(stieltjesOfMeasurableRat f ⋯ (a, a_1)) : ℝ → ℝ) (↑(↑b : ℚ) : ℝ)) ∂(ν : (a : α) → Measure β) a :
      ℝ≥0∞)
    ((((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) (s ×ˢ Iic x) : ℝ≥0∞)
neg₁ :
  ∀ (b : { r' : ℚ // x < (↑r' : ℝ) }),
    ∫⁻ (a_1 : β) in s,
        ENNReal.ofReal
          ((↑(stieltjesOfMeasurableRat f ⋯ (a, a_1)) : ℝ → ℝ) (↑(↑b : ℚ) : ℝ)) ∂(ν : (a : α) → Measure β) a ≠
      ∞
neg₂ :
  Directed (fun (x1 x2 : β → ℝ≥0∞) ↦ x1 ≥ x2) fun (r : { r' : ℚ // x < (↑r' : ℝ) }) (b : β) ↦
    ENNReal.ofReal ((↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) (↑(↑r : ℚ) : ℝ))
⊢ ∫⁻ (b : β) in s, ENNReal.ofReal ((↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) x) ∂(ν : (a : α) → Measure β) a =
    (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) (s ×ˢ Iic x)
have rw : ∀ (q : { r' : ℚ // x < (↑r' : ℝ) }),
  Measurable (β := ℝ≥0∞) fun (b : β) ↦ ENNReal.ofReal ((↑(stieltjesOfMeasurableRat f sorry (a, b)) : ℝ → ℝ) (↑(↑q : ℚ) : ℝ))
Tactic: rw [h, lintegral_iInf_directed_of_measurable hρ_zero fun q : { r' : ℚ // x < ↑r' } ↦ ?_]
-- 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 : α × β → ℚ → ℝ
inst : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
x : ℝ
s : Set β
hs : MeasurableSet s
hρ_zero : ¬Eq (α := Measure β) (Measure.restrict ((ν : (a : α) → Measure β) a) s) 0
h :
  ∫⁻ (b : β) in s, ENNReal.ofReal ((↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) x) ∂(ν : (a : α) → Measure β) a =
    ∫⁻ (b : β) in s,
      ⨅ (r : { r' : ℚ // x < (↑r' : ℝ) }),
        ENNReal.ofReal ((↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) (↑(↑r : ℚ) : ℝ)) ∂(ν : (a : α) → Measure β) a
h_nonempty : Nonempty { r' : ℚ // x < (↑r' : ℝ) }
b : { r' : ℚ // x < (↑r' : ℝ) }
⊢ ∫⁻ (a_1 : β) in s,
      ENNReal.ofReal ((↑(stieltjesOfMeasurableRat f ⋯ (a, a_1)) : ℝ → ℝ) (↑(↑b : ℚ) : ℝ)) ∂(ν : (a : α) → Measure β) a ≠
    ∞
have neg : Ne (α := ℝ≥0∞)
  ((((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞)
      (SProd.sprod (β := Set ℝ) s (Iic (↑(↑b : ℚ) : ℝ))) :
    ℝ≥0∞)
  (∞ : ℝ≥0∞)
Tactic: rw [setLIntegral_stieltjesOfMeasurableRat_rat hf a _ 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 : α × β → ℚ → ℝ
inst : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
x : ℝ
s : Set β
hs : MeasurableSet s
hρ_zero : ¬Eq (α := Measure β) (Measure.restrict ((ν : (a : α) → Measure β) a) s) 0
h :
  ∫⁻ (b : β) in s, ENNReal.ofReal ((↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) x) ∂(ν : (a : α) → Measure β) a =
    ∫⁻ (b : β) in s,
      ⨅ (r : { r' : ℚ // x < (↑r' : ℝ) }),
        ENNReal.ofReal ((↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) (↑(↑r : ℚ) : ℝ)) ∂(ν : (a : α) → Measure β) a
h_nonempty : Nonempty { r' : ℚ // x < (↑r' : ℝ) }
⊢ Directed (fun (x1 x2 : β → ℝ≥0∞) ↦ x1 ≥ x2) fun (r : { r' : ℚ // x < (↑r' : ℝ) }) (b : β) ↦
    ENNReal.ofReal ((↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) (↑(↑r : ℚ) : ℝ))
have neg : ∀ (i j : { r' : ℚ // x < (↑r' : ℝ) }) (hij : i ≤ j) (b : β),
  ENNReal.ofReal ((↑(stieltjesOfMeasurableRat f sorry (a, b)) : ℝ → ℝ) (↑(↑i : ℚ) : ℝ)) ≤
    ENNReal.ofReal ((↑(stieltjesOfMeasurableRat f sorry (a, b)) : ℝ → ℝ) (↑(↑j : ℚ) : ℝ))
Tactic: refine Monotone.directed_ge fun i j hij b ↦ ?_