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 : IsRatCondKernelCDFAux f κ ν
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel ν
a : α
q : ℚ
s : Set β
hs : MeasurableSet s
h : LT.lt (α := ℝ≥0∞) ((((ν : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
refine_3 :
  (@integral _ _ _ _ mβ (Measure.restrict ((ν : (a : α) → Measure β) a) s) fun (x : β) ↦
      ⨅ (r : (↑(Ioi q) : Type)), f (a, x) (↑r : ℚ)) =
    Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (β × ℝ)) a)
      (SProd.sprod (β := Set ℝ) s (Iic (↑q : ℝ)))
⊢ Eq (α := ℝ)
    (@integral _ _ _ _ mβ (Measure.restrict ((ν : (a : α) → Measure β) a) s) fun (x : β) ↦
      ⨅ (r : (↑(Ioi q) : Type)), f (a, x) (↑r : ℚ))
    (@integral _ _ _ _ mβ (Measure.restrict ((ν : (a : α) → Measure β) a) s) fun (x : β) ↦ f (a, x) q)
have refine_3₁ : Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (β × ℝ)) a)
    (SProd.sprod (β := Set ℝ) s (Iic (↑q : ℝ))) =
  Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (β × ℝ)) a)
    (SProd.sprod (β := Set ℝ) s (Iic (↑q : ℝ)))
Tactic: rw [hf.setIntegral _ hs, hf.setIntegral_iInf_rat_gt _ _ 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 : IsRatCondKernelCDFAux f κ ν
inst : IsFiniteKernel κ
inst_1 : IsFiniteKernel ν
a : α
⊢ ∀ᵐ (t : β) ∂((ν : (a : α) → Measure β) a : Measure β), IsRatStieltjesPoint f (a, t)
have h : ∀ (t : β) (ht_top : Tendsto (f (a, t)) atTop (𝓝 1)) (ht_bot : Tendsto (f (a, t)) atBot (𝓝 0))
  (ht_iInf : ∀ (q : ℚ), ⨅ (r : (↑(Ioi q) : Type)), f (a, t) (↑r : ℚ) = f (a, t) q) (h_mono : Monotone (f (a, t))),
  IsRatStieltjesPoint f (a, t)
Tactic: filter_upwards [hf.tendsto_atTop_one a, hf.tendsto_atBot_zero a,
    hf.iInf_rat_gt_eq a, hf.mono a] with t ht_top ht_bot ht_iInf h_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 : α × β → StieltjesFunction ℝ
hf : IsCondKernelCDF f κ ν
a : α
x : ℝ
⊢ (@MeasureTheory.integral _ _ _ _ mβ ((ν : (a : α) → Measure β) a) fun (b : β) ↦ (↑(f (a, b)) : ℝ → ℝ) x) =
    Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (β × ℝ)) a)
      (SProd.sprod (α := Set β) univ (Iic x))
have rw : Eq (α := ℝ) (@MeasureTheory.integral _ _ _ _ mβ ((ν : (a : α) → Measure β) a) fun (b : β) ↦ (↑(f (a, b)) : ℝ → ℝ) x)
  (@MeasureTheory.integral _ _ _ _ mβ (Measure.restrict ((ν : (a : α) → Measure β) a) univ) fun (b : β) ↦
    (↑(f (a, b)) : ℝ → ℝ) x)
Tactic: rw [← hf.setIntegral _ MeasurableSet.univ, Measure.restrict_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 ℝ
hf : IsCondKernelCDF f κ ν
a : α
x : ℝ
rw :
  Eq (α := ℝ) (@MeasureTheory.integral _ _ _ _ mβ ((ν : (a : α) → Measure β) a) fun (b : β) ↦ (↑(f (a, b)) : ℝ → ℝ) x)
    (@MeasureTheory.integral _ _ _ _ mβ (Measure.restrict ((ν : (a : α) → Measure β) a) univ) fun (b : β) ↦
      (↑(f (a, b)) : ℝ → ℝ) x)
⊢ (@MeasureTheory.integral _ _ _ _ mβ ((ν : (a : α) → Measure β) a) fun (b : β) ↦ (↑(f (a, b)) : ℝ → ℝ) x) =
    Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (β × ℝ)) a)
      (SProd.sprod (α := Set β) univ (Iic x))
