awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μs : ℕ → LevyProkhorov (ProbabilityMeasure Ω)
ν : LevyProkhorov (ProbabilityMeasure Ω)
hμs : Tendsto μs atTop (𝓝 ν)
P : ProbabilityMeasure Ω := ν.toMeasure
Ps : ℕ → ProbabilityMeasure Ω := toMeasure ∘ μs
f_1 f : Ω →ᵇ ℝ
f_nn : 0 ≤ f
f_zero : ¬‖f‖ = 0
norm_f_pos : 0 < ‖f‖
δ : ℝ
δ_pos : 0 < δ
εs : ℕ → ℝ
left : StrictAnti εs
εs_lim : Tendsto εs atTop (𝓝 0)
ε_of_room : Tendsto (β := ℝ) (fun (x : ℕ) ↦ dist (μs x) ν + εs x) atTop (𝓝 0)
ε_of_room' : Tendsto (β := ℝ) (fun (n : ℕ) ↦ dist (μs n) ν + εs n) atTop (𝓝[>] 0)
key :
  Tendsto (β := ℝ)
    (fun (x : ℕ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 ‖f‖)) fun (t : ℝ) ↦
        (↑P : Measure Ω).real (thickening (dist (μs x) ν + εs x) {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}))
    atTop
    (𝓝
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 ‖f‖)) fun (t : ℝ) ↦
        (↑P : Measure Ω).real {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}))
aux : ∀ (z : ℝ), Iio (z + δ / 2) ∈ 𝓝 z
n : ℕ
hn :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 ‖f‖)) fun (t : ℝ) ↦
      (↑P : Measure Ω).real (thickening (dist (μs n) ν + εs n) {a : Ω | t ≤ (f : (a : Ω) → ℝ) a})) <
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 ‖f‖)) fun (t : ℝ) ↦
        (↑P : Measure Ω).real {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) +
      δ / 2
hn' : dist (μs n) ν + εs n < ‖f‖⁻¹ * δ / 2
εs_pos : 0 < εs n
h :
  ∀
    (bound :
      ∫ (ω : Ω), (f : (a : Ω) → ℝ) ω ∂(↑(Ps n) : Measure Ω) ≤
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 ‖f‖)) fun (t : ℝ) ↦
            (↑P : Measure Ω).real (thickening (dist (μs n) ν + εs n) {a : Ω | t ≤ (f : (a : Ω) → ℝ) a})) +
          (dist (μs n) ν + εs n) * ‖f‖),
    ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑(Ps n) : Measure Ω) ≤ ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑P : Measure Ω) + δ
h₁ : 0 < dist (μs n) ν + εs n
h₂ : levyProkhorovEDist (↑(Ps n) : Measure Ω) (↑P : Measure Ω) < ENNReal.ofReal (dist (μs n) ν + εs n)
⊢ ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑(Ps n) : Measure Ω) ≤ ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑P : Measure Ω) + δ
have h₃ : (ae (↑(Ps n) : Measure Ω)).EventuallyLE (β := ℝ) 0 (⇑f : (a : Ω) → ℝ)
Tactic: have bound := BoundedContinuousFunction.integral_le_of_levyProkhorovEDist_lt
                    (Ps n) P (ε := dist (μs n) ν + εs n) ?_ ?_ f ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μs : ℕ → LevyProkhorov (ProbabilityMeasure Ω)
ν : LevyProkhorov (ProbabilityMeasure Ω)
hμs : Tendsto μs atTop (𝓝 ν)
P : ProbabilityMeasure Ω := ν.toMeasure
Ps : ℕ → ProbabilityMeasure Ω := toMeasure ∘ μs
f_1 f : Ω →ᵇ ℝ
f_nn : 0 ≤ f
f_zero : ¬‖f‖ = 0
norm_f_pos : 0 < ‖f‖
δ : ℝ
δ_pos : 0 < δ
εs : ℕ → ℝ
left : StrictAnti εs
εs_lim : Tendsto εs atTop (𝓝 0)
ε_of_room : Tendsto (β := ℝ) (fun (x : ℕ) ↦ dist (μs x) ν + εs x) atTop (𝓝 0)
ε_of_room' : Tendsto (β := ℝ) (fun (n : ℕ) ↦ dist (μs n) ν + εs n) atTop (𝓝[>] 0)
key :
  Tendsto (β := ℝ)
    (fun (x : ℕ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 ‖f‖)) fun (t : ℝ) ↦
        (↑P : Measure Ω).real (thickening (dist (μs x) ν + εs x) {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}))
    atTop
    (𝓝
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 ‖f‖)) fun (t : ℝ) ↦
        (↑P : Measure Ω).real {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}))
