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 Ω
f : Ω →ᵇ ℝ
A : Set ℝ
A_finmeas : Ne (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) A : ℝ≥0∞) (∞ : ℝ≥0∞)
μ : ProbabilityMeasure Ω
⊢ ∀ᶠ (n : ℝ) in 𝓝[>] 0,
    ∀ᵐ (a : ℝ) ∂Measure.restrict volume A,
      ‖(↑((μ : (a : Set Ω) → ℝ≥0) (thickening n {a_1 : Ω | a ≤ (f : (a : Ω) → ℝ) a_1})) : ℝ)‖ ≤ 1 a
have apply : ∀ (i : ℝ),
  ∀ᵐ (a : ℝ) ∂Measure.restrict volume A,
    ‖(↑((μ : (a : Set Ω) → ℝ≥0) (thickening i {a_1 : Ω | a ≤ (f : (a : Ω) → ℝ) a_1})) : ℝ)‖ ≤ 1 a
Tactic: apply Eventually.of_forall (fun i ↦ ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
f : Ω →ᵇ ℝ
A : Set ℝ
A_finmeas : Ne (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) A : ℝ≥0∞) (∞ : ℝ≥0∞)
μ : ProbabilityMeasure Ω
i : ℝ
⊢ ∀ᵐ (a : ℝ) ∂Measure.restrict volume A,
    ‖(↑((μ : (a : Set Ω) → ℝ≥0) (thickening i {a_1 : Ω | a ≤ (f : (a : Ω) → ℝ) a_1})) : ℝ)‖ ≤ 1 a
have apply : ∀ (t : ℝ), ‖(↑((μ : (a : Set Ω) → ℝ≥0) (thickening i {a : Ω | t ≤ (f : (a : Ω) → ℝ) a})) : ℝ)‖ ≤ 1 t
Tactic: apply Eventually.of_forall (fun t ↦ ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
f : Ω →ᵇ ℝ
A : Set ℝ
A_finmeas : Ne (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) A : ℝ≥0∞) (∞ : ℝ≥0∞)
μ : ProbabilityMeasure Ω
i t : ℝ
⊢ ‖(↑((μ : (a : Set Ω) → ℝ≥0) (thickening i {a : Ω | t ≤ (f : (a : Ω) → ℝ) a})) : ℝ)‖ ≤ 1 t
have simp : (↑((μ : (a : Set Ω) → ℝ≥0) (thickening i {a : Ω | t ≤ (f : (a : Ω) → ℝ) a})) : ℝ) ≤ 1
Tactic: simp only [Real.norm_eq_abs, NNReal.abs_eq, Pi.one_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (hypothesis)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
f : Ω →ᵇ ℝ
A : Set ℝ
A_finmeas : Ne (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) A : ℝ≥0∞) (∞ : ℝ≥0∞)
μ : ProbabilityMeasure Ω
⊢ @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace 1 (Measure.restrict volume A)
have aux : IsFiniteMeasure (m0 := MeasureSpace.toMeasurableSpace) (Measure.restrict volume A)
Tactic: have aux : IsFiniteMeasure (volume.restrict A) := ⟨by simp [lt_top_iff_ne_top, A_finmeas]⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
f : Ω →ᵇ ℝ
A : Set ℝ
A_finmeas : Ne (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) A : ℝ≥0∞) (∞ : ℝ≥0∞)
μ : ProbabilityMeasure Ω
⊢ ∀ᵐ (a : ℝ) ∂Measure.restrict volume A,
    Tendsto (fun (n : ℝ) ↦ (↑((μ : (a : Set Ω) → ℝ≥0) (thickening n {a_1 : Ω | a ≤ (f : (a : Ω) → ℝ) a_1})) : ℝ))
      (𝓝[>] 0) (𝓝 (↑((μ : (a : Set Ω) → ℝ≥0) {a_1 : Ω | a ≤ (f : (a : Ω) → ℝ) a_1}) : ℝ))