have rw₁ : Eq (α := ℝ) (@MeasureTheory.integral _ _ _ _ mβ ((ν : (a : α) → Measure β) a) fun (b : β) ↦ (↑(f (a, b)) : ℝ → ℝ) x)
  (@MeasureTheory.integral _ _ _ _ mβ ((ν : (a : α) → Measure β) a) fun (b : β) ↦ (↑(f (a, b)) : ℝ → ℝ) x)
Tactic: rw [← hf.setIntegral _ MeasurableSet.univ, Measure.restrict_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 α β
inst : IsFiniteKernel κ
f : α × β → StieltjesFunction ℝ
hf : IsCondKernelCDF f κ ν
a : α
s : Set β
hs : MeasurableSet s
x : ℝ
⊢ ∫⁻ (b : β) in s, ENNReal.ofReal ((↑(f (a, b)) : ℝ → ℝ) x) ∂(ν : (a : α) → Measure β) a =
    (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) (s ×ˢ Iic x)
have rw : ENNReal.ofReal
    (@MeasureTheory.integral _ _ _ _ mβ (Measure.restrict ((ν : (a : α) → Measure β) a) s) fun (x_1 : β) ↦
      (↑(f (a, x_1)) : ℝ → ℝ) x) =
  (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) (s ×ˢ Iic x)
Tactic: rw [← ofReal_integral_eq_lintegral_ofReal (hf.integrable a x).restrict
    (ae_of_all _ (fun _ ↦ hf.nonneg _ _)), hf.setIntegral a hs x, 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 α β
inst : IsFiniteKernel κ
f : α × β → StieltjesFunction ℝ
hf : IsCondKernelCDF f κ ν
a : α
s : Set β
hs : MeasurableSet s
x : ℝ
rw :
  ENNReal.ofReal
      (@MeasureTheory.integral _ _ _ _ mβ (Measure.restrict ((ν : (a : α) → Measure β) a) s) fun (x_1 : β) ↦
        (↑(f (a, x_1)) : ℝ → ℝ) x) =
    (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) (s ×ˢ Iic x)
⊢ ∫⁻ (b : β) in s, ENNReal.ofReal ((↑(f (a, b)) : ℝ → ℝ) x) ∂(ν : (a : α) → Measure β) a =
    (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) (s ×ˢ Iic x)
have rw₁ : ENNReal.ofReal (Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (β × ℝ)) a) (s ×ˢ Iic x)) =
  (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) (s ×ˢ Iic x)