aux : ∀ (z : ℝ), Iio (z + δ / 2) ∈ 𝓝 z
n : ℕ
hn :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 ‖f‖)) fun (t : ℝ) ↦
      (↑P : Measure Ω).real (thickening (dist (μs n) ν + εs n) {a : Ω | t ≤ (f : (a : Ω) → ℝ) a})) <
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 ‖f‖)) fun (t : ℝ) ↦
        (↑P : Measure Ω).real {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) +
      δ / 2
hn' : dist (μs n) ν + εs n < ‖f‖⁻¹ * δ / 2
εs_pos : 0 < εs n
bound :
  ∫ (ω : Ω), (f : (a : Ω) → ℝ) ω ∂(↑(Ps n) : Measure Ω) ≤
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 ‖f‖)) fun (t : ℝ) ↦
        (↑P : Measure Ω).real (thickening (dist (μs n) ν + εs n) {a : Ω | t ≤ (f : (a : Ω) → ℝ) a})) +
      (dist (μs n) ν + εs n) * ‖f‖
⊢ ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑(Ps n) : Measure Ω) ≤ ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑P : Measure Ω) + δ
have h : (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 ‖f‖)) fun (t : ℝ) ↦
      (↑P : Measure Ω).real {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) +
    (δ / 2 + ‖f‖ * (dist (μs n) ν + εs n)) ≤
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 ‖f‖)) fun (t : ℝ) ↦
      (↑P : Measure Ω).real {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) +
    δ
Tactic: grw [bound, hn, BoundedContinuousFunction.integral_eq_integral_meas_le _ _ <| .of_forall f_nn,
        add_assoc, mul_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μs : ℕ → LevyProkhorov (ProbabilityMeasure Ω)
ν : LevyProkhorov (ProbabilityMeasure Ω)
hμs : Tendsto μs atTop (𝓝 ν)
P : ProbabilityMeasure Ω := ν.toMeasure
Ps : ℕ → ProbabilityMeasure Ω := toMeasure ∘ μs
f_1 f : Ω →ᵇ ℝ
f_nn : 0 ≤ f
f_zero : ¬‖f‖ = 0
norm_f_pos : 0 < ‖f‖
δ : ℝ
δ_pos : 0 < δ
εs : ℕ → ℝ
left : StrictAnti εs
εs_lim : Tendsto εs atTop (𝓝 0)
ε_of_room : Tendsto (β := ℝ) (fun (x : ℕ) ↦ dist (μs x) ν + εs x) atTop (𝓝 0)
ε_of_room' : Tendsto (β := ℝ) (fun (n : ℕ) ↦ dist (μs n) ν + εs n) atTop (𝓝[>] 0)
key :
  Tendsto (β := ℝ)
    (fun (x : ℕ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 ‖f‖)) fun (t : ℝ) ↦
        (↑P : Measure Ω).real (thickening (dist (μs x) ν + εs x) {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}))
    atTop
    (𝓝
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 ‖f‖)) fun (t : ℝ) ↦
        (↑P : Measure Ω).real {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}))
aux : ∀ (z : ℝ), Iio (z + δ / 2) ∈ 𝓝 z
n : ℕ
hn :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 ‖f‖)) fun (t : ℝ) ↦
      (↑P : Measure Ω).real (thickening (dist (μs n) ν + εs n) {a : Ω | t ≤ (f : (a : Ω) → ℝ) a})) <
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 ‖f‖)) fun (t : ℝ) ↦
        (↑P : Measure Ω).real {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) +
      δ / 2