have apply : ∀ (t : ℝ),
  Tendsto (fun (n : ℝ) ↦ (↑((μ : (a : Set Ω) → ℝ≥0) (thickening n {a : Ω | t ≤ (f : (a : Ω) → ℝ) a})) : ℝ)) (𝓝[>] 0)
    (𝓝 (↑((μ : (a : Set Ω) → ℝ≥0) {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) : ℝ))
Tactic: apply Eventually.of_forall (fun t ↦ ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
f : Ω →ᵇ ℝ
A : Set ℝ
A_finmeas : Ne (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) A : ℝ≥0∞) (∞ : ℝ≥0∞)
μ : ProbabilityMeasure Ω
t : ℝ
⊢ Tendsto (fun (n : ℝ) ↦ (↑((μ : (a : Set Ω) → ℝ≥0) (thickening n {a : Ω | t ≤ (f : (a : Ω) → ℝ) a})) : ℝ)) (𝓝[>] 0)
    (𝓝 (↑((μ : (a : Set Ω) → ℝ≥0) {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) : ℝ))
have simp : Tendsto (β := ℝ≥0) (fun (a : ℝ) ↦ ((μ : (a : Set Ω) → ℝ≥0) (thickening a {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) : ℝ≥0))
  (𝓝[>] 0) (𝓝 ((μ : (a : Set Ω) → ℝ≥0) {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) : Filter ℝ≥0)
Tactic: simp only [NNReal.tendsto_coe]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
f : Ω →ᵇ ℝ
A : Set ℝ
A_finmeas : Ne (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) A : ℝ≥0∞) (∞ : ℝ≥0∞)
μ : ProbabilityMeasure Ω
t : ℝ
⊢ Tendsto (β := ℝ≥0) (fun (a : ℝ) ↦ ((μ : (a : Set Ω) → ℝ≥0) (thickening a {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) : ℝ≥0))
    (𝓝[>] 0) (𝓝 ((μ : (a : Set Ω) → ℝ≥0) {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) : Filter ℝ≥0)
have apply : Tendsto (β := ℝ≥0∞)
  (fun (a : ℝ) ↦ (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (thickening a {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) : ℝ≥0∞))
  (𝓝[>] 0) (𝓝 (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) : Filter ℝ≥0∞)
Tactic: apply (ENNReal.tendsto_toNNReal _).comp
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
f : Ω →ᵇ ℝ
A : Set ℝ
A_finmeas : Ne (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) A : ℝ≥0∞) (∞ : ℝ≥0∞)
μ : ProbabilityMeasure Ω
t : ℝ
apply :
  Tendsto (β := ℝ≥0∞)
    (fun (a : ℝ) ↦ (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (thickening a {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) : Filter ℝ≥0∞)
⊢ Tendsto (β := ℝ≥0) (fun (a : ℝ) ↦ ((μ : (a : Set Ω) → ℝ≥0) (thickening a {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) : ℝ≥0))
    (𝓝[>] 0) (𝓝 ((μ : (a : Set Ω) → ℝ≥0) {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) : Filter ℝ≥0)
have apply₁ : Ne (α := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {a : Ω | t ≤ (f : (a : Ω) → ℝ) a} : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: apply (ENNReal.tendsto_toNNReal _).comp
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
f : Ω →ᵇ ℝ
A : Set ℝ
A_finmeas : Ne (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) A : ℝ≥0∞) (∞ : ℝ≥0∞)
μ : ProbabilityMeasure Ω
t : ℝ
⊢ Tendsto (β := ℝ≥0∞)
    (fun (a : ℝ) ↦ (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (thickening a {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) : Filter ℝ≥0∞)
have apply : ∃ R > 0,
  Ne (α := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (thickening R {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) : ℝ≥0∞)
    (∞ : ℝ≥0∞)
Tactic: apply tendsto_measure_thickening_of_isClosed ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
f : Ω →ᵇ ℝ
A : Set ℝ
A_finmeas : Ne (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) A : ℝ≥0∞) (∞ : ℝ≥0∞)
μ : ProbabilityMeasure Ω
t : ℝ
apply :
  ∃ R > 0,
    Ne (α := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (thickening R {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) : ℝ≥0∞)
      (∞ : ℝ≥0∞)
⊢ Tendsto (β := ℝ≥0∞)
    (fun (a : ℝ) ↦ (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (thickening a {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) : Filter ℝ≥0∞)
have apply₁ : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}
Tactic: apply tendsto_measure_thickening_of_isClosed ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, ProbabilityMeasure.instTopologicalSpace] toMeasure
have refine : SeqContinuous.{u_1, u_1} (X := LevyProkhorov (ProbabilityMeasure Ω)) toMeasure
Tactic: refine SeqContinuous.continuous ?_
-- 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
⊢ Tendsto Ps atTop (𝓝 P)
have rw : ∀ (f : Ω →ᵇ ℝ),
  Tendsto (β := ℝ) (fun (i : ℕ) ↦ ∫ (ω : Ω), (f : (a : Ω) → ℝ) ω ∂(↑(Ps i) : Measure Ω)) atTop
    (𝓝 (∫ (ω : Ω), (f : (a : Ω) → ℝ) ω ∂(↑P : Measure Ω)))
Tactic: rw [ProbabilityMeasure.tendsto_iff_forall_integral_tendsto]
-- 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 : Ω →ᵇ ℝ),
    Tendsto (β := ℝ) (fun (i : ℕ) ↦ ∫ (ω : Ω), (f : (a : Ω) → ℝ) ω ∂(↑(Ps i) : Measure Ω)) atTop
      (𝓝 (∫ (ω : Ω), (f : (a : Ω) → ℝ) ω ∂(↑P : Measure Ω)))
have refine : ∀ (f f : Ω →ᵇ ℝ),
  0 ≤ f →
    LE.le (α := ℝ) (limsup (fun (i : ℕ) ↦ ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑(Ps i) : Measure Ω)) atTop)
      (∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑P : Measure Ω))
Tactic: refine fun f ↦ tendsto_integral_of_forall_limsup_integral_le_integral ?_ 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
⊢ LE.le (α := ℝ) (limsup (fun (i : ℕ) ↦ ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑(Ps i) : Measure Ω)) atTop)
    (∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑P : Measure Ω))
have pos : ∀ (f_zero : ‖f‖ = 0),
  LE.le (α := ℝ) (limsup (fun (i : ℕ) ↦ ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑(Ps i) : Measure Ω)) atTop)
    (∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑P : Measure Ω))
Tactic: by_cases f_zero : ‖f‖ = 0
-- 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
pos :
  ∀ (f_zero : ‖f‖ = 0),
    LE.le (α := ℝ) (limsup (fun (i : ℕ) ↦ ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑(Ps i) : Measure Ω)) atTop)
      (∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑P : Measure Ω))
⊢ LE.le (α := ℝ) (limsup (fun (i : ℕ) ↦ ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑(Ps i) : Measure Ω)) atTop)
    (∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑P : Measure Ω))
have neg : ∀ (f_zero : ¬‖f‖ = 0),
  LE.le (α := ℝ) (limsup (fun (i : ℕ) ↦ ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑(Ps i) : Measure Ω)) atTop)
    (∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑P : Measure Ω))
