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 : α × β → ℚ → ℝ
hf : IsRatCondKernelCDF f κ ν
a : α
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
⊢ ∀ᵐ (b : β) ∂((ν : (a : α) → Measure β) a : Measure β), Monotone (f (a, b))
have h₁ : ∀ (a_1 : β), IsRatStieltjesPoint f (a, a_1) → Monotone (f (a, a_1))
Tactic: filter_upwards [hf.isRatStieltjesPoint_ae a] with b hb using hb.mono
-- 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 β), Tendsto (f (a, b)) atTop (𝓝 1)
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 : β) ↦ Tendsto (f (a, b)) atTop (𝓝 1)) x} x}
    a_1
Tactic: filter_upwards [hf.isRatStieltjesPoint_ae a] with b hb using hb.tendsto_atTop_one
-- 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 : α
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 : β) ↦ Tendsto (f (a, b)) atTop (𝓝 1)) x} x}
      a_1
⊢ ∀ᵐ (b : β) ∂((ν : (a : α) → Measure β) a : Measure β), Tendsto (f (a, b)) atTop (𝓝 1)
have h₁ : ∀ (a_1 : β), IsRatStieltjesPoint f (a, a_1) → Tendsto (f (a, a_1)) atTop (𝓝 1)
Tactic: filter_upwards [hf.isRatStieltjesPoint_ae a] with b hb using hb.tendsto_atTop_one
-- 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 β), Tendsto (f (a, b)) atBot (𝓝 0)
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 : β) ↦ Tendsto (f (a, b)) atBot (𝓝 0)) x} x}
    a_1
Tactic: filter_upwards [hf.isRatStieltjesPoint_ae a] with b hb using hb.tendsto_atBot_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 : α × β → ℚ → ℝ
hf : IsRatCondKernelCDF f κ ν
a : α
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 : β) ↦ Tendsto (f (a, b)) atBot (𝓝 0)) x} x}
      a_1
⊢ ∀ᵐ (b : β) ∂((ν : (a : α) → Measure β) a : Measure β), Tendsto (f (a, b)) atBot (𝓝 0)
have h₁ : ∀ (a_1 : β), IsRatStieltjesPoint f (a, a_1) → Tendsto (f (a, a_1)) atBot (𝓝 0)
Tactic: filter_upwards [hf.isRatStieltjesPoint_ae a] with b hb using hb.tendsto_atBot_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 : α × β → ℚ → ℝ
hf : IsRatCondKernelCDF f κ ν
a : α
⊢ ∀ᵐ (b : β) ∂((ν : (a : α) → Measure β) a : Measure β),
    ∀ (q : ℚ), ⨅ (r : (↑(Ioi q) : Type)), f (a, b) (↑r : ℚ) = f (a, b) q
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 : β) ↦ ∀ (q : ℚ), ⨅ (r : (↑(Ioi q) : Type)), f (a, b) (↑r : ℚ) = f (a, b) q) x} x}
    a_1
Tactic: filter_upwards [hf.isRatStieltjesPoint_ae a] with b hb using hb.iInf_rat_gt_eq
-- 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 : α
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 : β) ↦ ∀ (q : ℚ), ⨅ (r : (↑(Ioi q) : Type)), f (a, b) (↑r : ℚ) = f (a, b) q) x} x}
      a_1
⊢ ∀ᵐ (b : β) ∂((ν : (a : α) → Measure β) a : Measure β),
    ∀ (q : ℚ), ⨅ (r : (↑(Ioi q) : Type)), f (a, b) (↑r : ℚ) = f (a, b) q
have h₁ : ∀ (a_1 : β), IsRatStieltjesPoint f (a, a_1) → ∀ (q : ℚ), ⨅ (r : (↑(Ioi q) : Type)), f (a, a_1) (↑r : ℚ) = f (a, a_1) q
Tactic: filter_upwards [hf.isRatStieltjesPoint_ae a] with b hb using hb.iInf_rat_gt_eq
-- 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 : α
q : ℚ
⊢ (ae (F := Measure β) ((ν : (a : α) → Measure β) a : Measure β)).EventuallyEq (β := ℝ)
    (fun (b : β) ↦ (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) (↑q : ℝ)) fun (b : β) ↦ f (a, b) q
