-- 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
Ω : 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
⊢ ∫ (x : Ω), f x ∂↑((⇑(equiv (ProbabilityMeasure Ω)) ∘ μs) n) ≤ ∫ (x : Ω), f x ∂↑P + δ

Tactic:
have bound := BoundedContinuousFunction.integral_le_of_levyProkhorovEDist_lt
                (Ps n) P (ε := dist (μs n) ν + εs n) ?_ ?_ f ?_

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‖
⊢ ∫ (x : Ω), f x ∂↑((⇑(equiv (ProbabilityMeasure Ω)) ∘ μs) n) ≤ ∫ (x : Ω), f x ∂↑P + δ

case h.refine_1
Ω : 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
⊢ 0 < dist (μs n) ν + εs n

case h.refine_2
Ω : 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
⊢ levyProkhorovEDist ↑(Ps n) ↑P < ENNReal.ofReal (dist (μs n) ν + εs n)

case h.refine_3
Ω : 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
⊢ 0 ≤ᶠ[ae ↑(Ps n)] ⇑f