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_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}))
aux : ∀ (z : ℝ), Iio (z + δ / 2) ∈ 𝓝 z
h :
  ∀ (n : ℕ)
    (hn :
      Membership.mem (γ := Set ℕ)
        (((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) ⁻¹'
          Iio
            ((@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 ‖f‖)) fun (t : ℝ) ↦
                (↑P : Measure Ω).real {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) +
              δ / 2))
        n)
    (hn' : Membership.mem (γ := Set ℕ) ((fun (x : ℕ) ↦ dist (μs x) ν + εs x) ⁻¹' Iio (‖f‖⁻¹ * δ / 2)) n),
    ∫ (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:
filter_upwards [key (aux _), ε_of_room <| Iio_mem_nhds <| half_pos <|
                      mul_pos (inv_pos.mpr norm_f_pos) δ_pos]
      with n hn hn'

Premises used: Iff.mpr, Iio_mem_nhds, half_pos, inv_pos, mul_pos
-- 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}))
aux : ∀ (z : ℝ), Iio (z + δ / 2) ∈ 𝓝 z
n : ℕ
hn :
  Membership.mem (γ := Set ℕ)
    (((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) ⁻¹'
      Iio
        ((@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 ‖f‖)) fun (t : ℝ) ↦
            (↑P : Measure Ω).real {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) +
          δ / 2))
    n
hn' : Membership.mem (γ := Set ℕ) ((fun (x : ℕ) ↦ dist (μs x) ν + εs x) ⁻¹' Iio (‖f‖⁻¹ * δ / 2)) n
⊢ (@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

Tactic:
simp only [mem_preimage, Function.comp_def, mem_Iio] at *

Premises used: Set.mem_Iio, Function.comp_def, Set.mem_preimage
-- 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}))
aux : ∀ (z : ℝ), Iio (z + δ / 2) ∈ 𝓝 z
n : ℕ
hn :
  Membership.mem (γ := Set ℕ)
    (((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) ⁻¹'
      Iio
        ((@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 ‖f‖)) fun (t : ℝ) ↦
            (↑P : Measure Ω).real {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) +
          δ / 2))
    n
hn' : Membership.mem (γ := Set ℕ) ((fun (x : ℕ) ↦ dist (μs x) ν + εs x) ⁻¹' Iio (‖f‖⁻¹ * δ / 2)) 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
⊢ dist (μs n) ν + εs n < ‖f‖⁻¹ * δ / 2

Tactic:
simp only [mem_preimage, Function.comp_def, mem_Iio] at *

Premises used: Set.mem_Iio, Function.comp_def, Set.mem_preimage
-- 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 (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
⊢ 0 < εs n

Tactic:
specialize εs_pos 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_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 :
  ∀
    (bound :
      ∫ (ω : Ω), (f : (a : Ω) → ℝ) ω ∂(↑(Ps n) : Measure Ω) ≤
        (@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})) +
          (dist (μs n) ν + εs n) * ‖f‖),
    ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑(Ps n) : Measure Ω) ≤ ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑P : Measure Ω) + δ
h₁ : 0 < dist (μs n) ν + εs n
h₂ : levyProkhorovEDist (↑(Ps n) : Measure Ω) (↑P : Measure Ω) < ENNReal.ofReal (dist (μs n) ν + εs n)
h₃ : (ae (↑(Ps n) : Measure Ω)).EventuallyLE (β := ℝ) 0 (⇑f : (a : Ω) → ℝ)
⊢ ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑(Ps n) : Measure Ω) ≤ ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑P : Measure Ω) + δ

Tactic:
have bound := BoundedContinuousFunction.integral_le_of_levyProkhorovEDist_lt
                    (Ps n) P (ε := dist (μs n) ν + εs n) ?_ ?_ f ?_
-- 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
bound :
  ∫ (ω : Ω), (f : (a : Ω) → ℝ) ω ∂(↑(Ps n) : Measure Ω) ≤
    (@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})) +
      (dist (μs n) ν + εs n) * ‖f‖
h :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 ‖f‖)) fun (t : ℝ) ↦
        (↑P : Measure Ω).real {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) +
      (δ / 2 + ‖f‖ * (dist (μs n) ν + εs n)) ≤
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 ‖f‖)) fun (t : ℝ) ↦
        (↑P : Measure Ω).real {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) +
      δ
⊢ ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑(Ps n) : Measure Ω) ≤ ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑P : Measure Ω) + δ

Tactic:
grw [bound, hn, BoundedContinuousFunction.integral_eq_integral_meas_le _ _ <| .of_forall f_nn,
        add_assoc, mul_comm]

Premises used: add_assoc, MeasureTheory.BoundedContinuousFunction.integral_eq_integral_meas_le, mul_comm
-- 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
bound :
  ∫ (ω : Ω), (f : (a : Ω) → ℝ) ω ∂(↑(Ps n) : Measure Ω) ≤
    (@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})) +
      (dist (μs n) ν + εs n) * ‖f‖
h : δ / 2 + ‖f‖ * (dist (μs n) ν + εs n) ≤ δ
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 ‖f‖)) fun (t : ℝ) ↦
        (↑P : Measure Ω).real {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) +
      (δ / 2 + ‖f‖ * (dist (μs n) ν + εs n)) ≤
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 ‖f‖)) fun (t : ℝ) ↦
        (↑P : Measure Ω).real {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) +
      δ

Tactic:
gcongr
-- 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
bound :
  ∫ (ω : Ω), (f : (a : Ω) → ℝ) ω ∂(↑(Ps n) : Measure Ω) ≤
    (@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})) +
      (dist (μs n) ν + εs n) * ‖f‖
bc : 0 ≤ ‖f‖
⊢ δ / 2 + ‖f‖ * (dist (μs n) ν + εs n) ≤ δ / 2 + ‖f‖ * (‖f‖⁻¹ * δ / 2)

Tactic:
gcongr
-- 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
bound :
  ∫ (ω : Ω), (f : (a : Ω) → ℝ) ω ∂(↑(Ps n) : Measure Ω) ≤
    (@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})) +
      (dist (μs n) ν + εs n) * ‖f‖
⊢ δ / 2 + ‖f‖ * (‖f‖⁻¹ * δ / 2) = δ

Tactic:
field
-- 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
bound :
  ∫ (ω : Ω), (f : (a : Ω) → ℝ) ω ∂(↑(Ps n) : Measure Ω) ≤
    (@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})) +
      (dist (μs n) ν + εs n) * ‖f‖
δ₁ : δ / 2 + ‖f‖ * (dist (μs n) ν + εs n) ≤ δ / 2 + ‖f‖ * (‖f‖⁻¹ * δ / 2)
δ₂ : δ / 2 + ‖f‖ * (‖f‖⁻¹ * δ / 2) = δ
⊢ δ / 2 + ‖f‖ * (dist (μs n) ν + εs n) ≤ δ

Tactic:
calc
        δ / 2 + ‖f‖ * (dist (μs n) ν + εs n)
        _ ≤ δ / 2 + ‖f‖ * (‖f‖⁻¹ * δ / 2) := by gcongr
        _ = δ := by field

Premises used: Norm.norm, HMul.hMul, HDiv.hDiv, Inv.inv, HAdd.hAdd, Dist.dist, OfNat.ofNat