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 (α × ℝ)
s : Set α
hs : MeasurableSet s
⊢ Tendsto (β := ℝ≥0∞) (fun (r : ℚ) ↦ ((ρ.IicSnd (↑r : ℝ) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)) atTop
    (𝓝 ((ρ.fst : (a : Set α) → ℝ≥0∞) s) : Filter ℝ≥0∞)
have simp_rw : Tendsto (β := ℝ≥0∞) (fun (r : ℚ) ↦ ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s (Iic (↑r : ℝ))) : ℝ≥0∞))
  atTop (𝓝 ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s univ)) : Filter ℝ≥0∞)
Tactic: simp_rw [ρ.IicSnd_apply _ hs, fst_apply hs, ← prod_univ]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CondCDF (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
s : Set α
hs : MeasurableSet s
⊢ Tendsto (β := ℝ≥0∞)
    (fun (r : ℚ) ↦ ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s (Iic (↑r : ℝ))) : ℝ≥0∞)) atTop
    (𝓝 ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s univ)) : Filter ℝ≥0∞)
have rw : Tendsto (β := ℝ≥0∞) (fun (r : ℚ) ↦ ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s (Iic (↑r : ℝ))) : ℝ≥0∞))
  atTop (𝓝 ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (⋃ (i : ℚ), SProd.sprod (β := Set ℝ) s (Iic (↑i : ℝ)))) : Filter ℝ≥0∞)
Tactic: rw [← Real.iUnion_Iic_rat, prod_iUnion]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CondCDF (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
s : Set α
hs : MeasurableSet s
⊢ Tendsto (β := ℝ≥0∞)
    (fun (r : ℚ) ↦ ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s (Iic (↑r : ℝ))) : ℝ≥0∞)) atTop
    (𝓝 ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (⋃ (i : ℚ), SProd.sprod (β := Set ℝ) s (Iic (↑i : ℝ)))) : Filter ℝ≥0∞)
have hm : Monotone.{0, u_1} (β := Set (α × ℝ)) fun (r : ℚ) ↦ SProd.sprod (β := Set ℝ) s (Iic (↑r : ℝ))
Tactic: apply tendsto_measure_iUnion_atTop
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CondCDF (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
⊢ Tendsto (β := ℝ≥0∞) (fun (r : ℚ) ↦ (ρ.IicSnd (↑r : ℝ) : (a : Set α) → ℝ≥0∞) s) atBot (𝓝 0)
have simp_rw : Tendsto (β := ℝ≥0∞) (fun (r : ℚ) ↦ (ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s (Iic (↑r : ℝ)))) atBot
  (𝓝 0)
Tactic: simp_rw [ρ.IicSnd_apply _ hs]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CondCDF (hypothesis)
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
⊢ Tendsto (β := ℝ≥0∞) (fun (r : ℚ) ↦ (ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s (Iic (↑r : ℝ)))) atBot
    (𝓝 0)
have h_empty : Eq (α := ℝ≥0∞) ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s ∅) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: have h_empty : ρ (s ×ˢ ∅) = 0 := by simp only [prod_empty, measure_empty]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CondCDF (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
h_empty : Eq (α := ℝ≥0∞) ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s ∅) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Tendsto (β := ℝ≥0∞) (fun (r : ℚ) ↦ (ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s (Iic (↑r : ℝ)))) atBot
    (𝓝 0)
have rw : Tendsto (β := ℝ≥0∞) (fun (r : ℚ) ↦ ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s (Iic (↑r : ℝ))) : ℝ≥0∞))
  atBot (𝓝 ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (⋂ (i : ℚ), SProd.sprod (β := Set ℝ) s (Iic (↑i : ℝ)))) : Filter ℝ≥0∞)
Tactic: rw [← h_empty, ← Real.iInter_Iic_rat, prod_iInter]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CondCDF (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
h_empty : Eq (α := ℝ≥0∞) ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s ∅) : ℝ≥0∞) (0 : ℝ≥0∞)
h_neg :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℚ) ↦ ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s (Iic (↑(-r) : ℝ))) : ℝ≥0∞)) atTop
    (𝓝 ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (⋂ (r : ℚ), SProd.sprod (β := Set ℝ) s (Iic (↑(-r) : ℝ)))) : Filter ℝ≥0∞)