Tactic: rw [← ofReal_integral_eq_lintegral_ofReal (hf.integrable a x).restrict
    (ae_of_all _ (fun _ ↦ hf.nonneg _ _)), hf.setIntegral a hs x, 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 α β
inst : IsFiniteKernel κ
f : α × β → StieltjesFunction ℝ
hf : IsCondKernelCDF f κ ν
a : α
s : Set β
hs : MeasurableSet s
x : ℝ
rw :
  ENNReal.ofReal
      (@MeasureTheory.integral _ _ _ _ mβ (Measure.restrict ((ν : (a : α) → Measure β) a) s) fun (x_1 : β) ↦
        (↑(f (a, x_1)) : ℝ → ℝ) x) =
    (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) (s ×ˢ Iic x)
rw₁ :
  ENNReal.ofReal (Measure.real (m := Prod.instMeasurableSpace) ((κ : (a : α) → Measure (β × ℝ)) a) (s ×ˢ Iic x)) =
    (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) (s ×ˢ Iic x)
⊢ ∫⁻ (b : β) in s, ENNReal.ofReal ((↑(f (a, b)) : ℝ → ℝ) x) ∂(ν : (a : α) → Measure β) a =
    (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) (s ×ˢ Iic x)
have rw₂ : Eq (α := ℝ≥0∞) ((((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) (s ×ˢ Iic x) : ℝ≥0∞)
  ((((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) (s ×ˢ Iic x) : ℝ≥0∞)
Tactic: rw [← ofReal_integral_eq_lintegral_ofReal (hf.integrable a x).restrict
    (ae_of_all _ (fun _ ↦ hf.nonneg _ _)), hf.setIntegral a hs x, 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 α β
inst : IsFiniteKernel κ
f : α × β → StieltjesFunction ℝ
hf : IsCondKernelCDF f κ ν
a : α
x : ℝ
⊢ ∫⁻ (b : β), ENNReal.ofReal ((↑(f (a, b)) : ℝ → ℝ) x) ∂(ν : (a : α) → Measure β) a =
    (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞)
      (SProd.sprod (α := Set β) univ (Iic x))
have rw : ∫⁻ (b : β), ENNReal.ofReal ((↑(f (a, b)) : ℝ → ℝ) x) ∂(ν : (a : α) → Measure β) a =
  ∫⁻ (b : β) in univ, ENNReal.ofReal ((↑(f (a, b)) : ℝ → ℝ) x) ∂(ν : (a : α) → Measure β) a
Tactic: rw [← hf.setLIntegral _ MeasurableSet.univ, Measure.restrict_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 α β
inst : IsFiniteKernel κ
f : α × β → StieltjesFunction ℝ
hf : IsCondKernelCDF f κ ν
a : α
x : ℝ
rw :
  ∫⁻ (b : β), ENNReal.ofReal ((↑(f (a, b)) : ℝ → ℝ) x) ∂(ν : (a : α) → Measure β) a =
    ∫⁻ (b : β) in univ, ENNReal.ofReal ((↑(f (a, b)) : ℝ → ℝ) x) ∂(ν : (a : α) → Measure β) a
⊢ ∫⁻ (b : β), ENNReal.ofReal ((↑(f (a, b)) : ℝ → ℝ) x) ∂(ν : (a : α) → Measure β) a =
    (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞)
      (SProd.sprod (α := Set β) univ (Iic x))
have rw₁ : ∫⁻ (b : β), ENNReal.ofReal ((↑(f (a, b)) : ℝ → ℝ) x) ∂(ν : (a : α) → Measure β) a =
  ∫⁻ (b : β), ENNReal.ofReal ((↑(f (a, b)) : ℝ → ℝ) x) ∂(ν : (a : α) → Measure β) a
Tactic: rw [← hf.setLIntegral _ MeasurableSet.univ, Measure.restrict_univ]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CDFToKernel (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
x_1 : MeasurableSpace β
f : α × β → StieltjesFunction ℝ
κ : Kernel.{u_1, u_2} α (β × ℝ)
ν : Kernel α β
hf : IsCondKernelCDF f κ ν
p : α × β
x : ℝ
⊢ (((toKernel f hf : (a : α × β) → Measure ℝ) p : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (Iic x) =
    ENNReal.ofReal ((↑(f p) : ℝ → ℝ) x)
have rw : ENNReal.ofReal ((↑(f p) : ℝ → ℝ) x - 0) = ENNReal.ofReal ((↑(f p) : ℝ → ℝ) x)
Tactic: rw [IsCondKernelCDF.toKernel_apply p, (f p).measure_Iic (hf.tendsto_atBot_zero p)]
-- 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 : α
x : ℝ
s : Set β
hs : MeasurableSet s
⊢ ∫⁻ (b : β) in s,
      (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, b) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
        (Iic x) ∂(ν : (a : α) → Measure β) a =
    (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) (s ×ˢ Iic x)
have simp_rw : ∫⁻ (b : β) in s, ENNReal.ofReal ((↑(f (a, b)) : ℝ → ℝ) x) ∂(ν : (a : α) → Measure β) a =
  (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) (s ×ˢ Iic x)
Tactic: simp_rw [IsCondKernelCDF.toKernel_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 : α × β → StieltjesFunction ℝ
inst : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a : α
s : Set β
hs : MeasurableSet s
⊢ ∫⁻ (b : β) in s,
      (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, b) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
        univ ∂(ν : (a : α) → Measure β) a =
    (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s univ)
have rw : ∫⁻ (b : β) in s,
    (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, b) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
      (⋃ (r : ℚ), Iic (↑r : ℝ)) ∂(ν : (a : α) → Measure β) a =
  (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞)
    (⋃ (i : ℚ), SProd.sprod (β := Set ℝ) s (Iic (↑i : ℝ)))
Tactic: rw [← Real.iUnion_Iic_rat, prod_iUnion]
-- 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 β
hs : MeasurableSet s
⊢ Directed (fun (x y : Set ℝ) ↦ x ⊆ y) fun (q : ℚ) ↦ Iic (↑q : ℝ)
have refine : ∀ (r r' : ℚ) (hrr' : r ≤ r'), LE.le (α := ℝ) (↑r : ℝ) (↑r' : ℝ)
Tactic: refine Monotone.directed_le fun r r' hrr' ↦ Iic_subset_Iic.mpr ?_
-- 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 β
hs : MeasurableSet s
⊢ ∫⁻ (b : β) in s,
      (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, b) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
        (⋃ (r : ℚ), Iic (↑r : ℝ)) ∂(ν : (a : α) → Measure β) a =
    (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞)
      (⋃ (i : ℚ), SProd.sprod (β := Set ℝ) s (Iic (↑i : ℝ)))
have h_dir : Directed (fun (x y : Set ℝ) ↦ x ⊆ y) fun (q : ℚ) ↦ Iic (↑q : ℝ)
Tactic: have h_dir : Directed (fun x y ↦ x ⊆ y) fun q : ℚ ↦ Iic (q : ℝ) := by
    refine Monotone.directed_le fun r r' hrr' ↦ Iic_subset_Iic.mpr ?_
    exact mod_cast hrr'
-- 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 β
hs : MeasurableSet s
h_dir : Directed (fun (x y : Set ℝ) ↦ x ⊆ y) fun (q : ℚ) ↦ Iic (↑q : ℝ)
⊢ Directed (fun (x y : Set (β × ℝ)) ↦ x ⊆ y) fun (q : ℚ) ↦ SProd.sprod (β := Set ℝ) s (Iic (↑q : ℝ))
have refine : ∀ (i j : ℚ) (hij : i ≤ j), SProd.sprod (β := Set ℝ) s (Iic (↑i : ℝ)) ≤ SProd.sprod (β := Set ℝ) s (Iic (↑j : ℝ))
Tactic: refine Monotone.directed_le fun i j hij ↦ ?_
-- 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 β
hs : MeasurableSet s
h_dir : Directed (fun (x y : Set ℝ) ↦ x ⊆ y) fun (q : ℚ) ↦ Iic (↑q : ℝ)
i j : ℚ
hij : i ≤ j
⊢ SProd.sprod (β := Set ℝ) s (Iic (↑i : ℝ)) ≤ SProd.sprod (β := Set ℝ) s (Iic (↑j : ℝ))
have refine : LE.le (α := ℝ) (↑i : ℝ) (↑j : ℝ)
Tactic: refine prod_subset_prod_iff.mpr (Or.inl ⟨subset_rfl, Iic_subset_Iic.mpr ?_⟩)
-- 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 β
hs : MeasurableSet s
h_dir : Directed (fun (x y : Set ℝ) ↦ x ⊆ y) fun (q : ℚ) ↦ Iic (↑q : ℝ)
⊢ ∫⁻ (b : β) in s,
      (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, b) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
        (⋃ (r : ℚ), Iic (↑r : ℝ)) ∂(ν : (a : α) → Measure β) a =
    (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞)
      (⋃ (i : ℚ), SProd.sprod (β := Set ℝ) s (Iic (↑i : ℝ)))
have h_dir_prod : Directed (fun (x y : Set (β × ℝ)) ↦ x ⊆ y) fun (q : ℚ) ↦ SProd.sprod (β := Set ℝ) s (Iic (↑q : ℝ))
Tactic: have h_dir_prod : Directed (fun x y ↦ x ⊆ y) fun q : ℚ ↦ s ×ˢ Iic (q : ℝ) := by
    refine Monotone.directed_le fun i j hij ↦ ?_
    refine prod_subset_prod_iff.mpr (Or.inl ⟨subset_rfl, Iic_subset_Iic.mpr ?_⟩)
    exact mod_cast hij
-- 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 β
hs : MeasurableSet s
h_dir : Directed (fun (x y : Set ℝ) ↦ x ⊆ y) fun (q : ℚ) ↦ Iic (↑q : ℝ)
h_dir_prod : Directed (fun (x y : Set (β × ℝ)) ↦ x ⊆ y) fun (q : ℚ) ↦ SProd.sprod (β := Set ℝ) s (Iic (↑q : ℝ))
⊢ ∫⁻ (b : β) in s,
      (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, b) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
        (⋃ (r : ℚ), Iic (↑r : ℝ)) ∂(ν : (a : α) → Measure β) a =
    (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞)
      (⋃ (i : ℚ), SProd.sprod (β := Set ℝ) s (Iic (↑i : ℝ)))
have simp_rw : ∫⁻ (b : β) in s,
    ⨆ (i : ℚ),
      (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, b) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
        (Iic (↑i : ℝ)) ∂(ν : (a : α) → Measure β) a =
  ⨆ (i : ℚ),
    (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞)
      (SProd.sprod (β := Set ℝ) s (Iic (↑i : ℝ)))
Tactic: simp_rw [h_dir.measure_iUnion, h_dir_prod.measure_iUnion]
-- 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 β
hs : MeasurableSet s
h_dir : Directed (fun (x y : Set ℝ) ↦ x ⊆ y) fun (q : ℚ) ↦ Iic (↑q : ℝ)
h_dir_prod : Directed (fun (x y : Set (β × ℝ)) ↦ x ⊆ y) fun (q : ℚ) ↦ SProd.sprod (β := Set ℝ) s (Iic (↑q : ℝ))
⊢ ∫⁻ (b : β) in s,
      ⨆ (i : ℚ),
        (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, b) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
          (Iic (↑i : ℝ)) ∂(ν : (a : α) → Measure β) a =
    ⨆ (i : ℚ),
      (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞)
        (SProd.sprod (β := Set ℝ) s (Iic (↑i : ℝ)))
have rw : Eq (α := ℝ≥0∞)
  (⨆ (b : ℚ),
    ∫⁻ (a_1 : β) in s,
      (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, a_1) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
        (Iic (↑b : ℝ)) ∂(ν : (a : α) → Measure β) a)
  (⨆ (i : ℚ),
    (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞)
      (SProd.sprod (β := Set ℝ) s (Iic (↑i : ℝ))))
Tactic: rw [lintegral_iSup_directed]
-- 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 β
hs : MeasurableSet s
h_dir : Directed (fun (x y : Set ℝ) ↦ x ⊆ y) fun (q : ℚ) ↦ Iic (↑q : ℝ)
h_dir_prod : Directed (fun (x y : Set (β × ℝ)) ↦ x ⊆ y) fun (q : ℚ) ↦ SProd.sprod (β := Set ℝ) s (Iic (↑q : ℝ))
rw :
  Eq (α := ℝ≥0∞)
    (⨆ (b : ℚ),
      ∫⁻ (a_1 : β) in s,
        (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, a_1) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
          (Iic (↑b : ℝ)) ∂(ν : (a : α) → Measure β) a)
    (⨆ (i : ℚ),
      (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞)
        (SProd.sprod (β := Set ℝ) s (Iic (↑i : ℝ))))
⊢ ∫⁻ (b : β) in s,
      ⨆ (i : ℚ),
        (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, b) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
          (Iic (↑i : ℝ)) ∂(ν : (a : α) → Measure β) a =
    ⨆ (i : ℚ),
      (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞)
        (SProd.sprod (β := Set ℝ) s (Iic (↑i : ℝ)))
have hf₁ : ∀ (b : ℚ),
  AEMeasurable (β := ℝ≥0∞) (_m := mβ)
    (fun (b_1 : β) ↦
      (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, b_1) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
        (Iic (↑b : ℝ)))
    (Measure.restrict ((ν : (a : α) → Measure β) a) s)
Tactic: rw [lintegral_iSup_directed]
-- 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 β
hs : MeasurableSet s
h_dir : Directed (fun (x y : Set ℝ) ↦ x ⊆ y) fun (q : ℚ) ↦ Iic (↑q : ℝ)
h_dir_prod : Directed (fun (x y : Set (β × ℝ)) ↦ x ⊆ y) fun (q : ℚ) ↦ SProd.sprod (β := Set ℝ) s (Iic (↑q : ℝ))
rw :
  Eq (α := ℝ≥0∞)
    (⨆ (b : ℚ),
      ∫⁻ (a_1 : β) in s,
        (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, a_1) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
          (Iic (↑b : ℝ)) ∂(ν : (a : α) → Measure β) a)
    (⨆ (i : ℚ),
      (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞)
        (SProd.sprod (β := Set ℝ) s (Iic (↑i : ℝ))))
hf₁ :
  ∀ (b : ℚ),
    AEMeasurable (β := ℝ≥0∞) (_m := mβ)
      (fun (b_1 : β) ↦
        (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, b_1) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
          (Iic (↑b : ℝ)))
      (Measure.restrict ((ν : (a : α) → Measure β) a) s)
⊢ ∫⁻ (b : β) in s,
      ⨆ (i : ℚ),
        (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, b) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
          (Iic (↑i : ℝ)) ∂(ν : (a : α) → Measure β) a =
    ⨆ (i : ℚ),
      (((κ : (a : α) → Measure (β × ℝ)) a : Measure (β × ℝ)) : (a : Set (β × ℝ)) → ℝ≥0∞)
        (SProd.sprod (β := Set ℝ) s (Iic (↑i : ℝ)))
have h_directed : Directed (fun (x1 x2 : β → ℝ≥0∞) ↦ x1 ≤ x2) fun (i : ℚ) (b : β) ↦
  (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, b) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (Iic (↑i : ℝ))
Tactic: rw [lintegral_iSup_directed]
-- 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 β
hs : MeasurableSet s
h_dir : Directed (fun (x y : Set ℝ) ↦ x ⊆ y) fun (q : ℚ) ↦ Iic (↑q : ℝ)
h_dir_prod : Directed (fun (x y : Set (β × ℝ)) ↦ x ⊆ y) fun (q : ℚ) ↦ SProd.sprod (β := Set ℝ) s (Iic (↑q : ℝ))
⊢ ∀ (b : ℚ),
    AEMeasurable (β := ℝ≥0∞) (_m := mβ)
      (fun (b_1 : β) ↦
        (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, b_1) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞)
          (Iic (↑b : ℝ)))
      (Measure.restrict ((ν : (a : α) → Measure β) a) s)
have hf₁ : ∀ (q : ℚ),
  Measurable (β := ℝ≥0∞) fun (b : β) ↦
    (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, b) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (Iic (↑q : ℝ))
Tactic: refine fun q ↦ Measurable.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 : α × β → StieltjesFunction ℝ
inst : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a : α
s : Set β
hs : MeasurableSet s
h_dir : Directed (fun (x y : Set ℝ) ↦ x ⊆ y) fun (q : ℚ) ↦ Iic (↑q : ℝ)
h_dir_prod : Directed (fun (x y : Set (β × ℝ)) ↦ x ⊆ y) fun (q : ℚ) ↦ SProd.sprod (β := Set ℝ) s (Iic (↑q : ℝ))
⊢ Directed (fun (x1 x2 : β → ℝ≥0∞) ↦ x1 ≤ x2) fun (i : ℚ) (b : β) ↦
    (((IsCondKernelCDF.toKernel f hf : (a : α × β) → Measure ℝ) (a, b) : Measure ℝ) : (a : Set ℝ) → ℝ≥0∞) (Iic (↑i : ℝ))
have h_directed : ∀ (i j : ℚ) (hij : i ≤ j) (t : β), LE.le (α := ℝ) (↑i : ℝ) (↑j : ℝ)
Tactic: refine Monotone.directed_le fun i j hij t ↦ measure_mono (Iic_subset_Iic.mpr ?_)