Tactic: by_cases f_zero : ‖f‖ = 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (hypothesis)
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
⊢ LE.le (α := ℝ) (limsup (fun (i : ℕ) ↦ ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑(Ps i) : Measure Ω)) atTop)
    (∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑P : Measure Ω))
have f_zero₁ : f = 0
Tactic: simp only [norm_eq_zero] at f_zero
Cleared hypotheses: f_zero
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (hypothesis)
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
⊢ LE.le (α := ℝ) (limsup (fun (i : ℕ) ↦ ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑(Ps i) : Measure Ω)) atTop)
    (∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑P : Measure Ω))
have norm_f_pos : 0 < ‖f‖
Tactic: have norm_f_pos : 0 < ‖f‖ := lt_of_le_of_ne (norm_nonneg _) (fun a => f_zero a.symm)
-- 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‖
⊢ LE.le (α := ℝ) (limsup (fun (i : ℕ) ↦ ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑(Ps i) : Measure Ω)) atTop)
    (∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑P : Measure Ω))
have neg : ∀ (ε : ℝ),
  0 < ε →
    limsup (fun (i : ℕ) ↦ ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑(Ps i) : Measure Ω)) atTop ≤
      ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑P : Measure Ω) + ε
Tactic: apply _root_.le_of_forall_pos_le_add
-- 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 < δ
⊢ limsup (fun (i : ℕ) ↦ ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑(Ps i) : Measure Ω)) atTop ≤
    ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑P : Measure Ω) + δ
