awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CondCDF (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
r : ℚ
s : Set α
hs : MeasurableSet s
inst : IsFiniteMeasure ρ
rw : ENNReal.toReal ((ρ.IicSnd (↑r : ℝ) : (a : Set α) → ℝ≥0∞) s) = (ρ.IicSnd (↑r : ℝ)).real s
⊢ (∫⁻ (a : α) in s, preCDF ρ r a ∂ρ.fst).toReal = (ρ.IicSnd (↑r : ℝ)).real s
have rw₁ : ENNReal.toReal ((ρ.IicSnd (↑r : ℝ) : (a : Set α) → ℝ≥0∞) s) =
  ENNReal.toReal ((ρ.IicSnd (↑r : ℝ) : (a : Set α) → ℝ≥0∞) s)
Tactic: rw [setLIntegral_preCDF_fst _ _ hs, measureReal_def]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CondCDF (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
r : ℚ
s : Set α
hs : MeasurableSet s
inst : IsFiniteMeasure ρ
⊢ ∀ᵐ (x : α) ∂ρ.fst.restrict s, preCDF ρ r x < ∞
have hf : ∀ᵐ (x : α) ∂ρ.fst, preCDF ρ r x < ∞
Tactic: refine ae_restrict_of_ae ?_
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CondCDF (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
r : ℚ
s : Set α
hs : MeasurableSet s
inst : IsFiniteMeasure ρ
⊢ ∀ᵐ (x : α) ∂ρ.fst, preCDF ρ r x < ∞
have h : ∀ (a : α) (ha : ∀ (r : ℚ), preCDF ρ r a ≤ 1), preCDF ρ r a < ∞
Tactic: filter_upwards [preCDF_le_one ρ] with a ha
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CondCDF (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
r : ℚ
inst : IsFiniteMeasure ρ
⊢ ∫ (x : α), (preCDF ρ r x).toReal ∂ρ.fst = (ρ.IicSnd (↑r : ℝ)).real univ
have rw : ∫ (x : α) in univ, (preCDF ρ r x).toReal ∂ρ.fst = (ρ.IicSnd (↑r : ℝ)).real univ
Tactic: rw [← setIntegral_univ, setIntegral_preCDF_fst ρ _ MeasurableSet.univ]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CondCDF (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
r : ℚ
inst : IsFiniteMeasure ρ
rw : ∫ (x : α) in univ, (preCDF ρ r x).toReal ∂ρ.fst = (ρ.IicSnd (↑r : ℝ)).real univ
⊢ ∫ (x : α), (preCDF ρ r x).toReal ∂ρ.fst = (ρ.IicSnd (↑r : ℝ)).real univ
have rw₁ : (ρ.IicSnd (↑r : ℝ)).real univ = (ρ.IicSnd (↑r : ℝ)).real univ
Tactic: rw [← setIntegral_univ, setIntegral_preCDF_fst ρ _ MeasurableSet.univ]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CondCDF (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
x : ℚ
⊢ Integrable (ε := ℝ) (fun (a : α) ↦ (preCDF ρ x a).toReal) ρ.fst
have refine_1 : AEStronglyMeasurable (β := ℝ) (fun (a : α) ↦ (preCDF ρ x a).toReal) ρ.fst
Tactic: refine integrable_of_forall_fin_meas_le _ (measure_lt_top ρ.fst univ) ?_ fun t _ _ ↦ ?_
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CondCDF (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
x : ℚ
refine_1 : AEStronglyMeasurable (β := ℝ) (fun (a : α) ↦ (preCDF ρ x a).toReal) ρ.fst
⊢ Integrable (ε := ℝ) (fun (a : α) ↦ (preCDF ρ x a).toReal) ρ.fst
have refine_2 : ∀ (t : Set α),
  MeasurableSet t →
    Ne (α := ℝ≥0∞) ((ρ.fst : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞) →
      ∫⁻ (x_3 : α) in t, ‖(preCDF ρ x x_3).toReal‖ₑ ∂ρ.fst ≤ (ρ.fst : (a : Set α) → ℝ≥0∞) univ
Tactic: refine integrable_of_forall_fin_meas_le _ (measure_lt_top ρ.fst univ) ?_ fun t _ _ ↦ ?_
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CondCDF (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
x : ℚ
t : Set α
h : MeasurableSet t
h_1 : Ne (α := ℝ≥0∞) ((ρ.fst : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∫⁻ (x_1 : α) in t, ‖(preCDF ρ x x_1).toReal‖ₑ ∂ρ.fst ≤ (ρ.fst : (a : Set α) → ℝ≥0∞) univ
have refine_2 : ∫⁻ (x_1 : α) in t, ENNReal.ofReal (preCDF ρ x x_1).toReal ∂ρ.fst ≤ (ρ.fst : (a : Set α) → ℝ≥0∞) univ
Tactic: simp_rw [← ofReal_norm, Real.norm_of_nonneg ENNReal.toReal_nonneg]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CondCDF (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
x : ℚ
t : Set α
h : MeasurableSet t
h_1 : Ne (α := ℝ≥0∞) ((ρ.fst : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∫⁻ (x_1 : α) in t, ENNReal.ofReal (preCDF ρ x x_1).toReal ∂ρ.fst ≤ (ρ.fst : (a : Set α) → ℝ≥0∞) univ
have refine_2 : ∫⁻ (x_1 : α) in t, ENNReal.ofReal (preCDF ρ x x_1).toReal ∂ρ.fst ≤ ∫⁻ (x : α), 1 ∂ρ.fst
Tactic: rw [← lintegral_one]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CondCDF (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
x : ℚ
t : Set α
h : MeasurableSet t
h_1 : Ne (α := ℝ≥0∞) ((ρ.fst : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∫⁻ (x_1 : α) in t, ENNReal.ofReal (preCDF ρ x x_1).toReal ∂ρ.fst ≤ ∫⁻ (x : α), 1 ∂ρ.fst
have refine_2 : ∀ᵐ (a : α) ∂ρ.fst, ENNReal.ofReal (preCDF ρ x a).toReal ≤ 1
Tactic: refine (setLIntegral_le_lintegral _ _).trans (lintegral_mono_ae ?_)
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CondCDF (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
x : ℚ
t : Set α
h : MeasurableSet t
h_1 : Ne (α := ℝ≥0∞) ((ρ.fst : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∀ᵐ (a : α) ∂ρ.fst, ENNReal.ofReal (preCDF ρ x a).toReal ≤ 1
have h : ∀ (a : α),
  Membership.mem (γ := Set α)
    {x_1 : α |
      Membership.mem (γ := Set α) {x : α | (fun (a : α) ↦ ∀ (r : ℚ), preCDF ρ r a ≤ 1) x} x_1 →
        Membership.mem (γ := Set α) {x_2 : α | (fun (a : α) ↦ ENNReal.ofReal (preCDF ρ x a).toReal ≤ 1) x_2} x_1}
    a
Tactic: filter_upwards [preCDF_le_one ρ] with a ha using ENNReal.ofReal_toReal_le.trans (ha _)
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CondCDF (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
x : ℚ
t : Set α
h_1 : MeasurableSet t
h_2 : Ne (α := ℝ≥0∞) ((ρ.fst : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
h :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x_1 : α |
        Membership.mem (γ := Set α) {x : α | (fun (a : α) ↦ ∀ (r : ℚ), preCDF ρ r a ≤ 1) x} x_1 →
          Membership.mem (γ := Set α) {x_2 : α | (fun (a : α) ↦ ENNReal.ofReal (preCDF ρ x a).toReal ≤ 1) x_2} x_1}
      a
⊢ ∀ᵐ (a : α) ∂ρ.fst, ENNReal.ofReal (preCDF ρ x a).toReal ≤ 1
have h₁ : ∀ (a : α), (∀ (r : ℚ), preCDF ρ r a ≤ 1) → ENNReal.ofReal (preCDF ρ x a).toReal ≤ 1
Tactic: filter_upwards [preCDF_le_one ρ] with a ha using ENNReal.ofReal_toReal_le.trans (ha _)
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CondCDF (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
a : Unit
r r' : ℚ
hrr' : r ≤ r'
⊢ ∀ᵐ (c : α) ∂((Kernel.const Unit ρ.fst : (a : Unit) → Measure α) a : Measure α),
    (preCDF ρ r (a, c).2).toReal ≤ (preCDF ρ r' (a, c).2).toReal
have h : ∀ (a : α) (h₁ : Monotone (β := ℝ≥0∞) fun (r : ℚ) ↦ preCDF ρ r a) (h₂ : ∀ (r : ℚ), preCDF ρ r a ≤ 1),
  (preCDF ρ r a).toReal ≤ (preCDF ρ r' a).toReal
Tactic: filter_upwards [monotone_preCDF ρ, preCDF_le_one ρ] with a h₁ h₂
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CondCDF (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
a : Unit
q : ℚ
⊢ ∀ᵐ (c : α) ∂((Kernel.const Unit ρ.fst : (a : Unit) → Measure α) a : Measure α), (preCDF ρ q (a, c).2).toReal ≤ 1
have simp : ∀ᵐ (c : α) ∂ρ.fst, (preCDF ρ q c).toReal ≤ 1
Tactic: simp only [Kernel.const_apply]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CondCDF (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
a : Unit
q : ℚ
⊢ ∀ᵐ (c : α) ∂ρ.fst, (preCDF ρ q c).toReal ≤ 1
have h : ∀ (a : α) (ha : ∀ (r : ℚ), preCDF ρ r a ≤ 1), (preCDF ρ q a).toReal ≤ 1
Tactic: filter_upwards [preCDF_le_one ρ] with a ha
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CondCDF (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
a_1 : Unit
q : ℚ
a : α
ha : ∀ (r : ℚ), preCDF ρ r a ≤ 1
⊢ (preCDF ρ q a).toReal ≤ 1
have h : preCDF ρ q a ≤ ENNReal.ofReal 1
Tactic: refine ENNReal.toReal_le_of_le_ofReal zero_le_one ?_
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CondCDF (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
a : Unit
s : ℕ → ℚ
h : Antitone s
hs_tendsto : Tendsto s atTop atBot
⊢ Tendsto (β := ℝ)
    (fun (m : ℕ) ↦
      @integral _ _ _ _ mα ((Kernel.const Unit ρ.fst : (a : Unit) → Measure α) a) fun (c : α) ↦
        (preCDF ρ (s m) (a, c).2).toReal)
    atTop (𝓝 0)
have simp_rw : Tendsto (β := ℝ) (fun (m : ℕ) ↦ (ρ.IicSnd (↑(s m) : ℝ)).real univ) atTop (𝓝 0)
Tactic: simp_rw [Kernel.const_apply, integral_preCDF_fst ρ]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CondCDF (hypothesis)
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
a : Unit
s : ℕ → ℚ
h : Antitone s
hs_tendsto : Tendsto s atTop atBot
⊢ Tendsto (β := ℝ) (fun (m : ℕ) ↦ (ρ.IicSnd (↑(s m) : ℝ)).real univ) atTop (𝓝 0)
have h : Tendsto (β := ℝ≥0∞) (fun (r : ℚ) ↦ (ρ.IicSnd (↑r : ℝ) : (a : Set α) → ℝ≥0∞) univ) atBot (𝓝 0)
Tactic: have h := ρ.tendsto_IicSnd_atBot MeasurableSet.univ
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CondCDF (hypothesis)
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
a : Unit
s : ℕ → ℚ
h_1 : Antitone s
hs_tendsto : Tendsto s atTop atBot
h : Tendsto (β := ℝ≥0∞) (fun (r : ℚ) ↦ (ρ.IicSnd (↑r : ℝ) : (a : Set α) → ℝ≥0∞) univ) atBot (𝓝 0)
⊢ Tendsto (fun (m : ℕ) ↦ (ρ.IicSnd (↑(s m) : ℝ)).real univ) atTop (𝓝 (ENNReal.toReal 0))
have h0 : Tendsto ENNReal.toReal (𝓝 0) (𝓝 0)
Tactic: have h0 : Tendsto ENNReal.toReal (𝓝 0) (𝓝 0) :=
      ENNReal.continuousAt_toReal ENNReal.zero_ne_top
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CondCDF (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
a : Unit
s : ℕ → ℚ
h : Monotone s
hs_tendsto : Tendsto s atTop atTop
⊢ Tendsto
    (fun (m : ℕ) ↦
      @integral _ _ _ _ mα ((Kernel.const Unit ρ.fst : (a : Unit) → Measure α) a) fun (c : α) ↦
        (preCDF ρ (s m) (a, c).2).toReal)
    atTop (𝓝 (Measure.real.{u_1} (α := α) (m := mα) ((Kernel.const Unit ρ.fst : (a : Unit) → Measure α) a) univ))
have simp_rw : Tendsto (fun (m : ℕ) ↦ (ρ.IicSnd (↑(s m) : ℝ)).real univ) atTop (𝓝 (ρ.fst.real univ))
Tactic: simp_rw [Kernel.const_apply, integral_preCDF_fst ρ]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CondCDF (hypothesis)
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
a : Unit
s : ℕ → ℚ
h : Monotone s
hs_tendsto : Tendsto s atTop atTop
⊢ Tendsto (fun (m : ℕ) ↦ (ρ.IicSnd (↑(s m) : ℝ)).real univ) atTop (𝓝 (ρ.fst.real univ))
have h : Tendsto (β := ℝ≥0∞) (fun (r : ℚ) ↦ ((ρ.IicSnd (↑r : ℝ) : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)) atTop
  (𝓝 ((ρ.fst : (a : Set α) → ℝ≥0∞) univ) : Filter ℝ≥0∞)
Tactic: have h := ρ.tendsto_IicSnd_atTop MeasurableSet.univ
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CondCDF (hypothesis)
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
a : Unit
s : ℕ → ℚ
h_1 : Monotone s
hs_tendsto : Tendsto s atTop atTop
h :
  Tendsto (β := ℝ≥0∞) (fun (r : ℚ) ↦ ((ρ.IicSnd (↑r : ℝ) : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)) atTop
    (𝓝 ((ρ.fst : (a : Set α) → ℝ≥0∞) univ) : Filter ℝ≥0∞)
⊢ Tendsto (fun (m : ℕ) ↦ (ρ.IicSnd (↑(s m) : ℝ)).real univ) atTop (𝓝 (ρ.fst.real univ))
have h0 : Tendsto ENNReal.toReal (𝓝 ((ρ.fst : (a : Set α) → ℝ≥0∞) univ)) (𝓝 (ρ.fst.real univ))
Tactic: have h0 : Tendsto ENNReal.toReal (𝓝 (ρ.fst univ)) (𝓝 (ρ.fst.real univ)) :=
      ENNReal.continuousAt_toReal (measure_ne_top _ _)
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CondCDF (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
a : Unit
s : Set α
hs : MeasurableSet s
q : ℚ
⊢ (@integral _ _ _ _ mα (Measure.restrict ((Kernel.const Unit ρ.fst : (a : Unit) → Measure α) a) s) fun (c : α) ↦
      (preCDF ρ q (a, c).2).toReal) =
    Measure.real (m := Prod.instMeasurableSpace) ((Kernel.const Unit ρ : (a : Unit) → Measure (α × ℝ)) a)
      (SProd.sprod (β := Set ℝ) s (Iic (↑q : ℝ)))
have rw : ∫ (c : α) in s, (preCDF ρ q (a, c).2).toReal ∂ρ.fst =
  Measure.real (m := Prod.instMeasurableSpace) ((Kernel.const Unit ρ : (a : Unit) → Measure (α × ℝ)) a)
    (SProd.sprod (β := Set ℝ) s (Iic (↑q : ℝ)))
Tactic: rw [Kernel.const_apply, Kernel.const_apply,
    setIntegral_preCDF_fst _ _ hs, measureReal_def, measureReal_def, Measure.IicSnd_apply _ _ hs]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CondCDF (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
a : Unit
s : Set α
hs : MeasurableSet s
q : ℚ
rw :
  ∫ (c : α) in s, (preCDF ρ q (a, c).2).toReal ∂ρ.fst =
    Measure.real (m := Prod.instMeasurableSpace) ((Kernel.const Unit ρ : (a : Unit) → Measure (α × ℝ)) a)
      (SProd.sprod (β := Set ℝ) s (Iic (↑q : ℝ)))
⊢ (@integral _ _ _ _ mα (Measure.restrict ((Kernel.const Unit ρ.fst : (a : Unit) → Measure α) a) s) fun (c : α) ↦
      (preCDF ρ q (a, c).2).toReal) =
    Measure.real (m := Prod.instMeasurableSpace) ((Kernel.const Unit ρ : (a : Unit) → Measure (α × ℝ)) a)
      (SProd.sprod (β := Set ℝ) s (Iic (↑q : ℝ)))
have rw₁ : ∫ (c : α) in s, (preCDF ρ q (a, c).2).toReal ∂ρ.fst = ρ.real (SProd.sprod (β := Set ℝ) s (Iic (↑q : ℝ)))
Tactic: rw [Kernel.const_apply, Kernel.const_apply,
    setIntegral_preCDF_fst _ _ hs, measureReal_def, measureReal_def, Measure.IicSnd_apply _ _ hs]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CondCDF (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
a : Unit
s : Set α
hs : MeasurableSet s
q : ℚ
rw :
  ∫ (c : α) in s, (preCDF ρ q (a, c).2).toReal ∂ρ.fst =
    Measure.real (m := Prod.instMeasurableSpace) ((Kernel.const Unit ρ : (a : Unit) → Measure (α × ℝ)) a)
      (SProd.sprod (β := Set ℝ) s (Iic (↑q : ℝ)))
rw₁ : ∫ (c : α) in s, (preCDF ρ q (a, c).2).toReal ∂ρ.fst = ρ.real (SProd.sprod (β := Set ℝ) s (Iic (↑q : ℝ)))
⊢ (@integral _ _ _ _ mα (Measure.restrict ((Kernel.const Unit ρ.fst : (a : Unit) → Measure α) a) s) fun (c : α) ↦
      (preCDF ρ q (a, c).2).toReal) =
    Measure.real (m := Prod.instMeasurableSpace) ((Kernel.const Unit ρ : (a : Unit) → Measure (α × ℝ)) a)
      (SProd.sprod (β := Set ℝ) s (Iic (↑q : ℝ)))
have rw₂ : (ρ.IicSnd (↑q : ℝ)).real s = ρ.real (SProd.sprod (β := Set ℝ) s (Iic (↑q : ℝ)))
Tactic: rw [Kernel.const_apply, Kernel.const_apply,
    setIntegral_preCDF_fst _ _ hs, measureReal_def, measureReal_def, Measure.IicSnd_apply _ _ hs]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CondCDF (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
a : Unit
s : Set α
hs : MeasurableSet s
q : ℚ
rw :
  ∫ (c : α) in s, (preCDF ρ q (a, c).2).toReal ∂ρ.fst =
    Measure.real (m := Prod.instMeasurableSpace) ((Kernel.const Unit ρ : (a : Unit) → Measure (α × ℝ)) a)
      (SProd.sprod (β := Set ℝ) s (Iic (↑q : ℝ)))
rw₁ : ∫ (c : α) in s, (preCDF ρ q (a, c).2).toReal ∂ρ.fst = ρ.real (SProd.sprod (β := Set ℝ) s (Iic (↑q : ℝ)))
rw₂ : (ρ.IicSnd (↑q : ℝ)).real s = ρ.real (SProd.sprod (β := Set ℝ) s (Iic (↑q : ℝ)))
⊢ (@integral _ _ _ _ mα (Measure.restrict ((Kernel.const Unit ρ.fst : (a : Unit) → Measure α) a) s) fun (c : α) ↦
      (preCDF ρ q (a, c).2).toReal) =
    Measure.real (m := Prod.instMeasurableSpace) ((Kernel.const Unit ρ : (a : Unit) → Measure (α × ℝ)) a)
      (SProd.sprod (β := Set ℝ) s (Iic (↑q : ℝ)))
have rw₃ : ENNReal.toReal ((ρ.IicSnd (↑q : ℝ) : (a : Set α) → ℝ≥0∞) s) = ρ.real (SProd.sprod (β := Set ℝ) s (Iic (↑q : ℝ)))
Tactic: rw [Kernel.const_apply, Kernel.const_apply,
    setIntegral_preCDF_fst _ _ hs, measureReal_def, measureReal_def, Measure.IicSnd_apply _ _ hs]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CondCDF (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
a : Unit
s : Set α
hs : MeasurableSet s
q : ℚ
rw :
  ∫ (c : α) in s, (preCDF ρ q (a, c).2).toReal ∂ρ.fst =
    Measure.real (m := Prod.instMeasurableSpace) ((Kernel.const Unit ρ : (a : Unit) → Measure (α × ℝ)) a)
      (SProd.sprod (β := Set ℝ) s (Iic (↑q : ℝ)))
rw₁ : ∫ (c : α) in s, (preCDF ρ q (a, c).2).toReal ∂ρ.fst = ρ.real (SProd.sprod (β := Set ℝ) s (Iic (↑q : ℝ)))
rw₂ : (ρ.IicSnd (↑q : ℝ)).real s = ρ.real (SProd.sprod (β := Set ℝ) s (Iic (↑q : ℝ)))
rw₃ : ENNReal.toReal ((ρ.IicSnd (↑q : ℝ) : (a : Set α) → ℝ≥0∞) s) = ρ.real (SProd.sprod (β := Set ℝ) s (Iic (↑q : ℝ)))
⊢ (@integral _ _ _ _ mα (Measure.restrict ((Kernel.const Unit ρ.fst : (a : Unit) → Measure α) a) s) fun (c : α) ↦
      (preCDF ρ q (a, c).2).toReal) =
    Measure.real (m := Prod.instMeasurableSpace) ((Kernel.const Unit ρ : (a : Unit) → Measure (α × ℝ)) a)
      (SProd.sprod (β := Set ℝ) s (Iic (↑q : ℝ)))
have rw₄ : ENNReal.toReal ((ρ.IicSnd (↑q : ℝ) : (a : Set α) → ℝ≥0∞) s) =
  ENNReal.toReal ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s (Iic (↑q : ℝ))))
Tactic: rw [Kernel.const_apply, Kernel.const_apply,
    setIntegral_preCDF_fst _ _ hs, measureReal_def, measureReal_def, Measure.IicSnd_apply _ _ hs]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CondCDF (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
a : Unit
s : Set α
hs : MeasurableSet s
q : ℚ
rw :
  ∫ (c : α) in s, (preCDF ρ q (a, c).2).toReal ∂ρ.fst =
    Measure.real (m := Prod.instMeasurableSpace) ((Kernel.const Unit ρ : (a : Unit) → Measure (α × ℝ)) a)
      (SProd.sprod (β := Set ℝ) s (Iic (↑q : ℝ)))
rw₁ : ∫ (c : α) in s, (preCDF ρ q (a, c).2).toReal ∂ρ.fst = ρ.real (SProd.sprod (β := Set ℝ) s (Iic (↑q : ℝ)))
rw₂ : (ρ.IicSnd (↑q : ℝ)).real s = ρ.real (SProd.sprod (β := Set ℝ) s (Iic (↑q : ℝ)))
rw₃ : ENNReal.toReal ((ρ.IicSnd (↑q : ℝ) : (a : Set α) → ℝ≥0∞) s) = ρ.real (SProd.sprod (β := Set ℝ) s (Iic (↑q : ℝ)))
rw₄ :
  ENNReal.toReal ((ρ.IicSnd (↑q : ℝ) : (a : Set α) → ℝ≥0∞) s) =
    ENNReal.toReal ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s (Iic (↑q : ℝ))))
⊢ (@integral _ _ _ _ mα (Measure.restrict ((Kernel.const Unit ρ.fst : (a : Unit) → Measure α) a) s) fun (c : α) ↦
      (preCDF ρ q (a, c).2).toReal) =
    Measure.real (m := Prod.instMeasurableSpace) ((Kernel.const Unit ρ : (a : Unit) → Measure (α × ℝ)) a)
      (SProd.sprod (β := Set ℝ) s (Iic (↑q : ℝ)))
have rw₅ : ENNReal.toReal ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s (Iic (↑q : ℝ)))) =
  ENNReal.toReal ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s (Iic (↑q : ℝ))))
Tactic: rw [Kernel.const_apply, Kernel.const_apply,
    setIntegral_preCDF_fst _ _ hs, measureReal_def, measureReal_def, Measure.IicSnd_apply _ _ hs]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CondCDF (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
a : α
⊢ condCDF ρ a = stieltjesOfMeasurableRat (fun (p : Unit × α) (r : ℚ) ↦ (preCDF ρ r p.2).toReal) ⋯ ((), a)
have h : ∀ (x : ℝ),
  (↑(condCDF ρ a) : ℝ → ℝ) x =
    (↑(stieltjesOfMeasurableRat (fun (p : Unit × α) (r : ℚ) ↦ (preCDF ρ r p.2).toReal) sorry ((), a)) : ℝ → ℝ) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CondCDF (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
a : α
x : ℝ
⊢ (↑(condCDF ρ a) : ℝ → ℝ) x =
    (↑(stieltjesOfMeasurableRat (fun (p : Unit × α) (r : ℚ) ↦ (preCDF ρ r p.2).toReal) ⋯ ((), a)) : ℝ → ℝ) x
have h : (↑(stieltjesOfMeasurableRat (fun (a : α) (r : ℚ) ↦ (preCDF ρ r a).toReal) sorry a) : ℝ → ℝ) x =
  (↑(stieltjesOfMeasurableRat (fun (p : Unit × α) (r : ℚ) ↦ (preCDF ρ r p.2).toReal) sorry ((), a)) : ℝ → ℝ) x
Tactic: rw [condCDF, ← stieltjesOfMeasurableRat_unit_prod]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CondCDF (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
a : α
x : ℝ
h :
  (↑(stieltjesOfMeasurableRat (fun (a : α) (r : ℚ) ↦ (preCDF ρ r a).toReal) ⋯ a) : ℝ → ℝ) x =
    (↑(stieltjesOfMeasurableRat (fun (p : Unit × α) (r : ℚ) ↦ (preCDF ρ r p.2).toReal) ⋯ ((), a)) : ℝ → ℝ) x
⊢ (↑(condCDF ρ a) : ℝ → ℝ) x =
    (↑(stieltjesOfMeasurableRat (fun (p : Unit × α) (r : ℚ) ↦ (preCDF ρ r p.2).toReal) ⋯ ((), a)) : ℝ → ℝ) x
have h₁ : (↑(stieltjesOfMeasurableRat (fun (p : Unit × α) (r : ℚ) ↦ (preCDF ρ r p.2).toReal) sorry ((), a)) : ℝ → ℝ) x =
  (↑(stieltjesOfMeasurableRat (fun (p : Unit × α) (r : ℚ) ↦ (preCDF ρ r p.2).toReal) sorry ((), a)) : ℝ → ℝ) x
Tactic: rw [condCDF, ← stieltjesOfMeasurableRat_unit_prod]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CondCDF (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
⊢ IsCondKernelCDF (mα := PUnit.instMeasurableSpace) (fun (p : Unit × α) ↦ condCDF ρ p.2) (Kernel.const Unit ρ)
    (Kernel.const Unit ρ.fst)
have simp_rw : IsCondKernelCDF (mα := PUnit.instMeasurableSpace)
  (fun (p : Unit × α) ↦ stieltjesOfMeasurableRat (fun (p : Unit × α) (r : ℚ) ↦ (preCDF ρ r p.2).toReal) sorry ((), p.2))
  (Kernel.const Unit ρ) (Kernel.const Unit ρ.fst)
Tactic: simp_rw [condCDF_eq_stieltjesOfMeasurableRat_unit_prod ρ]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CondCDF (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
r : ℚ
⊢ (ae ρ.fst).EventuallyEq (β := ℝ) (fun (a : α) ↦ (↑(condCDF ρ a) : ℝ → ℝ) (↑r : ℝ)) fun (a : α) ↦ (preCDF ρ r a).toReal
have simp_rw : (ae ρ.fst).EventuallyEq (β := ℝ)
  (fun (a : α) ↦
    (↑(stieltjesOfMeasurableRat (fun (p : Unit × α) (r : ℚ) ↦ (preCDF ρ r p.2).toReal) sorry ((), a)) : ℝ → ℝ) (↑r : ℝ))
  fun (a : α) ↦ (preCDF ρ r a).toReal
Tactic: simp_rw [condCDF_eq_stieltjesOfMeasurableRat_unit_prod ρ]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CondCDF (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
r : ℚ
⊢ (fun (a : α) ↦ ENNReal.ofReal ((↑(condCDF ρ a) : ℝ → ℝ) (↑r : ℝ))) =ᶠ[ae ρ.fst] preCDF ρ r
have h : ∀ (a : α) (ha : (↑(condCDF ρ a) : ℝ → ℝ) (↑r : ℝ) = (preCDF ρ r a).toReal) (ha_le_one : ∀ (r : ℚ), preCDF ρ r a ≤ 1),
  ENNReal.ofReal ((↑(condCDF ρ a) : ℝ → ℝ) (↑r : ℝ)) = preCDF ρ r a
Tactic: filter_upwards [condCDF_ae_eq ρ r, preCDF_le_one ρ] with a ha ha_le_one
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CondCDF (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
r : ℚ
a : α
ha : (↑(condCDF ρ a) : ℝ → ℝ) (↑r : ℝ) = (preCDF ρ r a).toReal
ha_le_one : ∀ (r : ℚ), preCDF ρ r a ≤ 1
⊢ ENNReal.ofReal ((↑(condCDF ρ a) : ℝ → ℝ) (↑r : ℝ)) = preCDF ρ r a
have h : preCDF ρ r a ≠ ∞
Tactic: rw [ha, ENNReal.ofReal_toReal]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CondCDF (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
a : α
x : ℝ
⊢ ((condCDF ρ a).measure : (a : Set ℝ) → ℝ≥0∞) (Iic x) = ENNReal.ofReal ((↑(condCDF ρ a) : ℝ → ℝ) x)
have rw : ((condCDF ρ a).measure : (a : Set ℝ) → ℝ≥0∞) (Iic x) = ENNReal.ofReal ((↑(condCDF ρ a) : ℝ → ℝ) x - 0)
Tactic: rw [← sub_zero (condCDF ρ a x)]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CondCDF (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
a : α
⊢ Eq (α := ℝ≥0∞) (((condCDF ρ a).measure : (a : Set ℝ) → ℝ≥0∞) univ : ℝ≥0∞) (1 : ℝ≥0∞)
have rw : ((condCDF ρ a).measure : (a : Set ℝ) → ℝ≥0∞) univ = ENNReal.ofReal (HSub.hSub (α := ℝ) 1 0)
Tactic: rw [← ENNReal.ofReal_one, ← sub_zero (1 : ℝ)]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CondCDF (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
⊢ ∀ (s : Set ℝ),
    Membership.mem (γ := Set (Set ℝ)) (range Iic) s →
      Measurable (β := ℝ≥0∞) fun (a : α) ↦ ((condCDF ρ a).measure : (a : Set ℝ) → ℝ≥0∞) s
have simp_rw : ∀ (i : ℝ), Measurable (β := ℝ≥0∞) fun (a : α) ↦ ENNReal.ofReal ((↑(condCDF ρ a) : ℝ → ℝ) i)
Tactic: simp_rw [forall_mem_range, measure_condCDF_Iic]