awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
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
⊢ 0 < dist (μs n) ν + εs n

Tactic:
positivity
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
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
⊢ 0 ≤ dist (μs n) ν

Tactic:
positivity
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
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
⊢ 0 ≤ εs n

Tactic:
positivity
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
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 :
  levyProkhorovEDist (↑(Ps n) : Measure Ω) (↑P : Measure Ω) + 0 < ENNReal.ofReal (dist (μs n) ν) + ENNReal.ofReal (εs n)
⊢ levyProkhorovEDist (↑(Ps n) : Measure Ω) (↑P : Measure Ω) < ENNReal.ofReal (dist (μs n) ν + εs n)

Tactic:
rw [ENNReal.ofReal_add (by positivity) (by positivity), ← add_zero (levyProkhorovEDist _ _)]

Premises used: ENNReal.ofReal_add, add_zero, MeasureTheory.levyProkhorovEDist
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
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
apply : levyProkhorovEDist (↑(Ps n) : Measure Ω) (↑P : Measure Ω) = ENNReal.ofReal (dist (μs n) ν)
⊢ levyProkhorovEDist (↑(Ps n) : Measure Ω) (↑P : Measure Ω) + 0 < ENNReal.ofReal (dist (μs n) ν) + ENNReal.ofReal (εs n)

Tactic:
apply ENNReal.add_lt_add_of_le_of_lt (levyProkhorovEDist_ne_top _ _)
            (le_of_eq ?_) (ofReal_pos.mpr εs_pos)

Premises used: Iff.mpr, ENNReal.add_lt_add_of_le_of_lt, MeasureTheory.levyProkhorovEDist_ne_top, ENNReal.ofReal_pos, le_of_eq
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
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
rw :
  levyProkhorovEDist (↑(Ps n) : Measure Ω) (↑P : Measure Ω) =
    levyProkhorovEDist (↑(μs n).toMeasure : Measure Ω) (↑ν.toMeasure : Measure Ω)
⊢ levyProkhorovEDist (↑(Ps n) : Measure Ω) (↑P : Measure Ω) = ENNReal.ofReal (dist (μs n) ν)

Tactic:
rw [LevyProkhorov.dist_probabilityMeasure_def, levyProkhorovDist,
        ofReal_toReal (levyProkhorovEDist_ne_top _ _)]

Premises used: MeasureTheory.LevyProkhorov.dist_probabilityMeasure_def, ENNReal.ofReal_toReal, MeasureTheory.levyProkhorovEDist_ne_top, MeasureTheory.levyProkhorovDist
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
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 Ω) =
    levyProkhorovEDist (↑(μs n).toMeasure : Measure Ω) (↑ν.toMeasure : Measure Ω)

Tactic:
rfl
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
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
⊢ (ae (↑(Ps n) : Measure Ω)).EventuallyLE (β := ℝ) 0 (⇑f : (a : Ω) → ℝ)

Tactic:
Eventually.of_forall f_nn

Premises used: Filter.Eventually.of_forall, Filter.EventuallyLE
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
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
⊢ (ae (↑(Ps n) : Measure Ω)).EventuallyLE (β := ℝ) 0 (⇑f : (a : Ω) → ℝ)

Tactic:
exact Eventually.of_forall f_nn

Premises used: Filter.Eventually.of_forall
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
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 < δ
simp : ∃ (b : ℝ), ∀ (a : ℝ) (x : ℕ) (h : ∀ b ≥ x, ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑(Ps b) : Measure Ω) ≤ a), b ≤ a
⊢ IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) atTop fun (i : ℕ) ↦ ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑(Ps i) : Measure Ω)

Tactic:
simp only [IsCoboundedUnder, IsCobounded, eventually_map, eventually_atTop,
               forall_exists_index]

Premises used: Filter.IsCoboundedUnder, forall_exists_index, Filter.eventually_map, Filter.IsCobounded, Filter.eventually_atTop
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
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 < δ
⊢ ∃ (b : ℝ), ∀ (a : ℝ) (x : ℕ) (h : ∀ b ≥ x, ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑(Ps b) : Measure Ω) ≤ a), b ≤ a

Tactic:
⟨0, fun a i hia ↦ le_trans (integral_nonneg f_nn) (hia i le_rfl)⟩

Premises used: MeasureTheory.integral_nonneg, le_rfl, Exists.intro, OfNat.ofNat, le_trans
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
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 < δ
⊢ ∃ (b : ℝ), ∀ (a : ℝ) (x : ℕ) (h : ∀ b ≥ x, ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑(Ps b) : Measure Ω) ≤ a), b ≤ a

Tactic:
refine ⟨0, fun a i hia ↦ le_trans (integral_nonneg f_nn) (hia i le_rfl)⟩
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
⊢ LE.le.{u_1} (α := TopologicalSpace (ProbabilityMeasure Ω)) (TopologicalSpace.coinduced toMeasure inferInstance)
    inferInstance

Tactic:
LevyProkhorov.continuous_toMeasure_probabilityMeasure.coinduced_le

Premises used: MeasureTheory.LevyProkhorov.continuous_toMeasure_probabilityMeasure, Continuous.coinduced_le
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
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
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
⊢ {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 < ε

Premises used: MeasureTheory.ProbabilityMeasure.toMeasure, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
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

Tactic:
Eventually.of_forall (fun _ ↦ lt_of_lt_of_le easy le_add_self)

Premises used: Set.Mem, Filter.Eventually, setOf, Filter.Eventually.of_forall, le_add_self, lt_of_lt_of_le
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
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

Tactic:
exact Eventually.of_forall (fun _ ↦ lt_of_lt_of_le easy le_add_self)

Premises used: Filter.Eventually.of_forall, le_add_self, lt_of_lt_of_le
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
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
pos :
  ∀ (ε_top : ε = ∞),
    {Q : ProbabilityMeasure Ω |
        ((↑P : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G <
          HAdd.hAdd (α := ℝ≥0∞) (((↑Q : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G : ℝ≥0∞) ε} ∈
      𝓝 P
neg :
  ∀ (ε_top : ¬ε = ∞),
    {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

Tactic:
by_cases ε_top : ε = ∞
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
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
ε_top : ε = ∞
⊢ {Q : ProbabilityMeasure Ω |
      ((↑P : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G <
        HAdd.hAdd (α := ℝ≥0∞) (((↑Q : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G : ℝ≥0∞) ε} ∈
    𝓝 P

Tactic:
simp [ε_top, measure_lt_top]

Premises used: MeasureTheory.measure_lt_top
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
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
ε_top : ¬ε = ∞
⊢ Ne (α := ℝ≥0∞) (((↑P : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
finiteness