hn' : dist (μs n) ν + εs n < ‖f‖⁻¹ * δ / 2
εs_pos : 0 < εs n
bound :
  ∫ (ω : Ω), (f : (a : Ω) → ℝ) ω ∂(↑(Ps n) : Measure Ω) ≤
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 ‖f‖)) fun (t : ℝ) ↦
        (↑P : Measure Ω).real (thickening (dist (μs n) ν + εs n) {a : Ω | t ≤ (f : (a : Ω) → ℝ) a})) +
      (dist (μs n) ν + εs n) * ‖f‖
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 ‖f‖)) fun (t : ℝ) ↦
        (↑P : Measure Ω).real {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) +
      (δ / 2 + ‖f‖ * (dist (μs n) ν + εs n)) ≤
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 ‖f‖)) fun (t : ℝ) ↦
        (↑P : Measure Ω).real {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) +
      δ
have h : δ / 2 + ‖f‖ * (dist (μs n) ν + εs n) ≤ δ
Tactic: gcongr
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μs : ℕ → LevyProkhorov (ProbabilityMeasure Ω)
ν : LevyProkhorov (ProbabilityMeasure Ω)
hμs : Tendsto μs atTop (𝓝 ν)
P : ProbabilityMeasure Ω := ν.toMeasure
Ps : ℕ → ProbabilityMeasure Ω := toMeasure ∘ μs
f_1 f : Ω →ᵇ ℝ
f_nn : 0 ≤ f
f_zero : ¬‖f‖ = 0
norm_f_pos : 0 < ‖f‖
δ : ℝ
δ_pos : 0 < δ
εs : ℕ → ℝ
left : StrictAnti εs
εs_lim : Tendsto εs atTop (𝓝 0)
ε_of_room : Tendsto (β := ℝ) (fun (x : ℕ) ↦ dist (μs x) ν + εs x) atTop (𝓝 0)
ε_of_room' : Tendsto (β := ℝ) (fun (n : ℕ) ↦ dist (μs n) ν + εs n) atTop (𝓝[>] 0)
key :
  Tendsto (β := ℝ)
    (fun (x : ℕ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 ‖f‖)) fun (t : ℝ) ↦
        (↑P : Measure Ω).real (thickening (dist (μs x) ν + εs x) {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}))
    atTop
    (𝓝
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 ‖f‖)) fun (t : ℝ) ↦
        (↑P : Measure Ω).real {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}))
aux : ∀ (z : ℝ), Iio (z + δ / 2) ∈ 𝓝 z
n : ℕ
hn :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 ‖f‖)) fun (t : ℝ) ↦
      (↑P : Measure Ω).real (thickening (dist (μs n) ν + εs n) {a : Ω | t ≤ (f : (a : Ω) → ℝ) a})) <
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 ‖f‖)) fun (t : ℝ) ↦
        (↑P : Measure Ω).real {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) +
      δ / 2
hn' : dist (μs n) ν + εs n < ‖f‖⁻¹ * δ / 2
εs_pos : 0 < εs n
bound :
  ∫ (ω : Ω), (f : (a : Ω) → ℝ) ω ∂(↑(Ps n) : Measure Ω) ≤
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 ‖f‖)) fun (t : ℝ) ↦
        (↑P : Measure Ω).real (thickening (dist (μs n) ν + εs n) {a : Ω | t ≤ (f : (a : Ω) → ℝ) a})) +
      (dist (μs n) ν + εs n) * ‖f‖
⊢ δ / 2 + ‖f‖ * (dist (μs n) ν + εs n) ≤ δ / 2 + ‖f‖ * (‖f‖⁻¹ * δ / 2)
have bc : 0 ≤ ‖f‖
Tactic: gcongr
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μs : ℕ → LevyProkhorov (ProbabilityMeasure Ω)
ν : LevyProkhorov (ProbabilityMeasure Ω)
hμs : Tendsto μs atTop (𝓝 ν)
P : ProbabilityMeasure Ω := ν.toMeasure
Ps : ℕ → ProbabilityMeasure Ω := toMeasure ∘ μs
f_1 f : Ω →ᵇ ℝ
f_nn : 0 ≤ f
f_zero : ¬‖f‖ = 0
norm_f_pos : 0 < ‖f‖
δ : ℝ
δ_pos : 0 < δ
εs : ℕ → ℝ
left : StrictAnti εs
εs_lim : Tendsto εs atTop (𝓝 0)
ε_of_room : Tendsto (β := ℝ) (fun (x : ℕ) ↦ dist (μs x) ν + εs x) atTop (𝓝 0)
ε_of_room' : Tendsto (β := ℝ) (fun (n : ℕ) ↦ dist (μs n) ν + εs n) atTop (𝓝[>] 0)
key :
  Tendsto (β := ℝ)
    (fun (x : ℕ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 ‖f‖)) fun (t : ℝ) ↦
        (↑P : Measure Ω).real (thickening (dist (μs x) ν + εs x) {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}))
    atTop
    (𝓝
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 ‖f‖)) fun (t : ℝ) ↦
        (↑P : Measure Ω).real {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}))