have h : ∀ (a_1 : β) (ha : IsRatStieltjesPoint f (a, a_1)),
  (↑(stieltjesOfMeasurableRat f sorry (a, a_1)) : ℝ → ℝ) (↑q : ℝ) = f (a, a_1) q
Tactic: filter_upwards [hf.isRatStieltjesPoint_ae a] with a 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 : α × β → ℚ → ℝ
hf : IsRatCondKernelCDF f κ ν
a_1 : α
q : ℚ
a : β
ha : IsRatStieltjesPoint f (a_1, a)
⊢ (↑(stieltjesOfMeasurableRat f ⋯ (a_1, a)) : ℝ → ℝ) (↑q : ℝ) = f (a_1, a) q
have h : toRatCDF f (a_1, a) q = f (a_1, a) q
Tactic: rw [stieltjesOfMeasurableRat_eq, toRatCDF_of_isRatStieltjesPoint 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 : α × β → ℚ → ℝ
hf : IsRatCondKernelCDF f κ ν
a_1 : α
q : ℚ
a : β
ha : IsRatStieltjesPoint f (a_1, a)
h : toRatCDF f (a_1, a) q = f (a_1, a) q
⊢ (↑(stieltjesOfMeasurableRat f ⋯ (a_1, a)) : ℝ → ℝ) (↑q : ℝ) = f (a_1, a) q
have h₁ : f (a_1, a) q = f (a_1, a) q
Tactic: rw [stieltjesOfMeasurableRat_eq, toRatCDF_of_isRatStieltjesPoint 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 : α × β → ℚ → ℝ
hf : IsRatCondKernelCDF f κ ν
a : α
q : ℚ
s : Set β
hs : MeasurableSet s
⊢ (@integral _ _ _ _ mβ (Measure.restrict ((ν : (a : α) → Measure β) a) s) fun (b : β) ↦
      (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) (↑q : ℝ)) =
    Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (β × ℝ)) a)
      (SProd.sprod (β := Set ℝ) s (Iic (↑q : ℝ)))
have rw : ∀ᵐ (x : β) ∂((ν : (a : α) → Measure β) a : Measure β),
  x ∈ s → (↑(stieltjesOfMeasurableRat f sorry (a, x)) : ℝ → ℝ) (↑q : ℝ) = (fun (b : β) ↦ f (a, b) q) x