have neg : ∀ᶠ (n : ℕ) in atTop,
  ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑(Ps n) : Measure Ω) ≤ ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑P : Measure Ω) + δ
Tactic: apply limsup_le_of_le ?_
-- 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 < δ
neg :
  ∀ᶠ (n : ℕ) in atTop,
    ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑(Ps n) : Measure Ω) ≤ ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑P : Measure Ω) + δ
⊢ limsup (fun (i : ℕ) ↦ ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑(Ps i) : Measure Ω)) atTop ≤
    ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑P : Measure Ω) + δ
have apply : IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) atTop fun (i : ℕ) ↦ ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑(Ps i) : Measure Ω)
Tactic: apply limsup_le_of_le ?_
-- 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 < δ
⊢ ∀ᶠ (n : ℕ) in atTop,
    ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑(Ps n) : Measure Ω) ≤ ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑P : Measure Ω) + δ
have neg : ∀ (εs : ℕ → ℝ),
  StrictAnti εs →
    ∀ (εs_pos : ∀ (n : ℕ), 0 < εs n) (εs_lim : Tendsto εs atTop (𝓝 0)),
      ∀ᶠ (n : ℕ) in atTop,
        ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑(Ps n) : Measure Ω) ≤ ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑P : Measure Ω) + δ
Tactic: obtain ⟨εs, _, εs_pos, εs_lim⟩ := exists_seq_strictAnti_tendsto (0 : ℝ)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (hypothesis)
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_pos : ∀ (n : ℕ), 0 < εs n
εs_lim : Tendsto εs atTop (𝓝 0)
⊢ ∀ᶠ (n : ℕ) in atTop,
    ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑(Ps n) : Measure Ω) ≤ ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑P : Measure Ω) + δ
have ε_of_room : Tendsto (fun (x : ℕ) ↦ dist (μs x) ν + εs x) atTop (𝓝 (HAdd.hAdd (α := ℝ) 0 0))
Tactic: have ε_of_room := Tendsto.add (tendsto_iff_dist_tendsto_zero.mp hμs) εs_lim
-- 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_pos : ∀ (n : ℕ), 0 < εs n
εs_lim : Tendsto εs atTop (𝓝 0)
ε_of_room : Tendsto (fun (x : ℕ) ↦ dist (μs x) ν + εs x) atTop (𝓝 (HAdd.hAdd (α := ℝ) 0 0))
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ dist (μs n) ν + εs n) atTop (𝓝[>] 0)
have rw : Tendsto (β := ℝ) (fun (n : ℕ) ↦ dist (μs n) ν + εs n) atTop (𝓝 0) ∧
  ∀ᶠ (n : ℕ) in atTop, Membership.mem (γ := Set ℝ) (Ioi 0) (dist (μs n) ν + εs n)
Tactic: rw [tendsto_nhdsWithin_iff]
-- 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_pos : ∀ (n : ℕ), 0 < εs n
εs_lim : Tendsto εs atTop (𝓝 0)
ε_of_room : Tendsto (fun (x : ℕ) ↦ dist (μs x) ν + εs x) atTop (𝓝 (HAdd.hAdd (α := ℝ) 0 0))
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ dist (μs n) ν + εs n) atTop (𝓝 0) ∧
    ∀ᶠ (n : ℕ) in atTop, Membership.mem (γ := Set ℝ) (Ioi 0) (dist (μs n) ν + εs n)