aux : ∀ (z : ℝ), Iio (z + δ / 2) ∈ 𝓝 z
n : ℕ
hn :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 ‖f‖)) fun (t : ℝ) ↦
      (↑P : Measure Ω).real (thickening (dist (μs n) ν + εs n) {a : Ω | t ≤ (f : (a : Ω) → ℝ) a})) <
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 ‖f‖)) fun (t : ℝ) ↦
        (↑P : Measure Ω).real {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) +
      δ / 2
hn' : dist (μs n) ν + εs n < ‖f‖⁻¹ * δ / 2
εs_pos : 0 < εs n
bound :
  ∫ (ω : Ω), (f : (a : Ω) → ℝ) ω ∂(↑(Ps n) : Measure Ω) ≤
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 ‖f‖)) fun (t : ℝ) ↦
        (↑P : Measure Ω).real (thickening (dist (μs n) ν + εs n) {a : Ω | t ≤ (f : (a : Ω) → ℝ) a})) +
      (dist (μs n) ν + εs n) * ‖f‖
⊢ δ / 2 + ‖f‖ * (dist (μs n) ν + εs n) ≤ δ
have δ₁ : δ / 2 + ‖f‖ * (dist (μs n) ν + εs n) ≤ δ / 2 + ‖f‖ * (‖f‖⁻¹ * δ / 2)
Tactic: calc
        δ / 2 + ‖f‖ * (dist (μs n) ν + εs n)
        _ ≤ δ / 2 + ‖f‖ * (‖f‖⁻¹ * δ / 2) := by gcongr
        _ = δ := by field
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μs : ℕ → LevyProkhorov (ProbabilityMeasure Ω)
ν : LevyProkhorov (ProbabilityMeasure Ω)
hμs : Tendsto μs atTop (𝓝 ν)
P : ProbabilityMeasure Ω := ν.toMeasure
Ps : ℕ → ProbabilityMeasure Ω := toMeasure ∘ μs
f_1 f : Ω →ᵇ ℝ
f_nn : 0 ≤ f
f_zero : ¬‖f‖ = 0
norm_f_pos : 0 < ‖f‖
δ : ℝ
δ_pos : 0 < δ
εs : ℕ → ℝ
left : StrictAnti εs
εs_lim : Tendsto εs atTop (𝓝 0)
ε_of_room : Tendsto (β := ℝ) (fun (x : ℕ) ↦ dist (μs x) ν + εs x) atTop (𝓝 0)
ε_of_room' : Tendsto (β := ℝ) (fun (n : ℕ) ↦ dist (μs n) ν + εs n) atTop (𝓝[>] 0)
key :
  Tendsto (β := ℝ)
    (fun (x : ℕ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 ‖f‖)) fun (t : ℝ) ↦
        (↑P : Measure Ω).real (thickening (dist (μs x) ν + εs x) {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}))
    atTop
    (𝓝
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 ‖f‖)) fun (t : ℝ) ↦
        (↑P : Measure Ω).real {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}))
aux : ∀ (z : ℝ), Iio (z + δ / 2) ∈ 𝓝 z
n : ℕ
hn :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 ‖f‖)) fun (t : ℝ) ↦
      (↑P : Measure Ω).real (thickening (dist (μs n) ν + εs n) {a : Ω | t ≤ (f : (a : Ω) → ℝ) a})) <
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 ‖f‖)) fun (t : ℝ) ↦
        (↑P : Measure Ω).real {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) +
      δ / 2
