-- Mathlib/MeasureTheory/Measure/LevyProkhorovMetric.lean
/-- The identity map `LevyProkhorov (ProbabilityMeasure Ω) → ProbabilityMeasure Ω` is continuous. -/
lemma LevyProkhorov.continuous_equiv_probabilityMeasure :
    Continuous (LevyProkhorov.equiv (α := ProbabilityMeasure Ω))

Proof state:
case h.refine_4
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : PseudoMetricSpace Ω
inst✝ : OpensMeasurableSpace Ω
μs : ℕ → LevyProkhorov (ProbabilityMeasure Ω)
ν : LevyProkhorov (ProbabilityMeasure Ω)
hμs : Tendsto μs atTop (𝓝 ν)
P : ProbabilityMeasure Ω := (equiv (ProbabilityMeasure Ω)) ν
Ps : ℕ → ProbabilityMeasure Ω := fun n => (equiv (ProbabilityMeasure Ω)) (μs n)
f✝ 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 ε => ∫ (t : ℝ) in Ioc 0 ‖f‖, (↑(P (thickening ε {a | t ≤ f a}))).toReal) ∘ fun n => dist (μs n) ν + εs n)
    atTop (𝓝 (∫ (t : ℝ) in Ioc 0 ‖f‖, (↑(P {a | t ≤ f a})).toReal))
aux : ∀ (z : ℝ), Iio (z + δ / 2) ∈ 𝓝 z
n : ℕ
hn :
  ((fun ε => ∫ (t : ℝ) in Ioc 0 ‖f‖, (↑(P (thickening ε {a | t ≤ f a}))).toReal) ∘ fun n => dist (μs n) ν + εs n) n <
    (∫ (t : ℝ) in Ioc 0 ‖f‖, (↑(P {a | t ≤ f a})).toReal) + δ / 2
hn' : dist (μs n) ν + εs n < ‖f‖⁻¹ * δ / 2
εs_pos : 0 < εs n
bound :
  ∫ (ω : Ω), f ω ∂↑(Ps n) ≤
    (∫ (t : ℝ) in Ioc 0 ‖f‖, (↑P (thickening (dist (μs n) ν + εs n) {a | t ≤ f a})).toReal) +
      (dist (μs n) ν + εs n) * ‖f‖
⊢ (∫ (t : ℝ) in Ioc 0 ‖f‖, (↑(P {a | t ≤ f a})).toReal) + δ / 2 + (dist (μs n) ν + εs n) * ‖f‖ ≤
    (∫ (t : ℝ) in Ioc 0 ‖f‖, (↑P {a | t ≤ f a}).toReal) + δ

Tactic:
simp only [ProbabilityMeasure.ennreal_coeFn_eq_coeFn_toMeasure]

Result:
case h.refine_4
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : PseudoMetricSpace Ω
inst✝ : OpensMeasurableSpace Ω
μs : ℕ → LevyProkhorov (ProbabilityMeasure Ω)
ν : LevyProkhorov (ProbabilityMeasure Ω)
hμs : Tendsto μs atTop (𝓝 ν)
P : ProbabilityMeasure Ω := (equiv (ProbabilityMeasure Ω)) ν
Ps : ℕ → ProbabilityMeasure Ω := fun n => (equiv (ProbabilityMeasure Ω)) (μs n)
f✝ 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 ε => ∫ (t : ℝ) in Ioc 0 ‖f‖, (↑(P (thickening ε {a | t ≤ f a}))).toReal) ∘ fun n => dist (μs n) ν + εs n)
    atTop (𝓝 (∫ (t : ℝ) in Ioc 0 ‖f‖, (↑(P {a | t ≤ f a})).toReal))
aux : ∀ (z : ℝ), Iio (z + δ / 2) ∈ 𝓝 z
n : ℕ
hn :
  ((fun ε => ∫ (t : ℝ) in Ioc 0 ‖f‖, (↑(P (thickening ε {a | t ≤ f a}))).toReal) ∘ fun n => dist (μs n) ν + εs n) n <
    (∫ (t : ℝ) in Ioc 0 ‖f‖, (↑(P {a | t ≤ f a})).toReal) + δ / 2