have refine : ∀ (n : ℕ), Membership.mem (γ := Set ℝ) (Ioi 0) (dist (μs n) ν + εs n)
Tactic: refine ⟨by simpa using ε_of_room, Eventually.of_forall fun n ↦ ?_⟩
-- 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_pos : ∀ (n : ℕ), 0 < εs n
εs_lim : Tendsto εs atTop (𝓝 0)
ε_of_room : Tendsto (fun (x : ℕ) ↦ dist (μs x) ν + εs x) atTop (𝓝 (HAdd.hAdd (α := ℝ) 0 0))
n : ℕ
⊢ 0 < dist (μs n) ν + εs n
have linarith : dist (μs n) ν + εs n ≤ 0 → dist (μs n) ν + εs n - 0 + (0 - εs n) + (0 - dist (μs n) ν) = 0
Tactic: linarith [εs_pos n, dist_nonneg (x := μs n) (y := ν)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (hypothesis)
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_pos : ∀ (n : ℕ), 0 < εs n
εs_lim : Tendsto εs atTop (𝓝 0)
ε_of_room : Tendsto (fun (x : ℕ) ↦ dist (μs x) ν + εs x) atTop (𝓝 (HAdd.hAdd (α := ℝ) 0 0))
⊢ ∀ᶠ (n : ℕ) in atTop,
    ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑(Ps n) : Measure Ω) ≤ ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑P : Measure Ω) + δ
have ε_of_room' : Tendsto (β := ℝ) (fun (n : ℕ) ↦ dist (μs n) ν + εs n) atTop (𝓝[>] 0)
Tactic: have ε_of_room' : Tendsto (fun n ↦ dist (μs n) ν + εs n) atTop (𝓝[>] 0) := by
      rw [tendsto_nhdsWithin_iff]
      refine ⟨by simpa using ε_of_room, Eventually.of_forall fun n ↦ ?_⟩
      · rw [mem_Ioi]
        linarith [εs_pos n, dist_nonneg (x := μs n) (y := ν)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (hypothesis)
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_pos : ∀ (n : ℕ), 0 < εs n
εs_lim : Tendsto εs atTop (𝓝 0)
ε_of_room : Tendsto (fun (x : ℕ) ↦ dist (μs x) ν + εs x) atTop (𝓝 (HAdd.hAdd (α := ℝ) 0 0))
ε_of_room' : Tendsto (β := ℝ) (fun (n : ℕ) ↦ dist (μs n) ν + εs n) atTop (𝓝[>] 0)
⊢ ∀ᶠ (n : ℕ) in atTop,
    ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑(Ps n) : Measure Ω) ≤ ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑P : Measure Ω) + δ
have ε_of_room₁ : Tendsto (β := ℝ) (fun (x : ℕ) ↦ dist (μs x) ν + εs x) atTop (𝓝 0)
Tactic: rw [add_zero] at ε_of_room
Cleared hypotheses: ε_of_room, ε_of_room'
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (hypothesis)
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_pos : ∀ (n : ℕ), 0 < εs n
ε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)
⊢ ∀ᶠ (n : ℕ) in atTop,
    ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑(Ps n) : Measure Ω) ≤ ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑P : Measure Ω) + δ
have key : Tendsto (α := ℕ) (β := ℝ)
  ((fun (ε : ℝ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 ‖f‖)) fun (t : ℝ) ↦
        (↑P : Measure Ω).real (thickening ε {a : Ω | t ≤ (f : (a : Ω) → ℝ) a})) ∘
    fun (n : ℕ) ↦ dist (μs n) ν + εs n)
  atTop
  (𝓝
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 ‖f‖)) fun (t : ℝ) ↦
      (↑P : Measure Ω).real {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}))
Tactic: have key := (tendsto_integral_meas_thickening_le f (A := Ioc 0 ‖f‖) (by simp) P).comp ε_of_room'