hn' : dist (μs n) ν + εs n < ‖f‖⁻¹ * δ / 2
εs_pos : 0 < εs n
bound :
  ∫ (ω : Ω), (f : (a : Ω) → ℝ) ω ∂(↑(Ps n) : Measure Ω) ≤
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 ‖f‖)) fun (t : ℝ) ↦
        (↑P : Measure Ω).real (thickening (dist (μs n) ν + εs n) {a : Ω | t ≤ (f : (a : Ω) → ℝ) a})) +
      (dist (μs n) ν + εs n) * ‖f‖
δ₁ : δ / 2 + ‖f‖ * (dist (μs n) ν + εs n) ≤ δ / 2 + ‖f‖ * (‖f‖⁻¹ * δ / 2)
⊢ δ / 2 + ‖f‖ * (dist (μs n) ν + εs n) ≤ δ
have δ₂ : δ / 2 + ‖f‖ * (‖f‖⁻¹ * δ / 2) = δ
Tactic: calc
        δ / 2 + ‖f‖ * (dist (μs n) ν + εs n)
        _ ≤ δ / 2 + ‖f‖ * (‖f‖⁻¹ * δ / 2) := by gcongr
        _ = δ := by field
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μs : ℕ → LevyProkhorov (ProbabilityMeasure Ω)
ν : LevyProkhorov (ProbabilityMeasure Ω)
hμs : Tendsto μs atTop (𝓝 ν)
P : ProbabilityMeasure Ω := ν.toMeasure
Ps : ℕ → ProbabilityMeasure Ω := toMeasure ∘ μs
f_1 f : Ω →ᵇ ℝ
f_nn : 0 ≤ f
f_zero : ¬‖f‖ = 0
norm_f_pos : 0 < ‖f‖
δ : ℝ
δ_pos : 0 < δ
εs : ℕ → ℝ
left : StrictAnti εs
εs_lim : Tendsto εs atTop (𝓝 0)
ε_of_room : Tendsto (β := ℝ) (fun (x : ℕ) ↦ dist (μs x) ν + εs x) atTop (𝓝 0)
ε_of_room' : Tendsto (β := ℝ) (fun (n : ℕ) ↦ dist (μs n) ν + εs n) atTop (𝓝[>] 0)
key :
  Tendsto (β := ℝ)
    (fun (x : ℕ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 ‖f‖)) fun (t : ℝ) ↦
        (↑P : Measure Ω).real (thickening (dist (μs x) ν + εs x) {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}))
    atTop
    (𝓝
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 ‖f‖)) fun (t : ℝ) ↦
        (↑P : Measure Ω).real {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}))
aux : ∀ (z : ℝ), Iio (z + δ / 2) ∈ 𝓝 z
n : ℕ
hn :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 ‖f‖)) fun (t : ℝ) ↦
      (↑P : Measure Ω).real (thickening (dist (μs n) ν + εs n) {a : Ω | t ≤ (f : (a : Ω) → ℝ) a})) <
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 ‖f‖)) fun (t : ℝ) ↦
        (↑P : Measure Ω).real {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) +
      δ / 2
hn' : dist (μs n) ν + εs n < ‖f‖⁻¹ * δ / 2
εs_pos : 0 < εs n
⊢ levyProkhorovEDist (↑(Ps n) : Measure Ω) (↑P : Measure Ω) < ENNReal.ofReal (dist (μs n) ν + εs n)
have h : levyProkhorovEDist (↑(Ps n) : Measure Ω) (↑P : Measure Ω) + 0 < ENNReal.ofReal (dist (μs n) ν) + ENNReal.ofReal (εs n)
Tactic: rw [ENNReal.ofReal_add (by positivity) (by positivity), ← add_zero (levyProkhorovEDist _ _)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μs : ℕ → LevyProkhorov (ProbabilityMeasure Ω)
ν : LevyProkhorov (ProbabilityMeasure Ω)
hμs : Tendsto μs atTop (𝓝 ν)
P : ProbabilityMeasure Ω := ν.toMeasure
Ps : ℕ → ProbabilityMeasure Ω := toMeasure ∘ μs
f_1 f : Ω →ᵇ ℝ
f_nn : 0 ≤ f
f_zero : ¬‖f‖ = 0
norm_f_pos : 0 < ‖f‖
δ : ℝ
δ_pos : 0 < δ
εs : ℕ → ℝ
left : StrictAnti εs
εs_lim : Tendsto εs atTop (𝓝 0)
ε_of_room : Tendsto (β := ℝ) (fun (x : ℕ) ↦ dist (μs x) ν + εs x) atTop (𝓝 0)
ε_of_room' : Tendsto (β := ℝ) (fun (n : ℕ) ↦ dist (μs n) ν + εs n) atTop (𝓝[>] 0)
key :
  Tendsto (β := ℝ)
    (fun (x : ℕ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 ‖f‖)) fun (t : ℝ) ↦
        (↑P : Measure Ω).real (thickening (dist (μs x) ν + εs x) {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}))
    atTop
    (𝓝
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 ‖f‖)) fun (t : ℝ) ↦
        (↑P : Measure Ω).real {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}))