⊢ Eq.{u_1 + 1} (α := Set (α × ℝ)) (⋂ (r : ℚ), SProd.sprod (β := Set ℝ) s (Iic (↑(-r) : ℝ)))
    (⋂ (r : ℚ), SProd.sprod (β := Set ℝ) s (Iic (↑r : ℝ)))
have h : ∀ (x : α × ℝ),
  Membership.mem (γ := Set (α × ℝ)) (⋂ (r : ℚ), SProd.sprod (β := Set ℝ) s (Iic (↑(-r) : ℝ))) x ↔
    Membership.mem (γ := Set (α × ℝ)) (⋂ (r : ℚ), SProd.sprod (β := Set ℝ) s (Iic (↑r : ℝ))) x
Tactic: ext1 x
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CondCDF (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
h_empty : Eq (α := ℝ≥0∞) ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s ∅) : ℝ≥0∞) (0 : ℝ≥0∞)
h_neg :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℚ) ↦ ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s (Iic (↑(-r) : ℝ))) : ℝ≥0∞)) atTop
    (𝓝 ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (⋂ (r : ℚ), SProd.sprod (β := Set ℝ) s (Iic (↑(-r) : ℝ)))) : Filter ℝ≥0∞)
x : α × ℝ
⊢ Membership.mem (γ := Set (α × ℝ)) (⋂ (r : ℚ), SProd.sprod (β := Set ℝ) s (Iic (↑(-r) : ℝ))) x ↔
    Membership.mem (γ := Set (α × ℝ)) (⋂ (r : ℚ), SProd.sprod (β := Set ℝ) s (Iic (↑r : ℝ))) x
have h : (∀ (i : ℚ), x.1 ∈ s ∧ x.2 ≤ (↑(-i) : ℝ)) ↔ ∀ (i : ℚ), x.1 ∈ s ∧ x.2 ≤ (↑i : ℝ)
Tactic: push _ ∈ _
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CondCDF (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
h_empty : Eq (α := ℝ≥0∞) ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s ∅) : ℝ≥0∞) (0 : ℝ≥0∞)
h_neg :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℚ) ↦ ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s (Iic (↑(-r) : ℝ))) : ℝ≥0∞)) atTop
    (𝓝 ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (⋂ (r : ℚ), SProd.sprod (β := Set ℝ) s (Iic (↑(-r) : ℝ)))) : Filter ℝ≥0∞)
x : α × ℝ
⊢ (∀ (i : ℚ), x.1 ∈ s ∧ x.2 ≤ (↑(-i) : ℝ)) ↔ ∀ (i : ℚ), x.1 ∈ s ∧ x.2 ≤ (↑i : ℝ)
have h : ∀ (h : ∀ (i : ℚ), x.1 ∈ s ∧ x.2 ≤ (↑(-i) : ℝ)) (i : ℚ), x.2 ≤ (↑i : ℝ)
Tactic: refine ⟨fun h i ↦ ⟨(h i).1, ?_⟩, fun h i ↦ ⟨(h i).1, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CondCDF (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
h_empty : Eq (α := ℝ≥0∞) ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s ∅) : ℝ≥0∞) (0 : ℝ≥0∞)
h_neg :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℚ) ↦ ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s (Iic (↑(-r) : ℝ))) : ℝ≥0∞)) atTop
    (𝓝 ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (⋂ (r : ℚ), SProd.sprod (β := Set ℝ) s (Iic (↑(-r) : ℝ)))) : Filter ℝ≥0∞)
