awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
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 : ℝ
⊢ ∃ R > 0,
    Ne (α := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (thickening R {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) : ℝ≥0∞)
      (∞ : ℝ≥0∞)

Tactic:
exact ⟨1, ⟨Real.zero_lt_one, measure_ne_top _ _⟩⟩
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
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 : ℝ
⊢ IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}

Tactic:
isClosed_le continuous_const f.continuous

Premises used: continuous_const, setOf, isClosed_le, BoundedContinuousFunction.continuous
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
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 : ℝ
⊢ IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}

Tactic:
exact isClosed_le continuous_const f.continuous

Premises used: continuous_const, isClosed_le, BoundedContinuousFunction.continuous
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
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 : ℝ
⊢ Ne (α := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {a : Ω | t ≤ (f : (a : Ω) → ℝ) a} : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
finiteness
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, ProbabilityMeasure.instTopologicalSpace] toMeasure

Tactic:
SeqContinuous.continuous ?_

Premises used: SeqContinuous.continuous
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
refine : SeqContinuous.{u_1, u_1} (X := LevyProkhorov (ProbabilityMeasure Ω)) toMeasure
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, ProbabilityMeasure.instTopologicalSpace] toMeasure

Tactic:
refine SeqContinuous.continuous ?_

Premises used: SeqContinuous.continuous
-- 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 (𝓝 ν)
set :
  let P := ν.toMeasure;
  Tendsto (toMeasure ∘ μs) atTop (𝓝 P)
⊢ Tendsto (toMeasure ∘ μs) atTop (𝓝 ν.toMeasure)

Tactic:
set P := ν.toMeasure

Premises used: MeasureTheory.LevyProkhorov.toMeasure
-- 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
set :
  let Ps := toMeasure ∘ μs;
  Tendsto Ps atTop (𝓝 P)
⊢ Tendsto (toMeasure ∘ μs) atTop (𝓝 P)

Tactic:
set Ps := LevyProkhorov.toMeasure ∘ μs

Premises used: MeasureTheory.LevyProkhorov.toMeasure
-- 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
rw :
  ∀ (f : Ω →ᵇ ℝ),
    Tendsto (β := ℝ) (fun (i : ℕ) ↦ ∫ (ω : Ω), (f : (a : Ω) → ℝ) ω ∂(↑(Ps i) : Measure Ω)) atTop
      (𝓝 (∫ (ω : Ω), (f : (a : Ω) → ℝ) ω ∂(↑P : Measure Ω)))
⊢ Tendsto Ps atTop (𝓝 P)

Tactic:
rw [ProbabilityMeasure.tendsto_iff_forall_integral_tendsto]

Premises used: MeasureTheory.ProbabilityMeasure.tendsto_iff_forall_integral_tendsto
-- 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 : Ω →ᵇ ℝ),
    Tendsto (β := ℝ) (fun (i : ℕ) ↦ ∫ (ω : Ω), (f : (a : Ω) → ℝ) ω ∂(↑(Ps i) : Measure Ω)) atTop
      (𝓝 (∫ (ω : Ω), (f : (a : Ω) → ℝ) ω ∂(↑P : Measure Ω)))

Tactic:
fun f ↦ tendsto_integral_of_forall_limsup_integral_le_integral ?_ f

Premises used: BoundedContinuousFunction.tendsto_integral_of_forall_limsup_integral_le_integral
-- 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
refine :
  ∀ (f f : Ω →ᵇ ℝ),
    0 ≤ f →
      LE.le (α := ℝ) (limsup (fun (i : ℕ) ↦ ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑(Ps i) : Measure Ω)) atTop)
        (∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑P : Measure Ω))
⊢ ∀ (f : Ω →ᵇ ℝ),
    Tendsto (β := ℝ) (fun (i : ℕ) ↦ ∫ (ω : Ω), (f : (a : Ω) → ℝ) ω ∂(↑(Ps i) : Measure Ω)) atTop
      (𝓝 (∫ (ω : Ω), (f : (a : Ω) → ℝ) ω ∂(↑P : Measure Ω)))

Tactic:
refine fun f ↦ tendsto_integral_of_forall_limsup_integral_le_integral ?_ f

Premises used: BoundedContinuousFunction.tendsto_integral_of_forall_limsup_integral_le_integral
-- 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
pos :
  ∀ (f_zero : ‖f‖ = 0),
    LE.le (α := ℝ) (limsup (fun (i : ℕ) ↦ ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑(Ps i) : Measure Ω)) atTop)
      (∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑P : Measure Ω))
neg :
  ∀ (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 Ω))

Tactic:
by_cases f_zero : ‖f‖ = 0
-- 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
⊢ f = 0