aux : ∀ (z : ℝ), Iio (z + δ / 2) ∈ 𝓝 z
n : ℕ
hn :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 ‖f‖)) fun (t : ℝ) ↦
      (↑P : Measure Ω).real (thickening (dist (μs n) ν + εs n) {a : Ω | t ≤ (f : (a : Ω) → ℝ) a})) <
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 ‖f‖)) fun (t : ℝ) ↦
        (↑P : Measure Ω).real {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) +
      δ / 2
hn' : dist (μs n) ν + εs n < ‖f‖⁻¹ * δ / 2
εs_pos : 0 < εs n
⊢ levyProkhorovEDist (↑(Ps n) : Measure Ω) (↑P : Measure Ω) + 0 < ENNReal.ofReal (dist (μs n) ν) + ENNReal.ofReal (εs n)
have apply : levyProkhorovEDist (↑(Ps n) : Measure Ω) (↑P : Measure Ω) = ENNReal.ofReal (dist (μs n) ν)
Tactic: apply ENNReal.add_lt_add_of_le_of_lt (levyProkhorovEDist_ne_top _ _)
            (le_of_eq ?_) (ofReal_pos.mpr εs_pos)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μs : ℕ → LevyProkhorov (ProbabilityMeasure Ω)
ν : LevyProkhorov (ProbabilityMeasure Ω)
hμs : Tendsto μs atTop (𝓝 ν)
P : ProbabilityMeasure Ω := ν.toMeasure
Ps : ℕ → ProbabilityMeasure Ω := toMeasure ∘ μs
f_1 f : Ω →ᵇ ℝ
f_nn : 0 ≤ f
f_zero : ¬‖f‖ = 0
norm_f_pos : 0 < ‖f‖
δ : ℝ
δ_pos : 0 < δ
εs : ℕ → ℝ
left : StrictAnti εs
εs_lim : Tendsto εs atTop (𝓝 0)
ε_of_room : Tendsto (β := ℝ) (fun (x : ℕ) ↦ dist (μs x) ν + εs x) atTop (𝓝 0)
ε_of_room' : Tendsto (β := ℝ) (fun (n : ℕ) ↦ dist (μs n) ν + εs n) atTop (𝓝[>] 0)
key :
  Tendsto (β := ℝ)
    (fun (x : ℕ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 ‖f‖)) fun (t : ℝ) ↦
        (↑P : Measure Ω).real (thickening (dist (μs x) ν + εs x) {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}))
    atTop
    (𝓝
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 ‖f‖)) fun (t : ℝ) ↦
        (↑P : Measure Ω).real {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}))
aux : ∀ (z : ℝ), Iio (z + δ / 2) ∈ 𝓝 z
n : ℕ
hn :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 ‖f‖)) fun (t : ℝ) ↦
      (↑P : Measure Ω).real (thickening (dist (μs n) ν + εs n) {a : Ω | t ≤ (f : (a : Ω) → ℝ) a})) <
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 ‖f‖)) fun (t : ℝ) ↦
        (↑P : Measure Ω).real {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) +
      δ / 2
hn' : dist (μs n) ν + εs n < ‖f‖⁻¹ * δ / 2
εs_pos : 0 < εs n
⊢ levyProkhorovEDist (↑(Ps n) : Measure Ω) (↑P : Measure Ω) = ENNReal.ofReal (dist (μs n) ν)
have rw : levyProkhorovEDist (↑(Ps n) : Measure Ω) (↑P : Measure Ω) =
  levyProkhorovEDist (↑(μs n).toMeasure : Measure Ω) (↑ν.toMeasure : Measure Ω)