x : α × ℝ
h : ∀ (h : ∀ (i : ℚ), x.1 ∈ s ∧ x.2 ≤ (↑(-i) : ℝ)) (i : ℚ), x.2 ≤ (↑i : ℝ)
⊢ (∀ (i : ℚ), x.1 ∈ s ∧ x.2 ≤ (↑(-i) : ℝ)) ↔ ∀ (i : ℚ), x.1 ∈ s ∧ x.2 ≤ (↑i : ℝ)
have h₁ : ∀ (h : ∀ (i : ℚ), x.1 ∈ s ∧ x.2 ≤ (↑i : ℝ)) (i : ℚ), x.2 ≤ (↑(-i) : ℝ)
Tactic: refine ⟨fun h i ↦ ⟨(h i).1, ?_⟩, fun h i ↦ ⟨(h i).1, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CondCDF (hypothesis)
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
h_empty : Eq (α := ℝ≥0∞) ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s ∅) : ℝ≥0∞) (0 : ℝ≥0∞)
h_neg :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℚ) ↦ ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s (Iic (↑(-r) : ℝ))) : ℝ≥0∞)) atTop
    (𝓝 ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (⋂ (r : ℚ), SProd.sprod (β := Set ℝ) s (Iic (↑(-r) : ℝ)))) : Filter ℝ≥0∞)
x : α × ℝ
h : ∀ (i : ℚ), x.1 ∈ s ∧ x.2 ≤ (↑(-i) : ℝ)
i : ℚ
⊢ x.2 ≤ (↑i : ℝ)
have h' : x.1 ∈ s ∧ x.2 ≤ (↑(- -i) : ℝ)
Tactic: have h' := h (-i)
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CondCDF (hypothesis)
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
h_empty : Eq (α := ℝ≥0∞) ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s ∅) : ℝ≥0∞) (0 : ℝ≥0∞)
h_neg :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℚ) ↦ ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s (Iic (↑(-r) : ℝ))) : ℝ≥0∞)) atTop
    (𝓝 ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (⋂ (r : ℚ), SProd.sprod (β := Set ℝ) s (Iic (↑(-r) : ℝ)))) : Filter ℝ≥0∞)
x : α × ℝ
h : ∀ (i : ℚ), x.1 ∈ s ∧ x.2 ≤ (↑i : ℝ)
i : ℚ
⊢ x.2 ≤ (↑(-i) : ℝ)
have h' : x.1 ∈ s ∧ x.2 ≤ (↑(-i) : ℝ)
Tactic: have h' := h (-i)
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CondCDF (hypothesis)
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
h_empty : Eq (α := ℝ≥0∞) ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s ∅) : ℝ≥0∞) (0 : ℝ≥0∞)
h_neg :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℚ) ↦ ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s (Iic (↑(-r) : ℝ))) : ℝ≥0∞)) atTop
    (𝓝 ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (⋂ (r : ℚ), SProd.sprod (β := Set ℝ) s (Iic (↑(-r) : ℝ)))) : Filter ℝ≥0∞)
x : α × ℝ
h : ∀ (i : ℚ), x.1 ∈ s ∧ x.2 ≤ (↑(-i) : ℝ)
i : ℚ
h' : x.1 ∈ s ∧ x.2 ≤ (↑(- -i) : ℝ)
⊢ x.2 ≤ (↑i : ℝ)
have h'₁ : x.1 ∈ s ∧ x.2 ≤ (↑i : ℝ)
Tactic: rw [neg_neg] at h'
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CondCDF (hypothesis)
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
h_empty : Eq (α := ℝ≥0∞) ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s ∅) : ℝ≥0∞) (0 : ℝ≥0∞)
h_neg :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℚ) ↦ ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s (Iic (↑(-r) : ℝ))) : ℝ≥0∞)) atTop
    (𝓝 ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (⋂ (r : ℚ), SProd.sprod (β := Set ℝ) s (Iic (↑(-r) : ℝ)))) : Filter ℝ≥0∞)
⊢ Tendsto (β := ℝ≥0∞)
    (fun (r : ℚ) ↦ ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s (Iic (↑r : ℝ))) : ℝ≥0∞)) atBot
    (𝓝 ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (⋂ (i : ℚ), SProd.sprod (β := Set ℝ) s (Iic (↑i : ℝ)))) : Filter ℝ≥0∞)
have h_inter_eq : Eq.{u_1 + 1} (α := Set (α × ℝ)) (⋂ (r : ℚ), SProd.sprod (β := Set ℝ) s (Iic (↑(-r) : ℝ)))
  (⋂ (r : ℚ), SProd.sprod (β := Set ℝ) s (Iic (↑r : ℝ)))
