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
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' : ℝ) }
i j : { r' : ℚ // x < (↑r' : ℝ) }
hij : i ≤ j
b : β
⊢ ENNReal.ofReal ((↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) (↑(↑i : ℚ) : ℝ)) ≤
    ENNReal.ofReal ((↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) (↑(↑j : ℚ) : ℝ))
have neg : LE.le (α := ℝ≥0∞) (((stieltjesOfMeasurableRat f sorry (a, b)).measure : (a : Set ℝ) → ℝ≥0∞) (Iic (↑(↑i : ℚ) : ℝ)) : ℝ≥0∞)
  (((stieltjesOfMeasurableRat f sorry (a, b)).measure : (a : Set ℝ) → ℝ≥0∞) (Iic (↑(↑j : ℚ) : ℝ)) : ℝ≥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
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' : ℝ) }
i j : { r' : ℚ // x < (↑r' : ℝ) }
hij : i ≤ j
b : β
⊢ LE.le (α := ℝ≥0∞) (((stieltjesOfMeasurableRat f ⋯ (a, b)).measure : (a : Set ℝ) → ℝ≥0∞) (Iic (↑(↑i : ℚ) : ℝ)) : ℝ≥0∞)
    (((stieltjesOfMeasurableRat f ⋯ (a, b)).measure : (a : Set ℝ) → ℝ≥0∞) (Iic (↑(↑j : ℚ) : ℝ)) : ℝ≥0∞)