Tactic: rw [LevyProkhorov.dist_probabilityMeasure_def, levyProkhorovDist,
        ofReal_toReal (levyProkhorovEDist_ne_top _ _)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μs : ℕ → LevyProkhorov (ProbabilityMeasure Ω)
ν : LevyProkhorov (ProbabilityMeasure Ω)
hμs : Tendsto μs atTop (𝓝 ν)
P : ProbabilityMeasure Ω := ν.toMeasure
Ps : ℕ → ProbabilityMeasure Ω := toMeasure ∘ μs
f_1 f : Ω →ᵇ ℝ
f_nn : 0 ≤ f
f_zero : ¬‖f‖ = 0
norm_f_pos : 0 < ‖f‖
δ : ℝ
δ_pos : 0 < δ
⊢ IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) atTop fun (i : ℕ) ↦ ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑(Ps i) : Measure Ω)
have simp : ∃ (b : ℝ), ∀ (a : ℝ) (x : ℕ) (h : ∀ b ≥ x, ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑(Ps b) : Measure Ω) ≤ a), b ≤ a
Tactic: simp only [IsCoboundedUnder, IsCobounded, eventually_map, eventually_atTop,
               forall_exists_index]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (goal)
Goal:
Ω : Type u_1
inst : PseudoMetricSpace Ω
inst_1 : MeasurableSpace Ω
inst_2 : OpensMeasurableSpace Ω
P : ProbabilityMeasure Ω
G : Set Ω
G_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] G
ε : ℝ≥0∞
ε_pos : 0 < ε
⊢ {Q : ProbabilityMeasure Ω |
      ((↑P : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G <
        HAdd.hAdd (α := ℝ≥0∞) (((↑Q : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G : ℝ≥0∞) ε} ∈
    𝓝 P
have pos : ∀ (easy : ((↑P : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G < ε),
  {Q : ProbabilityMeasure Ω |
      ((↑P : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G <
        HAdd.hAdd (α := ℝ≥0∞) (((↑Q : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G : ℝ≥0∞) ε} ∈
    𝓝 P
Tactic: by_cases! easy : P.toMeasure G < ε
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (goal)
Goal:
Ω : Type u_1
inst : PseudoMetricSpace Ω
inst_1 : MeasurableSpace Ω
inst_2 : OpensMeasurableSpace Ω
P : ProbabilityMeasure Ω
G : Set Ω
G_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] G
ε : ℝ≥0∞
ε_pos : 0 < ε
pos :
  ∀ (easy : ((↑P : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G < ε),
    {Q : ProbabilityMeasure Ω |
        ((↑P : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G <
          HAdd.hAdd (α := ℝ≥0∞) (((↑Q : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G : ℝ≥0∞) ε} ∈
      𝓝 P
⊢ {Q : ProbabilityMeasure Ω |
      ((↑P : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G <
        HAdd.hAdd (α := ℝ≥0∞) (((↑Q : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G : ℝ≥0∞) ε} ∈
    𝓝 P
have neg : ∀ (easy : ε ≤ ((↑P : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G),
  {Q : ProbabilityMeasure Ω |
      ((↑P : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G <
        HAdd.hAdd (α := ℝ≥0∞) (((↑Q : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G : ℝ≥0∞) ε} ∈
    𝓝 P
Tactic: by_cases! easy : P.toMeasure G < ε
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (goal)
Goal:
Ω : Type u_1
inst : PseudoMetricSpace Ω
inst_1 : MeasurableSpace Ω
inst_2 : OpensMeasurableSpace Ω
P : ProbabilityMeasure Ω
G : Set Ω
G_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] G
ε : ℝ≥0∞
ε_pos : 0 < ε
easy : ε ≤ ((↑P : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G
⊢ {Q : ProbabilityMeasure Ω |
      ((↑P : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G <
        HAdd.hAdd (α := ℝ≥0∞) (((↑Q : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G : ℝ≥0∞) ε} ∈
    𝓝 P
have pos : ∀ (ε_top : ε = ∞),
  {Q : ProbabilityMeasure Ω |
      ((↑P : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G <
        HAdd.hAdd (α := ℝ≥0∞) (((↑Q : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G : ℝ≥0∞) ε} ∈
    𝓝 P
Tactic: by_cases ε_top : ε = ∞