Tactic: have h_inter_eq : ⋂ r : ℚ, s ×ˢ Iic ↑(-r) = ⋂ r : ℚ, s ×ˢ Iic (r : ℝ) := by
      ext1 x
      push _ ∈ _
      refine ⟨fun h i ↦ ⟨(h i).1, ?_⟩, fun h i ↦ ⟨(h i).1, ?_⟩⟩ <;> have h' := h (-i)
      · rw [neg_neg] at h'; exact h'.2
      · exact h'.2
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CondCDF (hypothesis)
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
h_empty : Eq (α := ℝ≥0∞) ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s ∅) : ℝ≥0∞) (0 : ℝ≥0∞)
h_neg :
  Tendsto (β := ℝ≥0∞)
    (fun (r : ℚ) ↦ ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s (Iic (↑(-r) : ℝ))) : ℝ≥0∞)) atTop
    (𝓝 ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (⋂ (r : ℚ), SProd.sprod (β := Set ℝ) s (Iic (↑(-r) : ℝ)))) : Filter ℝ≥0∞)
h_inter_eq :
  Eq.{u_1 + 1} (α := Set (α × ℝ)) (⋂ (r : ℚ), SProd.sprod (β := Set ℝ) s (Iic (↑(-r) : ℝ)))
    (⋂ (r : ℚ), SProd.sprod (β := Set ℝ) s (Iic (↑r : ℝ)))
⊢ Tendsto (β := ℝ≥0∞)
    (fun (r : ℚ) ↦ ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s (Iic (↑r : ℝ))) : ℝ≥0∞)) atBot
    (𝓝 ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (⋂ (i : ℚ), SProd.sprod (β := Set ℝ) s (Iic (↑i : ℝ)))) : Filter ℝ≥0∞)
have h_neg₁ : Tendsto (β := ℝ≥0∞)
  (fun (r : ℚ) ↦ ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s (Iic (↑(-r) : ℝ))) : ℝ≥0∞)) atTop
  (𝓝 ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (⋂ (r : ℚ), SProd.sprod (β := Set ℝ) s (Iic (↑r : ℝ)))) : Filter ℝ≥0∞)
Tactic: rw [h_inter_eq] at h_neg
Cleared hypotheses: h_neg, h_inter_eq
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CondCDF (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
h_empty : Eq (α := ℝ≥0∞) ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s ∅) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Tendsto (β := ℝ≥0∞)
    (fun (r : ℚ) ↦ ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s (Iic (↑r : ℝ))) : ℝ≥0∞)) atBot
    (𝓝 ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (⋂ (i : ℚ), SProd.sprod (β := Set ℝ) s (Iic (↑i : ℝ)))) : Filter ℝ≥0∞)
have suffices : Tendsto (β := ℝ≥0∞)
  (fun (r : ℚ) ↦ ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s (Iic (↑(-r) : ℝ))) : ℝ≥0∞)) atTop
  (𝓝 ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (⋂ (r : ℚ), SProd.sprod (β := Set ℝ) s (Iic (↑(-r) : ℝ)))) : Filter ℝ≥0∞)
Tactic: suffices h_neg :
      Tendsto (fun r : ℚ ↦ ρ (s ×ˢ Iic ↑(-r))) atTop (𝓝 (ρ (⋂ r : ℚ, s ×ˢ Iic ↑(-r)))) by
    have h_inter_eq : ⋂ r : ℚ, s ×ˢ Iic ↑(-r) = ⋂ r : ℚ, s ×ˢ Iic (r : ℝ) := by
      ext1 x
      push _ ∈ _
      refine ⟨fun h i ↦ ⟨(h i).1, ?_⟩, fun h i ↦ ⟨(h i).1, ?_⟩⟩ <;> have h' := h (-i)
      · rw [neg_neg] at h'; exact h'.2
      · exact h'.2
    rw [h_inter_eq] at h_neg
    exact tendsto_comp_neg_atTop_iff.mp h_neg
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CondCDF (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
h_empty : Eq (α := ℝ≥0∞) ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s ∅) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Tendsto (β := ℝ≥0∞)
    (fun (r : ℚ) ↦ ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s (Iic (↑(-r) : ℝ))) : ℝ≥0∞)) atTop
    (𝓝 ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (⋂ (r : ℚ), SProd.sprod (β := Set ℝ) s (Iic (↑(-r) : ℝ)))) : Filter ℝ≥0∞)