have neg : LE.le (α := ℝ) (↑(↑i : ℚ) : ℝ) (↑(↑j : ℚ) : ℝ)
Tactic: refine measure_mono (Iic_subset_Iic.mpr ?_)
-- 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' : ℝ) }
q : { r' : ℚ // x < (↑r' : ℝ) }
⊢ Measurable (β := ℝ≥0∞) fun (b : β) ↦ ENNReal.ofReal ((↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) (↑(↑q : ℚ) : ℝ))
have refine : Measurable (β := ℝ) fun (b : β) ↦ (↑(stieltjesOfMeasurableRat f sorry (a, b)) : ℝ → ℝ) (↑(↑q : ℚ) : ℝ)
Tactic: refine Measurable.ennreal_ofReal ?_
-- 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' : ℝ) }
⊢ 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∞)
have neg : Eq (α := ℝ≥0∞)
  (⨅ (b : { r' : ℚ // x < (↑r' : ℝ) }),
      (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞)
        (SProd.sprod (β := Set ℝ) s (Iic (↑(↑b : ℚ) : ℝ))) :
    ℝ≥0∞)
  ((((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) (s ×ˢ Iic x) : ℝ≥0∞)
Tactic: simp_rw [setLIntegral_stieltjesOfMeasurableRat_rat hf _ _ 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' : ℝ) }
⊢ Eq (α := ℝ≥0∞)
    (⨅ (b : { r' : ℚ // x < (↑r' : ℝ) }),
        (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞)
          (SProd.sprod (β := Set ℝ) s (Iic (↑(↑b : ℚ) : ℝ))) :
      ℝ≥0∞)
    ((((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) (s ×ˢ Iic x) : ℝ≥0∞)
have neg : Eq (α := ℝ≥0∞)
  ((((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞)
      (⋂ (i : { r' : ℚ // x < (↑r' : ℝ) }), SProd.sprod (β := Set ℝ) s (Iic (↑(↑i : ℚ) : ℝ))) :
    ℝ≥0∞)
  ((((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) (s ×ˢ Iic x) : ℝ≥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
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∞)
    ((((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞)
        (⋂ (i : { r' : ℚ // x < (↑r' : ℝ) }), SProd.sprod (β := Set ℝ) s (Iic (↑(↑i : ℚ) : ℝ))) :
      ℝ≥0∞)
    ((((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) (s ×ˢ Iic x) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    (⨅ (b : { r' : ℚ // x < (↑r' : ℝ) }),
        (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞)
          (SProd.sprod (β := Set ℝ) s (Iic (↑(↑b : ℚ) : ℝ))) :
      ℝ≥0∞)
    ((((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) (s ×ˢ Iic x) : ℝ≥0∞)
have neg₁ : Monotone.{0, u_2} (β := Set (β × ℝ)) fun (b : { r' : ℚ // x < (↑r' : ℝ) }) ↦
  SProd.sprod (β := Set ℝ) s (Iic (↑(↑b : ℚ) : ℝ))
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
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∞)
    ((((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞)
        (⋂ (i : { r' : ℚ // x < (↑r' : ℝ) }), SProd.sprod (β := Set ℝ) s (Iic (↑(↑i : ℚ) : ℝ))) :
      ℝ≥0∞)
    ((((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) (s ×ˢ Iic x) : ℝ≥0∞)
neg₁ :
  Monotone.{0, u_2} (β := Set (β × ℝ)) fun (b : { r' : ℚ // x < (↑r' : ℝ) }) ↦
    SProd.sprod (β := Set ℝ) s (Iic (↑(↑b : ℚ) : ℝ))
⊢ Eq (α := ℝ≥0∞)
    (⨅ (b : { r' : ℚ // x < (↑r' : ℝ) }),
        (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞)
          (SProd.sprod (β := Set ℝ) s (Iic (↑(↑b : ℚ) : ℝ))) :
      ℝ≥0∞)
    ((((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) (s ×ˢ Iic x) : ℝ≥0∞)
have neg₂ : ∀ (i : { r' : ℚ // x < (↑r' : ℝ) }),
  NullMeasurableSet (SProd.sprod (β := Set ℝ) s (Iic (↑(↑i : ℚ) : ℝ))) ((κ : (a : α) → Measure (β × ℝ)) a)
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
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∞)
    ((((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞)
        (⋂ (i : { r' : ℚ // x < (↑r' : ℝ) }), SProd.sprod (β := Set ℝ) s (Iic (↑(↑i : ℚ) : ℝ))) :
      ℝ≥0∞)
    ((((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) (s ×ˢ Iic x) : ℝ≥0∞)
neg₁ :
  Monotone.{0, u_2} (β := Set (β × ℝ)) fun (b : { r' : ℚ // x < (↑r' : ℝ) }) ↦
    SProd.sprod (β := Set ℝ) s (Iic (↑(↑b : ℚ) : ℝ))
neg₂ :
  ∀ (i : { r' : ℚ // x < (↑r' : ℝ) }),
    NullMeasurableSet (SProd.sprod (β := Set ℝ) s (Iic (↑(↑i : ℚ) : ℝ))) ((κ : (a : α) → Measure (β × ℝ)) a)
⊢ Eq (α := ℝ≥0∞)
    (⨅ (b : { r' : ℚ // x < (↑r' : ℝ) }),
        (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞)
          (SProd.sprod (β := Set ℝ) s (Iic (↑(↑b : ℚ) : ℝ))) :
      ℝ≥0∞)
    ((((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) (s ×ˢ Iic x) : ℝ≥0∞)
have neg₃ : ∃ (i : { r' : ℚ // x < (↑r' : ℝ) }),
  Ne (α := ℝ≥0∞)
    ((((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞)
        (SProd.sprod (β := Set ℝ) s (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
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' : ℝ) }
⊢ Eq (α := ℝ≥0∞)
    ((((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞)
        (⋂ (i : { r' : ℚ // x < (↑r' : ℝ) }), SProd.sprod (β := Set ℝ) s (Iic (↑(↑i : ℚ) : ℝ))) :
      ℝ≥0∞)
    ((((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) (s ×ˢ Iic x) : ℝ≥0∞)
have neg : Eq (α := ℝ≥0∞)
  ((((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞)
      (SProd.sprod (β := Set ℝ) s (⋂ (i : { r' : ℚ // x < (↑r' : ℝ) }), Iic (↑(↑i : ℚ) : ℝ))) :
    ℝ≥0∞)
  ((((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) (s ×ˢ Iic x) : ℝ≥0∞)
Tactic: rw [← prod_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
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' : ℝ) }
⊢ Eq (α := ℝ≥0∞)
    ((((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞)
        (SProd.sprod (β := Set ℝ) s (⋂ (i : { r' : ℚ // x < (↑r' : ℝ) }), Iic (↑(↑i : ℚ) : ℝ))) :
      ℝ≥0∞)
    ((((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) (s ×ˢ Iic x) : ℝ≥0∞)
have neg : ∀ (y : ℝ), Membership.mem (γ := Set ℝ) (⋂ (i : { r' : ℚ // x < (↑r' : ℝ) }), Iic (↑(↑i : ℚ) : ℝ)) y ↔ y ∈ Iic x
Tactic: congr with y
-- 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' : ℝ) }
y : ℝ
⊢ Membership.mem (γ := Set ℝ) (⋂ (i : { r' : ℚ // x < (↑r' : ℝ) }), Iic (↑(↑i : ℚ) : ℝ)) y ↔ y ∈ Iic x
have neg : (∀ (a : ℚ) (b : x < (↑a : ℝ)), y ≤ (↑a : ℝ)) ↔ y ≤ x
Tactic: simp only [mem_iInter, mem_Iic, 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 : ℝ
⊢ ∫⁻ (b : β), ENNReal.ofReal ((↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) x) ∂(ν : (a : α) → Measure β) a =
    (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞)
      (SProd.sprod (α := Set β) univ (Iic x))
have rw : ∫⁻ (x_1 : β) in univ,
    ENNReal.ofReal ((↑(stieltjesOfMeasurableRat f sorry (a, x_1)) : ℝ → ℝ) x) ∂(ν : (a : α) → Measure β) a =
  (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞)
    (SProd.sprod (α := Set β) univ (Iic x))
Tactic: rw [← setLIntegral_univ, setLIntegral_stieltjesOfMeasurableRat hf _ _ MeasurableSet.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 : α × β → ℚ → ℝ
inst : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
x : ℝ
rw :
  ∫⁻ (x_1 : β) in univ,
      ENNReal.ofReal ((↑(stieltjesOfMeasurableRat f ⋯ (a, x_1)) : ℝ → ℝ) x) ∂(ν : (a : α) → Measure β) a =
    (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞)
      (SProd.sprod (α := Set β) univ (Iic x))
⊢ ∫⁻ (b : β), ENNReal.ofReal ((↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) x) ∂(ν : (a : α) → Measure β) a =
    (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞)
      (SProd.sprod (α := Set β) univ (Iic x))
have rw₁ : Eq (α := ℝ≥0∞)
  ((((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞)
      (SProd.sprod (α := Set β) univ (Iic x)) :
    ℝ≥0∞)
  ((((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞)
      (SProd.sprod (α := Set β) univ (Iic x)) :
    ℝ≥0∞)
Tactic: rw [← setLIntegral_univ, setLIntegral_stieltjesOfMeasurableRat hf _ _ MeasurableSet.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 : α × β → ℚ → ℝ
inst : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
x : ℝ
⊢ Eq.{u_2 + 1} (α := (b : β) → ℝ) (fun (b : β) ↦ (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) x) fun (b : β) ↦
    (ENNReal.ofReal ((↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) x)).toReal
have h : ∀ (t : β),
  (↑(stieltjesOfMeasurableRat f sorry (a, t)) : ℝ → ℝ) x =
    (ENNReal.ofReal ((↑(stieltjesOfMeasurableRat f sorry (a, t)) : ℝ → ℝ) x)).toReal
Tactic: ext t
-- 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 : ℝ
t : β
⊢ (↑(stieltjesOfMeasurableRat f ⋯ (a, t)) : ℝ → ℝ) x =
    (ENNReal.ofReal ((↑(stieltjesOfMeasurableRat f ⋯ (a, t)) : ℝ → ℝ) x)).toReal
have h : 0 ≤ (↑(stieltjesOfMeasurableRat f sorry (a, t)) : ℝ → ℝ) x
Tactic: rw [ENNReal.toReal_ofReal]
-- 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 : ℝ
⊢ @Integrable ℝ _ _ _ mβ (fun (b : β) ↦ (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) x)
    ((ν : (a : α) → Measure β) a)
have this : Eq.{u_2 + 1} (α := (b : β) → ℝ) (fun (b : β) ↦ (↑(stieltjesOfMeasurableRat f sorry (a, b)) : ℝ → ℝ) x) fun (b : β) ↦
  (ENNReal.ofReal ((↑(stieltjesOfMeasurableRat f sorry (a, b)) : ℝ → ℝ) x)).toReal
Tactic: have : (fun b ↦ stieltjesOfMeasurableRat f hf.measurable (a, b) x)
      = fun b ↦ (ENNReal.ofReal (stieltjesOfMeasurableRat f hf.measurable (a, b) x)).toReal := by
    ext t
    rw [ENNReal.toReal_ofReal]
    exact stieltjesOfMeasurableRat_nonneg _ _ _
-- 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 : ℝ
this :
  Eq.{u_2 + 1} (α := (b : β) → ℝ) (fun (b : β) ↦ (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) x) fun (b : β) ↦
    (ENNReal.ofReal ((↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) x)).toReal
⊢ @Integrable ℝ _ _ _ mβ (fun (b : β) ↦ (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) x)
    ((ν : (a : α) → Measure β) a)
have rw : @Integrable ℝ _ _ _ mβ (fun (b : β) ↦ (ENNReal.ofReal ((↑(stieltjesOfMeasurableRat f sorry (a, b)) : ℝ → ℝ) x)).toReal)
  ((ν : (a : α) → Measure β) a)
Tactic: rw [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 : ℝ
this :
  Eq.{u_2 + 1} (α := (b : β) → ℝ) (fun (b : β) ↦ (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) x) fun (b : β) ↦
    (ENNReal.ofReal ((↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) x)).toReal
⊢ @Integrable ℝ _ _ _ mβ (fun (b : β) ↦ (ENNReal.ofReal ((↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) x)).toReal)
    ((ν : (a : α) → Measure β) a)
have refine_1 : AEMeasurable (β := ℝ≥0∞) (_m := mβ) (fun (b : β) ↦ ENNReal.ofReal ((↑(stieltjesOfMeasurableRat f sorry (a, b)) : ℝ → ℝ) x))
  ((ν : (a : α) → Measure β) a)
Tactic: refine integrable_toReal_of_lintegral_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 : ℝ
this :
  Eq.{u_2 + 1} (α := (b : β) → ℝ) (fun (b : β) ↦ (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) x) fun (b : β) ↦
    (ENNReal.ofReal ((↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) x)).toReal
refine_1 :
  AEMeasurable (β := ℝ≥0∞) (_m := mβ)
    (fun (b : β) ↦ ENNReal.ofReal ((↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) x)) ((ν : (a : α) → Measure β) a)
⊢ @Integrable ℝ _ _ _ mβ (fun (b : β) ↦ (ENNReal.ofReal ((↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) x)).toReal)
    ((ν : (a : α) → Measure β) a)
have refine_2 : ∫⁻ (x_1 : β), ENNReal.ofReal ((↑(stieltjesOfMeasurableRat f sorry (a, x_1)) : ℝ → ℝ) x) ∂(ν : (a : α) → Measure β) a ≠ ∞
Tactic: refine integrable_toReal_of_lintegral_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 : ℝ
this :
  Eq.{u_2 + 1} (α := (b : β) → ℝ) (fun (b : β) ↦ (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) x) fun (b : β) ↦
    (ENNReal.ofReal ((↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) x)).toReal
⊢ AEMeasurable (β := ℝ≥0∞) (_m := mβ)
    (fun (b : β) ↦ ENNReal.ofReal ((↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) x)) ((ν : (a : α) → Measure β) a)
have refine_1 : Measurable (β := ℝ) fun (b : β) ↦ (↑(stieltjesOfMeasurableRat f sorry (a, b)) : ℝ → ℝ) x
Tactic: refine (Measurable.ennreal_ofReal ?_).aemeasurable
-- 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 : ℝ
this :
  Eq.{u_2 + 1} (α := (b : β) → ℝ) (fun (b : β) ↦ (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) x) fun (b : β) ↦
    (ENNReal.ofReal ((↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) x)).toReal
⊢ ∫⁻ (x_1 : β), ENNReal.ofReal ((↑(stieltjesOfMeasurableRat f ⋯ (a, x_1)) : ℝ → ℝ) x) ∂(ν : (a : α) → Measure β) a ≠ ∞
have refine_2 : Ne (α := ℝ≥0∞)
  ((((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞)
      (SProd.sprod (α := Set β) univ (Iic x)) :
    ℝ≥0∞)
  (∞ : ℝ≥0∞)
Tactic: rw [lintegral_stieltjesOfMeasurableRat hf]