Tactic: rw [setIntegral_congr_ae hs (g := fun b ↦ f (a, b) q) ?_, hf.setIntegral 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 : α × β → ℚ → ℝ
hf : IsRatCondKernelCDF f κ ν
a : α
q : ℚ
s : Set β
hs : MeasurableSet s
⊢ ∀ᵐ (x : β) ∂((ν : (a : α) → Measure β) a : Measure β),
    x ∈ s → (↑(stieltjesOfMeasurableRat f ⋯ (a, x)) : ℝ → ℝ) (↑q : ℝ) = (fun (b : β) ↦ f (a, b) q) x
have h : ∀ (a_1 : β),
  Membership.mem (γ := Set β)
    {x : β |
      Membership.mem (γ := Set β)
          {x : β |
            (fun (x : β) ↦
                Eq (α := ℝ) ((fun (b : β) ↦ (↑(stieltjesOfMeasurableRat f sorry (a, b)) : ℝ → ℝ) (↑q : ℝ)) x)
                  ((fun (b : β) ↦ f (a, b) q) x))
              x}
          x →
        Membership.mem (γ := Set β)
          {x : β |
            (fun (x : β) ↦
                x ∈ s → (↑(stieltjesOfMeasurableRat f sorry (a, x)) : ℝ → ℝ) (↑q : ℝ) = (fun (b : β) ↦ f (a, b) q) x)
              x}
          x}
    a_1
Tactic: filter_upwards [stieltjesOfMeasurableRat_ae_eq hf a q] with b hb using fun _ ↦ hb
-- 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 : α
q : ℚ
s : Set β
hs : MeasurableSet s
h :
  ∀ (a_1 : β),
    Membership.mem (γ := Set β)
      {x : β |
        Membership.mem (γ := Set β)
            {x : β |
              (fun (x : β) ↦
                  Eq (α := ℝ) ((fun (b : β) ↦ (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) (↑q : ℝ)) x)
                    ((fun (b : β) ↦ f (a, b) q) x))
                x}
            x →
          Membership.mem (γ := Set β)
            {x : β |
              (fun (x : β) ↦
                  x ∈ s → (↑(stieltjesOfMeasurableRat f ⋯ (a, x)) : ℝ → ℝ) (↑q : ℝ) = (fun (b : β) ↦ f (a, b) q) x)
                x}
            x}
      a_1
⊢ ∀ᵐ (x : β) ∂((ν : (a : α) → Measure β) a : Measure β),
    x ∈ s → (↑(stieltjesOfMeasurableRat f ⋯ (a, x)) : ℝ → ℝ) (↑q : ℝ) = (fun (b : β) ↦ f (a, b) q) x
have h₁ : ∀ (a_1 : β),
  (↑(stieltjesOfMeasurableRat f sorry (a, a_1)) : ℝ → ℝ) (↑q : ℝ) = f (a, a_1) q →
    a_1 ∈ s → (↑(stieltjesOfMeasurableRat f sorry (a, a_1)) : ℝ → ℝ) (↑q : ℝ) = f (a, a_1) q
Tactic: filter_upwards [stieltjesOfMeasurableRat_ae_eq hf a q] with b hb using fun _ ↦ hb
-- 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 : α
q : ℚ
s : Set β
hs : MeasurableSet s
⊢ ∫⁻ (b : β) in s,
      ENNReal.ofReal ((↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) (↑q : ℝ)) ∂(ν : (a : α) → Measure β) a =
    (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞)
      (SProd.sprod (β := Set ℝ) s (Iic (↑q : ℝ)))
have rw : ENNReal.ofReal
    (@integral _ _ _ _ mβ (Measure.restrict ((ν : (a : α) → Measure β) a) s) fun (x : β) ↦
      (↑(stieltjesOfMeasurableRat f sorry (a, x)) : ℝ → ℝ) (↑q : ℝ)) =
  (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞)
    (SProd.sprod (β := Set ℝ) s (Iic (↑q : ℝ)))
Tactic: rw [← ofReal_integral_eq_lintegral_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 : α
q : ℚ
s : Set β
hs : MeasurableSet s
rw :
  ENNReal.ofReal
      (@integral _ _ _ _ mβ (Measure.restrict ((ν : (a : α) → Measure β) a) s) fun (x : β) ↦
        (↑(stieltjesOfMeasurableRat f ⋯ (a, x)) : ℝ → ℝ) (↑q : ℝ)) =
    (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞)
      (SProd.sprod (β := Set ℝ) s (Iic (↑q : ℝ)))
⊢ ∫⁻ (b : β) in s,
      ENNReal.ofReal ((↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) (↑q : ℝ)) ∂(ν : (a : α) → Measure β) a =
    (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞)
      (SProd.sprod (β := Set ℝ) s (Iic (↑q : ℝ)))
have hfi : @Integrable ℝ _ _ _ mβ (fun (b : β) ↦ (↑(stieltjesOfMeasurableRat f sorry (a, b)) : ℝ → ℝ) (↑q : ℝ))
  (Measure.restrict ((ν : (a : α) → Measure β) a) s)
Tactic: rw [← ofReal_integral_eq_lintegral_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 : α
q : ℚ
s : Set β
hs : MeasurableSet s
rw :
  ENNReal.ofReal
      (@integral _ _ _ _ mβ (Measure.restrict ((ν : (a : α) → Measure β) a) s) fun (x : β) ↦
        (↑(stieltjesOfMeasurableRat f ⋯ (a, x)) : ℝ → ℝ) (↑q : ℝ)) =
    (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞)
      (SProd.sprod (β := Set ℝ) s (Iic (↑q : ℝ)))
hfi :
  @Integrable ℝ _ _ _ mβ (fun (b : β) ↦ (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) (↑q : ℝ))
    (Measure.restrict ((ν : (a : α) → Measure β) a) s)
⊢ ∫⁻ (b : β) in s,
      ENNReal.ofReal ((↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) (↑q : ℝ)) ∂(ν : (a : α) → Measure β) a =
    (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞)
      (SProd.sprod (β := Set ℝ) s (Iic (↑q : ℝ)))
have f_nn : (ae (F := Measure β) (Measure.restrict ((ν : (a : α) → Measure β) a) s)).EventuallyLE (β := ℝ) 0 fun (b : β) ↦
  (↑(stieltjesOfMeasurableRat f sorry (a, b)) : ℝ → ℝ) (↑q : ℝ)
Tactic: rw [← ofReal_integral_eq_lintegral_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 : α
q : ℚ
s : Set β
hs : MeasurableSet s
⊢ ENNReal.ofReal
      (@integral _ _ _ _ mβ (Measure.restrict ((ν : (a : α) → Measure β) a) s) fun (x : β) ↦
        (↑(stieltjesOfMeasurableRat f ⋯ (a, x)) : ℝ → ℝ) (↑q : ℝ)) =
    (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞)
      (SProd.sprod (β := Set ℝ) s (Iic (↑q : ℝ)))
have rw : ENNReal.ofReal
    (Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (β × ℝ)) a)
      (SProd.sprod (β := Set ℝ) s (Iic (↑q : ℝ)))) =
  (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞)
    (SProd.sprod (β := Set ℝ) s (Iic (↑q : ℝ)))
Tactic: rw [setIntegral_stieltjesOfMeasurableRat_rat hf a q hs, ofReal_measureReal]
-- 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 : α
q : ℚ
s : Set β
hs : MeasurableSet s
rw :
  ENNReal.ofReal
      (Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (β × ℝ)) a)
        (SProd.sprod (β := Set ℝ) s (Iic (↑q : ℝ)))) =
    (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞)
      (SProd.sprod (β := Set ℝ) s (Iic (↑q : ℝ)))