Tactic:
simp only [norm_eq_zero] at f_zero

Premises used: norm_eq_zero
-- 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
⊢ LE.le (α := ℝ) (limsup (fun (i : ℕ) ↦ ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑(Ps i) : Measure Ω)) atTop)
    (∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑P : Measure Ω))

Tactic:
simp [f_zero, limsup_const]

Premises used: Filter.limsup_const
-- 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
⊢ 0 < ‖f‖

Tactic:
have norm_f_pos : 0 < ‖f‖ := lt_of_le_of_ne (norm_nonneg _) (fun a => f_zero a.symm)
-- 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‖
neg :
  ∀ (ε : ℝ),
    0 < ε →
      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 Ω))

Tactic:
apply _root_.le_of_forall_pos_le_add

Premises used: le_of_forall_pos_le_add
-- 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 < δ
neg :
  ∀ᶠ (n : ℕ) in atTop,
    ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑(Ps n) : Measure Ω) ≤ ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑P : Measure Ω) + δ
apply :
  IsCoboundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) atTop fun (i : ℕ) ↦ ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑(Ps i) : Measure Ω)
⊢ limsup (fun (i : ℕ) ↦ ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑(Ps i) : Measure Ω)) atTop ≤
    ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑P : Measure Ω) + δ

Tactic:
apply limsup_le_of_le ?_

Premises used: Filter.limsup_le_of_le
-- 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 < δ
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 Ω) + δ
⊢ ∀ᶠ (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 : ℝ)

Premises used: exists_seq_strictAnti_tendsto, OfNat.ofNat
-- 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_pos : ∀ (n : ℕ), 0 < εs n
εs_lim : Tendsto εs atTop (𝓝 0)
⊢ 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
-- 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_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))
rw :
  Tendsto (β := ℝ) (fun (n : ℕ) ↦ dist (μs n) ν + εs n) atTop (𝓝 0) ∧
    ∀ᶠ (n : ℕ) in atTop, Membership.mem (γ := Set ℝ) (Ioi 0) (dist (μs n) ν + εs n)
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ dist (μs n) ν + εs n) atTop (𝓝[>] 0)

Tactic:
rw [tendsto_nhdsWithin_iff]

Premises used: tendsto_nhdsWithin_iff
-- 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_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)

Tactic:
simpa using ε_of_room
-- 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_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))
refine : ∀ (n : ℕ), Membership.mem (γ := Set ℝ) (Ioi 0) (dist (μs n) ν + εs n)
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ dist (μs n) ν + εs n) atTop (𝓝 0) ∧
    ∀ᶠ (n : ℕ) in atTop, Membership.mem (γ := Set ℝ) (Ioi 0) (dist (μs n) ν + εs n)

Tactic:
refine ⟨by simpa using ε_of_room, Eventually.of_forall fun n ↦ ?_⟩
-- 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_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 : ℕ
linarith : dist (μs n) ν + εs n ≤ 0 → dist (μs n) ν + εs n - 0 + (0 - εs n) + (0 - dist (μs n) ν) = 0
⊢ 0 < dist (μs n) ν + εs n

Tactic:
linarith [εs_pos n, dist_nonneg (x := μs n) (y := ν)]

Premises used: dist_nonneg
-- 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_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)

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 := ν)]
-- 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_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)
⊢ Tendsto (β := ℝ) (fun (x : ℕ) ↦ dist (μs x) ν + εs x) atTop (𝓝 0)

Tactic:
rw [add_zero] at ε_of_room

Premises used: add_zero
-- 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_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)
ε_of_room₁ : Tendsto (β := ℝ) (fun (x : ℕ) ↦ dist (μs x) ν + εs x) atTop (𝓝 0)
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ dist (μs n) ν + εs n) atTop (𝓝[>] 0)

Tactic:
rw [add_zero] at ε_of_room

Premises used: add_zero
-- 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_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)
⊢ Ne (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) (Ioc 0 ‖f‖) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
simp
-- 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_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)
⊢ 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'
-- 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_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)
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}))
z : ℝ
linarith : z + δ / 2 ≤ z → 2 / 2 = 1
linarith₁ : z + δ / 2 ≤ z → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : z + δ / 2 ≤ z → GT.gt (α := ℝ) 2 0
linarith₃ : z + δ / 2 ≤ z → 0 - δ + (2 * z + 1 * δ - 2 * z) = 0
⊢ z < z + δ / 2

Tactic:
linarith
-- 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_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)
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}))
⊢ ∀ (z : ℝ), Iio (z + δ / 2) ∈ 𝓝 z

Tactic:
have aux : ∀ (z : ℝ), Iio (z + δ / 2) ∈ 𝓝 z := fun z ↦ Iio_mem_nhds (by linarith)