hn' : dist (μs n) ν + εs n < ‖f‖⁻¹ * δ / 2
εs_pos : 0 < εs n
bound :
  ∫ (ω : Ω), f ω ∂↑(Ps n) ≤
    (∫ (t : ℝ) in Ioc 0 ‖f‖, (↑P (thickening (dist (μs n) ν + εs n) {a | t ≤ f a})).toReal) +
      (dist (μs n) ν + εs n) * ‖f‖
⊢ (∫ (t : ℝ) in Ioc 0 ‖f‖, (↑P {a | t ≤ f a}).toReal) + δ / 2 + (dist (μs n) ν + εs n) * ‖f‖ ≤
    (∫ (t : ℝ) in Ioc 0 ‖f‖, (↑P {a | t ≤ f a}).toReal) + δ

Proof state:
case neg.h.intro.intro.intro
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : PseudoMetricSpace Ω
inst✝ : OpensMeasurableSpace Ω
μs : ℕ → LevyProkhorov (ProbabilityMeasure Ω)
ν : LevyProkhorov (ProbabilityMeasure Ω)
hμs : Tendsto μs atTop (𝓝 ν)
P : ProbabilityMeasure Ω := (equiv (ProbabilityMeasure Ω)) ν
Ps : ℕ → ProbabilityMeasure Ω := fun n => (equiv (ProbabilityMeasure Ω)) (μs n)
f✝ 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 x ∂↑((⇑(equiv (ProbabilityMeasure Ω)) ∘ μs) n) ≤ ∫ (x : Ω), f x ∂↑P + δ

Tactic:
have ε_of_room := Tendsto.add (tendsto_iff_dist_tendsto_zero.mp hμs) εs_lim

Result:
case neg.h.intro.intro.intro
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : PseudoMetricSpace Ω
inst✝ : OpensMeasurableSpace Ω
μs : ℕ → LevyProkhorov (ProbabilityMeasure Ω)
ν : LevyProkhorov (ProbabilityMeasure Ω)
hμs : Tendsto μs atTop (𝓝 ν)
P : ProbabilityMeasure Ω := (equiv (ProbabilityMeasure Ω)) ν
Ps : ℕ → ProbabilityMeasure Ω := fun n => (equiv (ProbabilityMeasure Ω)) (μs n)
f✝ 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 + 0))
⊢ ∀ᶠ (n : ℕ) in atTop, ∫ (x : Ω), f x ∂↑((⇑(equiv (ProbabilityMeasure Ω)) ∘ μs) n) ≤ ∫ (x : Ω), f x ∂↑P + δ

Proof state:
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : PseudoMetricSpace Ω
inst✝ : OpensMeasurableSpace Ω
μs : ℕ → LevyProkhorov (ProbabilityMeasure Ω)
ν : LevyProkhorov (ProbabilityMeasure Ω)
hμs : Tendsto μs atTop (𝓝 ν)
P : ProbabilityMeasure Ω := (equiv (ProbabilityMeasure Ω)) ν
Ps : ℕ → ProbabilityMeasure Ω := fun n => (equiv (ProbabilityMeasure Ω)) (μs n)
⊢ Tendsto (⇑(equiv (ProbabilityMeasure Ω)) ∘ μs) atTop (𝓝 P)

Tactic:
rw [ProbabilityMeasure.tendsto_iff_forall_integral_tendsto]

Result:
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : PseudoMetricSpace Ω
inst✝ : OpensMeasurableSpace Ω
μs : ℕ → LevyProkhorov (ProbabilityMeasure Ω)
ν : LevyProkhorov (ProbabilityMeasure Ω)
hμs : Tendsto μs atTop (𝓝 ν)
P : ProbabilityMeasure Ω := (equiv (ProbabilityMeasure Ω)) ν
Ps : ℕ → ProbabilityMeasure Ω := fun n => (equiv (ProbabilityMeasure Ω)) (μs n)
⊢ ∀ (f : Ω →ᵇ ℝ),
    Tendsto (fun i => ∫ (ω : Ω), f ω ∂↑((⇑(equiv (ProbabilityMeasure Ω)) ∘ μs) i)) atTop (𝓝 (∫ (ω : Ω), f ω ∂↑P))