⊢ ENNReal.ofReal
      (@integral _ _ _ _ mβ (Measure.restrict ((ν : (a : α) → Measure β) a) s) fun (x : β) ↦
        (↑(stieltjesOfMeasurableRat f ⋯ (a, x)) : ℝ → ℝ) (↑q : ℝ)) =
    (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞)
      (SProd.sprod (β := Set ℝ) s (Iic (↑q : ℝ)))
have rw₁ : Eq (α := ℝ≥0∞)
  ((((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞)
      (SProd.sprod (β := Set ℝ) s (Iic (↑q : ℝ))) :
    ℝ≥0∞)
  ((((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞)
      (SProd.sprod (β := Set ℝ) s (Iic (↑q : ℝ))) :
    ℝ≥0∞)
Tactic: rw [setIntegral_stieltjesOfMeasurableRat_rat hf a q hs, ofReal_measureReal]
-- 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 : α
q : ℚ
s : Set β
hs : MeasurableSet s
⊢ @Integrable ℝ _ _ _ mβ (fun (b : β) ↦ (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) (↑q : ℝ))
    (Measure.restrict ((ν : (a : α) → Measure β) a) s)
have hfi : @Integrable ℝ _ _ _ mβ (fun (b : β) ↦ (↑(stieltjesOfMeasurableRat f sorry (a, b)) : ℝ → ℝ) (↑q : ℝ))
  ((ν : (a : α) → Measure β) a)
Tactic: refine Integrable.restrict ?_
-- 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 : α
q : ℚ
s : Set β
hs : MeasurableSet s
⊢ @Integrable ℝ _ _ _ mβ (fun (b : β) ↦ (↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) (↑q : ℝ))
    ((ν : (a : α) → Measure β) a)
have hfi : @Integrable ℝ _ _ _ mβ (fun (b : β) ↦ f (a, b) q) ((ν : (a : α) → Measure β) a)
Tactic: rw [integrable_congr (stieltjesOfMeasurableRat_ae_eq hf a 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
⊢ ∫⁻ (b : β) in s, ENNReal.ofReal ((↑(stieltjesOfMeasurableRat f ⋯ (a, b)) : ℝ → ℝ) x) ∂(ν : (a : α) → Measure β) a =
    (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) (s ×ˢ Iic x)
have pos : ∀ (hρ_zero : Eq (α := Measure β) (Measure.restrict ((ν : (a : α) → Measure β) a) s) 0),
  ∫⁻ (b : β) in s, ENNReal.ofReal ((↑(stieltjesOfMeasurableRat f sorry (a, b)) : ℝ → ℝ) x) ∂(ν : (a : α) → Measure β) a =
    (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) (s ×ˢ Iic x)
Tactic: by_cases hρ_zero : (ν a).restrict s = 0
-- 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
pos :
  ∀ (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)
⊢ ∫⁻ (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 : ∀ (hρ_zero : ¬Eq (α := Measure β) (Measure.restrict ((ν : (a : α) → Measure β) a) s) 0),
  ∫⁻ (b : β) in s, ENNReal.ofReal ((↑(stieltjesOfMeasurableRat f sorry (a, b)) : ℝ → ℝ) x) ∂(ν : (a : α) → Measure β) a =
    (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) (s ×ˢ Iic x)
Tactic: by_cases hρ_zero : (ν a).restrict s = 0
-- 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 =
    (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) (s ×ˢ Iic x)
have pos : Eq (α := ℝ≥0∞) (0 : ℝ≥0∞)
  ((((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) (s ×ˢ Iic x) : ℝ≥0∞)
Tactic: rw [hρ_zero, lintegral_zero_measure]
-- 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
⊢ Eq (α := ℝ≥0∞) (0 : ℝ≥0∞)
    ((((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) (s ×ˢ Iic x) : ℝ≥0∞)
have pos : ∀ (q : ℚ) (hq : x < (↑q : ℝ)),
  Eq (α := ℝ≥0∞) (0 : ℝ≥0∞)
    ((((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) (s ×ˢ Iic x) : ℝ≥0∞)
Tactic: have ⟨q, hq⟩ := exists_rat_gt x
-- 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 : ℝ)
this :
  Eq (α := ℝ≥0∞)
    ((((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞)
        (SProd.sprod (β := Set ℝ) s (Iic (↑q : ℝ))) :
      ℝ≥0∞)
    (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (0 : ℝ≥0∞)
    ((((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) (s ×ˢ Iic x) : ℝ≥0∞)
have symm : Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) (s ×ˢ Iic x) : ℝ≥0∞)
  (0 : ℝ≥0∞)
Tactic: symm
-- 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 : ℝ)
this :
  Eq (α := ℝ≥0∞)
    ((((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞)
        (SProd.sprod (β := Set ℝ) s (Iic (↑q : ℝ))) :
      ℝ≥0∞)
    (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    ((((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) (s ×ˢ Iic x) : ℝ≥0∞) (0 : ℝ≥0∞)
have refine : ∀ p ∈ s ×ˢ Iic x, p ∈ SProd.sprod (β := Set ℝ) s (Iic (↑q : ℝ))
Tactic: refine measure_mono_null (fun p ↦ ?_) 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 : ℝ)
this :
  Eq (α := ℝ≥0∞)
    ((((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞)
        (SProd.sprod (β := Set ℝ) s (Iic (↑q : ℝ))) :
      ℝ≥0∞)
    (0 : ℝ≥0∞)
p : β × ℝ
⊢ p ∈ s ×ˢ Iic x → p ∈ SProd.sprod (β := Set ℝ) s (Iic (↑q : ℝ))
have simp : p.1 ∈ s → p.2 ≤ x → p.1 ∈ s ∧ p.2 ≤ (↑q : ℝ)
Tactic: simp only [mem_prod, mem_Iic, and_imp]