have refine : Antitone.{0, u_1} (β := Set (α × ℝ)) fun (r : ℚ) ↦ SProd.sprod (β := Set ℝ) s (Iic (↑(-r) : ℝ))
Tactic: refine tendsto_measure_iInter_atTop (fun q ↦ (hs.prod measurableSet_Iic).nullMeasurableSet)
    ?_ ⟨0, measure_ne_top ρ _⟩
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CondCDF (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
h_empty : Eq (α := ℝ≥0∞) ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s ∅) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Antitone.{0, u_1} (β := Set (α × ℝ)) fun (r : ℚ) ↦ SProd.sprod (β := Set ℝ) s (Iic (↑(-r) : ℝ))
have refine : ∀ (q r : ℚ) (hqr : q ≤ r) (x : ℝ) (hx : Membership.mem (γ := Set ℝ) (Iic (↑(-r) : ℝ)) x),
  Membership.mem (γ := Set ℝ) (Iic (↑(-q) : ℝ)) x
Tactic: refine fun q r hqr ↦ Set.prod_mono subset_rfl fun x hx ↦ ?_
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CondCDF (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
h_empty : Eq (α := ℝ≥0∞) ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s ∅) : ℝ≥0∞) (0 : ℝ≥0∞)
q r : ℚ
hqr : q ≤ r
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Iic (↑(-r) : ℝ)) x
⊢ Membership.mem (γ := Set ℝ) (Iic (↑(-q) : ℝ)) x
have simp : ∀ (hx : x ≤ -(↑r : ℝ)), x ≤ -(↑q : ℝ)
Tactic: simp only [Rat.cast_neg, mem_Iic] at hx ⊢
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CondCDF (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
s : Set α
hs : MeasurableSet s
h_empty : Eq (α := ℝ≥0∞) ((ρ : (a : Set (α × ℝ)) → ℝ≥0∞) (SProd.sprod (β := Set ℝ) s ∅) : ℝ≥0∞) (0 : ℝ≥0∞)
q r : ℚ
hqr : q ≤ r
x : ℝ
hx : x ≤ -(↑r : ℝ)
⊢ x ≤ -(↑q : ℝ)
have refine : LE.le (α := ℝ) (↑q : ℝ) (↑r : ℝ)
Tactic: refine hx.trans (neg_le_neg ?_)
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CondCDF (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
⊢ Measurable (β := (r : ℚ) → ℝ) fun (a : α) (r : ℚ) ↦ (preCDF ρ r a).toReal
have rw : ∀ (a : ℚ), Measurable (β := ℝ) fun (x : α) ↦ (preCDF ρ a x).toReal
Tactic: rw [measurable_pi_iff]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CondCDF (hypothesis)
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
r : ℚ
s : Set α
hs : MeasurableSet s
inst : IsFiniteMeasure ρ
⊢ ∫⁻ (x : α) in s, preCDF ρ r x ∂ρ.fst = (ρ.IicSnd (↑r : ℝ) : (a : Set α) → ℝ≥0∞) s
have this : ∀ (r : ℚ), ∫⁻ (x : α) in s, preCDF ρ r x ∂ρ.fst = ∫⁻ (x : α) in s, HMul.hMul (β := α → ℝ≥0∞) (preCDF ρ r) 1 x ∂ρ.fst
Tactic: have : ∀ r, ∫⁻ x in s, preCDF ρ r x ∂ρ.fst = ∫⁻ x in s, (preCDF ρ r * 1) x ∂ρ.fst := by
    simp only [mul_one, forall_const]
-- 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 ρ
this :
  ∀ (r : ℚ), ∫⁻ (x : α) in s, preCDF ρ r x ∂ρ.fst = ∫⁻ (x : α) in s, HMul.hMul (β := α → ℝ≥0∞) (preCDF ρ r) 1 x ∂ρ.fst
⊢ ∫⁻ (x : α) in s, preCDF ρ r x ∂ρ.fst = (ρ.IicSnd (↑r : ℝ) : (a : Set α) → ℝ≥0∞) s
have rw : ∫⁻ (x : α) in s, 1 x ∂ρ.fst.withDensity (preCDF ρ r) = (ρ.IicSnd (↑r : ℝ) : (a : Set α) → ℝ≥0∞) s
Tactic: rw [this, ← setLIntegral_withDensity_eq_setLIntegral_mul _ measurable_preCDF _ hs]
-- 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 ρ
this :
  ∀ (r : ℚ), ∫⁻ (x : α) in s, preCDF ρ r x ∂ρ.fst = ∫⁻ (x : α) in s, HMul.hMul (β := α → ℝ≥0∞) (preCDF ρ r) 1 x ∂ρ.fst
rw : ∫⁻ (x : α) in s, 1 x ∂ρ.fst.withDensity (preCDF ρ r) = (ρ.IicSnd (↑r : ℝ) : (a : Set α) → ℝ≥0∞) s
⊢ ∫⁻ (x : α) in s, preCDF ρ r x ∂ρ.fst = (ρ.IicSnd (↑r : ℝ) : (a : Set α) → ℝ≥0∞) s
have rw₁ : Measurable.{u_1, 0} (α := α) (β := ℝ≥0∞) 1
Tactic: rw [this, ← setLIntegral_withDensity_eq_setLIntegral_mul _ measurable_preCDF _ hs]
-- 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 ∂ρ.fst = (ρ.IicSnd (↑r : ℝ) : (a : Set α) → ℝ≥0∞) univ
have rw : ∫⁻ (x : α) in univ, preCDF ρ r x ∂ρ.fst = (ρ.IicSnd (↑r : ℝ) : (a : Set α) → ℝ≥0∞) univ
Tactic: rw [← setLIntegral_univ, setLIntegral_preCDF_fst ρ r 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 ∂ρ.fst = (ρ.IicSnd (↑r : ℝ) : (a : Set α) → ℝ≥0∞) univ
⊢ ∫⁻ (x : α), preCDF ρ r x ∂ρ.fst = (ρ.IicSnd (↑r : ℝ) : (a : Set α) → ℝ≥0∞) univ
have rw₁ : Eq (α := ℝ≥0∞) ((ρ.IicSnd (↑r : ℝ) : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
  ((ρ.IicSnd (↑r : ℝ) : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
Tactic: rw [← setLIntegral_univ, setLIntegral_preCDF_fst ρ r MeasurableSet.univ]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CondCDF (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
⊢ ∀ᵐ (a : α) ∂ρ.fst, Monotone (β := ℝ≥0∞) fun (r : ℚ) ↦ preCDF ρ r a
have simp_rw : ∀ (i i_1 : ℚ) (i_2 : i ≤ i_1), ∀ᵐ (a : α) ∂ρ.fst, preCDF ρ i a ≤ preCDF ρ i_1 a
Tactic: simp_rw [Monotone, ae_all_iff]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CondCDF (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
⊢ ∀ (i i_1 : ℚ) (i_2 : i ≤ i_1), ∀ᵐ (a : α) ∂ρ.fst, preCDF ρ i a ≤ preCDF ρ i_1 a
have refine : ∀ (r r' : ℚ) (hrr' : r ≤ r') (s : Set α) (hs : MeasurableSet s),
  LT.lt (α := ℝ≥0∞) ((ρ.fst : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
    ∫⁻ (x : α) in s, preCDF ρ r x ∂ρ.fst ≤ ∫⁻ (x : α) in s, preCDF ρ r' x ∂ρ.fst
Tactic: refine fun r r' hrr' ↦ ae_le_of_forall_setLIntegral_le_of_sigmaFinite measurable_preCDF
    fun s hs _ ↦ ?_
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CondCDF (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
r r' : ℚ
hrr' : r ≤ r'
s : Set α
hs : MeasurableSet s
h : LT.lt (α := ℝ≥0∞) ((ρ.fst : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∫⁻ (x : α) in s, preCDF ρ r x ∂ρ.fst ≤ ∫⁻ (x : α) in s, preCDF ρ r' x ∂ρ.fst
have rw : LE.le (α := ℝ≥0∞) ((ρ.IicSnd (↑r : ℝ) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
  ((ρ.IicSnd (↑r' : ℝ) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [setLIntegral_preCDF_fst ρ r hs, setLIntegral_preCDF_fst ρ r' hs]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CondCDF (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
⊢ ∀ᵐ (a : α) ∂ρ.fst, ∀ (r : ℚ), preCDF ρ r a ≤ 1
have rw : ∀ (i : ℚ), ∀ᵐ (a : α) ∂ρ.fst, preCDF ρ i a ≤ 1
Tactic: rw [ae_all_iff]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CondCDF (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
⊢ ∀ (i : ℚ), ∀ᵐ (a : α) ∂ρ.fst, preCDF ρ i a ≤ 1
have refine : ∀ (r : ℚ) (s : Set α) (hs : MeasurableSet s),
  LT.lt (α := ℝ≥0∞) ((ρ.fst : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
    ∫⁻ (x : α) in s, preCDF ρ r x ∂ρ.fst ≤ ∫⁻ (x : α) in s, 1 ∂ρ.fst
Tactic: refine fun r ↦ ae_le_of_forall_setLIntegral_le_of_sigmaFinite measurable_preCDF fun s hs _ ↦ ?_
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CondCDF (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
r : ℚ
s : Set α
hs : MeasurableSet s
h : LT.lt (α := ℝ≥0∞) ((ρ.fst : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∫⁻ (x : α) in s, preCDF ρ r x ∂ρ.fst ≤ ∫⁻ (x : α) in s, 1 ∂ρ.fst
have rw : (ρ.IicSnd (↑r : ℝ) : (a : Set α) → ℝ≥0∞) s ≤ ∫⁻ (x : α) in s, 1 ∂ρ.fst
Tactic: rw [setLIntegral_preCDF_fst ρ r hs]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Disintegration.CondCDF (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst : IsFiniteMeasure ρ
r : ℚ
s : Set α
hs : MeasurableSet s
h : LT.lt (α := ℝ≥0∞) ((ρ.fst : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ (ρ.IicSnd (↑r : ℝ) : (a : Set α) → ℝ≥0∞) s ≤ ∫⁻ (x : α) in s, 1 ∂ρ.fst
have simp : LE.le (α := ℝ≥0∞) ((ρ.IicSnd (↑r : ℝ) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ρ.fst : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: simp only [lintegral_one, Measure.restrict_apply, MeasurableSet.univ, univ_inter]
-- 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 : α) in s, (preCDF ρ r x).toReal ∂ρ.fst = (ρ.IicSnd (↑r : ℝ)).real s
have rw : (∫⁻ (a : α) in s, preCDF ρ r a ∂ρ.fst).toReal = (ρ.IicSnd (↑r : ℝ)).real s
Tactic: rw [integral_toReal]
-- 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 : (∫⁻ (a : α) in s, preCDF ρ r a ∂ρ.fst).toReal = (ρ.IicSnd (↑r : ℝ)).real s
⊢ ∫ (x : α) in s, (preCDF ρ r x).toReal ∂ρ.fst = (ρ.IicSnd (↑r : ℝ)).real s
have hfm : AEMeasurable (preCDF ρ r) (ρ.fst.restrict s)
Tactic: rw [integral_toReal]
-- 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 : (∫⁻ (a : α) in s, preCDF ρ r a ∂ρ.fst).toReal = (ρ.IicSnd (↑r : ℝ)).real s
hfm : AEMeasurable (preCDF ρ r) (ρ.fst.restrict s)
⊢ ∫ (x : α) in s, (preCDF ρ r x).toReal ∂ρ.fst = (ρ.IicSnd (↑r : ℝ)).real s
have hf : ∀ᵐ (x : α) ∂ρ.fst.restrict s, preCDF ρ r x < ∞
Tactic: rw [integral_toReal]
-- 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 ρ
⊢ (∫⁻ (a : α) in s, preCDF ρ r a ∂ρ.fst).toReal = (ρ.IicSnd (↑r : ℝ)).real s
have rw : ENNReal.toReal ((ρ.IicSnd (↑r : ℝ) : (a : Set α) → ℝ≥0∞) s) = (ρ.IicSnd (↑r : ℝ)).real s
Tactic: rw [setLIntegral_preCDF_fst _ _ hs, measureReal_def]