awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ ν κ : Measure Ω
LPμν_finite : ¬levyProkhorovEDist μ ν = ∞
LPνκ_finite : ¬levyProkhorovEDist ν κ = ∞
ε : ℝ≥0∞
B : Set Ω
ε_pos : 0 < ε
ε_lt_top : ε < ∞
B_mble : MeasurableSet B
half_ε_pos : 0 < ε / 2
r : ℝ≥0∞ := levyProkhorovEDist μ ν + ε / 2
s : ℝ≥0∞ := levyProkhorovEDist ν κ + ε / 2
lt_r : levyProkhorovEDist μ ν < r
lt_s : levyProkhorovEDist ν κ < s
hs_add_r : s + r = levyProkhorovEDist μ ν + levyProkhorovEDist ν κ + ε
hs_add_r' : s.toReal + r.toReal = (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ + ε).toReal
rw :
  HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (thickening r.toReal (thickening s.toReal B)) : ℝ≥0∞) (r + s) =
    HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (thickening r.toReal (thickening s.toReal B)) : ℝ≥0∞) (s + r)
rw₁ rw₂ :
  HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (thickening r.toReal (thickening s.toReal B)) : ℝ≥0∞) (s + r) =
    HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (thickening r.toReal (thickening s.toReal B)) : ℝ≥0∞) (s + r)
⊢ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (thickening r.toReal (thickening s.toReal B)) : ℝ≥0∞) r + s =
    HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (thickening r.toReal (thickening s.toReal B)) : ℝ≥0∞) (s + r)

Tactic:
rw [add_assoc, add_comm r]

Premises used: add_assoc, add_comm
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ ν κ : Measure Ω
LPμν_finite : ¬levyProkhorovEDist μ ν = ∞
LPνκ_finite : ¬levyProkhorovEDist ν κ = ∞
ε : ℝ≥0∞
B : Set Ω
ε_pos : 0 < ε
ε_lt_top : ε < ∞
B_mble : MeasurableSet B
half_ε_pos : 0 < ε / 2
r : ℝ≥0∞ := levyProkhorovEDist μ ν + ε / 2
s : ℝ≥0∞ := levyProkhorovEDist ν κ + ε / 2
lt_r : levyProkhorovEDist μ ν < r
lt_s : levyProkhorovEDist ν κ < s
hs_add_r : s + r = levyProkhorovEDist μ ν + levyProkhorovEDist ν κ + ε
hs_add_r' : s.toReal + r.toReal = (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ + ε).toReal
grw grw₁ :
  HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (thickening (r.toReal + s.toReal) B) : ℝ≥0∞) (s + r) ≤
    HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (thickening (r.toReal + s.toReal) B) : ℝ≥0∞) (s + r)
⊢ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (thickening r.toReal (thickening s.toReal B)) : ℝ≥0∞) (s + r) ≤
    HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (thickening (r.toReal + s.toReal) B) : ℝ≥0∞) (s + r)

Tactic:
grw [thickening_thickening_subset]

Premises used: Metric.thickening_thickening_subset
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ ν κ : Measure Ω
LPμν_finite : ¬levyProkhorovEDist μ ν = ∞
LPνκ_finite : ¬levyProkhorovEDist ν κ = ∞
ε : ℝ≥0∞
B : Set Ω
ε_pos : 0 < ε
ε_lt_top : ε < ∞
B_mble : MeasurableSet B
half_ε_pos : 0 < ε / 2
r : ℝ≥0∞ := levyProkhorovEDist μ ν + ε / 2
s : ℝ≥0∞ := levyProkhorovEDist ν κ + ε / 2
lt_r : levyProkhorovEDist μ ν < r
lt_s : levyProkhorovEDist ν κ < s
hs_add_r : s + r = levyProkhorovEDist μ ν + levyProkhorovEDist ν κ + ε
hs_add_r' : s.toReal + r.toReal = (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ + ε).toReal
rw rw₁ :
  HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (thickening (s.toReal + r.toReal) B) : ℝ≥0∞) (s + r) =
    HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (thickening (s.toReal + r.toReal) B) : ℝ≥0∞) (s + r)
⊢ HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (thickening (r.toReal + s.toReal) B) : ℝ≥0∞) (s + r) =
    HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (thickening (s.toReal + r.toReal) B) : ℝ≥0∞) (s + r)

Tactic:
rw [add_comm r.toReal]

Premises used: add_comm, ENNReal.toReal
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ ν κ : Measure Ω
LPμν_finite : ¬levyProkhorovEDist μ ν = ∞
LPνκ_finite : ¬levyProkhorovEDist ν κ = ∞
ε : ℝ≥0∞
B : Set Ω
ε_pos : 0 < ε
ε_lt_top : ε < ∞
B_mble : MeasurableSet B
half_ε_pos : 0 < ε / 2
r : ℝ≥0∞ := levyProkhorovEDist μ ν + ε / 2
s : ℝ≥0∞ := levyProkhorovEDist ν κ + ε / 2
lt_r : levyProkhorovEDist μ ν < r
lt_s : levyProkhorovEDist ν κ < s
hs_add_r : s + r = levyProkhorovEDist μ ν + levyProkhorovEDist ν κ + ε
hs_add_r' : s.toReal + r.toReal = (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ + ε).toReal
calc :
  HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) (thickening s.toReal B) : ℝ≥0∞) s ≤
    HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (thickening r.toReal (thickening s.toReal B)) : ℝ≥0∞) r + s
calc₁ :
  HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (thickening r.toReal (thickening s.toReal B)) : ℝ≥0∞) r + s =
    HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (thickening r.toReal (thickening s.toReal B)) : ℝ≥0∞) (s + r)
calc₂ :
  HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (thickening r.toReal (thickening s.toReal B)) : ℝ≥0∞) (s + r) ≤
    HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (thickening (r.toReal + s.toReal) B) : ℝ≥0∞) (s + r)
calc₃ :
  HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (thickening (r.toReal + s.toReal) B) : ℝ≥0∞) (s + r) =
    HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (thickening (s.toReal + r.toReal) B) : ℝ≥0∞) (s + r)
⊢ (κ : (a : Set Ω) → ℝ≥0∞) B ≤
    HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) (thickening (s.toReal + r.toReal) B) : ℝ≥0∞) (s + r)

Tactic:
calc κ B ≤ ν (thickening s.toReal B) + s :=
      right_measure_le_of_levyProkhorovEDist_lt lt_s B_mble
    _ ≤ μ (thickening r.toReal (thickening s.toReal B)) + r + s := by
      grw [right_measure_le_of_levyProkhorovEDist_lt lt_r isOpen_thickening.measurableSet]
    _ = μ (thickening r.toReal (thickening s.toReal B)) + (s + r) := by rw [add_assoc, add_comm r]
    _ ≤ μ (thickening (r.toReal + s.toReal) B) + (s + r) := by grw [thickening_thickening_subset]
    _ = μ (thickening (s.toReal + r.toReal) B) + (s + r) := by rw [add_comm r.toReal]

Premises used: Metric.thickening, ENNReal.toReal, HAdd.hAdd, MeasureTheory.right_measure_le_of_levyProkhorovEDist_lt, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
μ : Measure Ω
⊢ levyProkhorovDist μ μ = 0

Tactic:
simp only [levyProkhorovDist, levyProkhorovEDist_self, toReal_zero]

Premises used: MeasureTheory.levyProkhorovDist, ENNReal.toReal_zero, MeasureTheory.levyProkhorovEDist_self
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
μ ν : Measure Ω
⊢ levyProkhorovDist μ ν = levyProkhorovDist ν μ

Tactic:
simp only [levyProkhorovDist, levyProkhorovEDist_comm]

Premises used: MeasureTheory.levyProkhorovEDist_comm, MeasureTheory.levyProkhorovDist
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ ν κ : Measure Ω
inst_3 : IsFiniteMeasure μ
inst_4 : IsFiniteMeasure ν
inst_5 : IsFiniteMeasure κ
⊢ levyProkhorovEDist μ ν ≠ ∞

Tactic:
have dμν_finite := (levyProkhorovEDist_lt_top μ ν).ne
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ ν κ : Measure Ω
inst_3 : IsFiniteMeasure μ
inst_4 : IsFiniteMeasure ν
inst_5 : IsFiniteMeasure κ
dμν_finite : levyProkhorovEDist μ ν ≠ ∞
⊢ levyProkhorovEDist ν κ ≠ ∞

Tactic:
have dνκ_finite := (levyProkhorovEDist_lt_top ν κ).ne
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ ν κ : Measure Ω
inst_3 : IsFiniteMeasure μ
inst_4 : IsFiniteMeasure ν
inst_5 : IsFiniteMeasure κ
dμν_finite : levyProkhorovEDist μ ν ≠ ∞
dνκ_finite : levyProkhorovEDist ν κ ≠ ∞
⊢ (levyProkhorovEDist μ κ).toReal ≤ (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ).toReal

Tactic:
ENNReal.toReal_mono ?_ <| levyProkhorovEDist_triangle μ ν κ

Premises used: MeasureTheory.levyProkhorovEDist_triangle, ENNReal.toReal_mono
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ ν κ : Measure Ω
inst_3 : IsFiniteMeasure μ
inst_4 : IsFiniteMeasure ν
inst_5 : IsFiniteMeasure κ
dμν_finite : levyProkhorovEDist μ ν ≠ ∞
dνκ_finite : levyProkhorovEDist ν κ ≠ ∞
h : levyProkhorovDist μ ν + levyProkhorovDist ν κ = (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ).toReal
convert! : levyProkhorovEDist μ ν + levyProkhorovEDist ν κ ≠ ∞
⊢ levyProkhorovDist μ κ ≤ levyProkhorovDist μ ν + levyProkhorovDist ν κ

Tactic:
convert! ENNReal.toReal_mono ?_ <| levyProkhorovEDist_triangle μ ν κ

Premises used: MeasureTheory.levyProkhorovEDist_triangle, ENNReal.toReal_mono
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ ν κ : Measure Ω
inst_3 : IsFiniteMeasure μ
inst_4 : IsFiniteMeasure ν
inst_5 : IsFiniteMeasure κ
dμν_finite : levyProkhorovEDist μ ν ≠ ∞
dνκ_finite : levyProkhorovEDist ν κ ≠ ∞
⊢ levyProkhorovDist μ ν + levyProkhorovDist ν κ = (levyProkhorovEDist μ ν + levyProkhorovEDist ν κ).toReal

Tactic:
simp only [levyProkhorovDist, ENNReal.toReal_add dμν_finite dνκ_finite]

Premises used: ENNReal.toReal_add, MeasureTheory.levyProkhorovDist
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ ν κ : Measure Ω
inst_3 : IsFiniteMeasure μ
inst_4 : IsFiniteMeasure ν
inst_5 : IsFiniteMeasure κ
dμν_finite : levyProkhorovEDist μ ν ≠ ∞
dνκ_finite : levyProkhorovEDist ν κ ≠ ∞
⊢ levyProkhorovEDist μ ν + levyProkhorovEDist ν κ ≠ ∞

Tactic:
ENNReal.add_ne_top.mpr ⟨dμν_finite, dνκ_finite⟩

Premises used: Iff.mpr, And.intro, ENNReal.add_ne_top
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ ν κ : Measure Ω
inst_3 : IsFiniteMeasure μ
inst_4 : IsFiniteMeasure ν
inst_5 : IsFiniteMeasure κ
dμν_finite : levyProkhorovEDist μ ν ≠ ∞
dνκ_finite : levyProkhorovEDist ν κ ≠ ∞
⊢ levyProkhorovEDist μ ν + levyProkhorovEDist ν κ ≠ ∞

Tactic:
exact ENNReal.add_ne_top.mpr ⟨dμν_finite, dνκ_finite⟩

Premises used: Iff.mpr, And.intro, ENNReal.add_ne_top
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ ν : Measure Ω
hLP : levyProkhorovEDist μ ν = 0
s : Set Ω
s_mble : MeasurableSet s
h_finite : ∃ δ > 0, Ne (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) (thickening δ s) : ℝ≥0∞) (∞ : ℝ≥0∞)
h1 : Tendsto ENNReal.toReal (𝓝[>] 0) (𝓝 0)
h2 : ∀ᶠ (x : ℝ≥0∞) in 𝓝[>] 0, Membership.mem (γ := Set ℝ) (Ioi 0) x.toReal
⊢ Tendsto ENNReal.toReal (𝓝[>] 0) (𝓝[>] 0)

Tactic:
apply tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within (s := Ioi 0) ENNReal.toReal

Premises used: ENNReal.toReal, tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ ν : Measure Ω
hLP : levyProkhorovEDist μ ν = 0
s : Set Ω
s_mble : MeasurableSet s
h_finite : ∃ δ > 0, Ne (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) (thickening δ s) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Tendsto ENNReal.toReal (𝓝[>] 0) (𝓝 0)

Tactic:
tendsto_nhdsWithin_of_tendsto_nhds (continuousAt_toReal zero_ne_top).tendsto

Premises used: ENNReal.zero_ne_top, ENNReal.continuousAt_toReal, tendsto_nhdsWithin_of_tendsto_nhds, ContinuousAt.tendsto
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ ν : Measure Ω
hLP : levyProkhorovEDist μ ν = 0
s : Set Ω
s_mble : MeasurableSet s
h_finite : ∃ δ > 0, Ne (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) (thickening δ s) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Tendsto ENNReal.toReal (𝓝[>] 0) (𝓝 0)

Tactic:
exact tendsto_nhdsWithin_of_tendsto_nhds (continuousAt_toReal zero_ne_top).tendsto

Premises used: ENNReal.zero_ne_top, ENNReal.continuousAt_toReal, tendsto_nhdsWithin_of_tendsto_nhds, ContinuousAt.tendsto
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ ν : Measure Ω
hLP : levyProkhorovEDist μ ν = 0
s : Set Ω
s_mble : MeasurableSet s
h_finite : ∃ δ > 0, Ne (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) (thickening δ s) : ℝ≥0∞) (∞ : ℝ≥0∞)
h : ∀ (x : ℝ≥0∞) (hx : Membership.mem (γ := Set ℝ≥0∞) (Ioo 0 1) x), Membership.mem (γ := Set ℝ) (Ioi 0) x.toReal
⊢ ∀ᶠ (x : ℝ≥0∞) in 𝓝[>] 0, Membership.mem (γ := Set ℝ) (Ioi 0) x.toReal

Tactic:
filter_upwards [Ioo_mem_nhdsGT zero_lt_one] with x hx

Premises used: zero_lt_one, Ioo_mem_nhdsGT
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ ν : Measure Ω
hLP : levyProkhorovEDist μ ν = 0
s : Set Ω
s_mble : MeasurableSet s
h_finite : ∃ δ > 0, Ne (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) (thickening δ s) : ℝ≥0∞) (∞ : ℝ≥0∞)
x : ℝ≥0∞
hx : Membership.mem (γ := Set ℝ≥0∞) (Ioo 0 1) x
⊢ Membership.mem (γ := Set ℝ) (Ioi 0) x.toReal

Tactic:
toReal_pos hx.1.ne' <| ne_top_of_lt hx.2

Premises used: Set.Ioi, Set.Mem, setOf, ENNReal.toReal_pos, LT.lt.ne', And.right, And.left, ne_top_of_lt
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ ν : Measure Ω
hLP : levyProkhorovEDist μ ν = 0
s : Set Ω
s_mble : MeasurableSet s
h_finite : ∃ δ > 0, Ne (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) (thickening δ s) : ℝ≥0∞) (∞ : ℝ≥0∞)
x : ℝ≥0∞
hx : Membership.mem (γ := Set ℝ≥0∞) (Ioo 0 1) x
⊢ Membership.mem (γ := Set ℝ) (Ioi 0) x.toReal

Tactic:
exact toReal_pos hx.1.ne' <| ne_top_of_lt hx.2

Premises used: ENNReal.toReal_pos, LT.lt.ne', And.right, And.left, ne_top_of_lt
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ ν : Measure Ω
hLP : levyProkhorovEDist μ ν = 0
s : Set Ω
s_mble : MeasurableSet s
h_finite : ∃ δ > 0, Ne (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) (thickening δ s) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Tendsto ENNReal.toReal (𝓝[>] 0) (𝓝[>] 0)

Tactic:
have aux : Tendsto ENNReal.toReal (𝓝[>] 0) (𝓝[>] 0) := by
      apply tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within (s := Ioi 0) ENNReal.toReal
      · exact tendsto_nhdsWithin_of_tendsto_nhds (continuousAt_toReal zero_ne_top).tendsto
      · filter_upwards [Ioo_mem_nhdsGT zero_lt_one] with x hx
        exact toReal_pos hx.1.ne' <| ne_top_of_lt hx.2
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ ν : Measure Ω
hLP : levyProkhorovEDist μ ν = 0
s : Set Ω
s_mble : MeasurableSet s
h_finite : ∃ δ > 0, Ne (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) (thickening δ s) : ℝ≥0∞) (∞ : ℝ≥0∞)
aux : Tendsto ENNReal.toReal (𝓝[>] 0) (𝓝[>] 0)
⊢ Tendsto (β := ℝ≥0∞) (fun (ε : ℝ≥0∞) ↦ ((ν : (a : Set Ω) → ℝ≥0∞) (thickening ε.toReal s) : ℝ≥0∞)) (𝓝[>] 0)
    (𝓝 ((ν : (a : Set Ω) → ℝ≥0∞) (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s)) : Filter ℝ≥0∞)

Tactic:
(tendsto_measure_thickening h_finite).comp aux

Premises used: tendsto_measure_thickening, Filter.Tendsto.comp
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ ν : Measure Ω
hLP : levyProkhorovEDist μ ν = 0
s : Set Ω
s_mble : MeasurableSet s
h_finite : ∃ δ > 0, Ne (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) (thickening δ s) : ℝ≥0∞) (∞ : ℝ≥0∞)
aux : Tendsto ENNReal.toReal (𝓝[>] 0) (𝓝[>] 0)
⊢ Tendsto (β := ℝ≥0∞) (fun (ε : ℝ≥0∞) ↦ ((ν : (a : Set Ω) → ℝ≥0∞) (thickening ε.toReal s) : ℝ≥0∞)) (𝓝[>] 0)
    (𝓝 ((ν : (a : Set Ω) → ℝ≥0∞) (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s)) : Filter ℝ≥0∞)

Tactic:
exact (tendsto_measure_thickening h_finite).comp aux

Premises used: tendsto_measure_thickening, Filter.Tendsto.comp
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ ν : Measure Ω
hLP : levyProkhorovEDist μ ν = 0
s : Set Ω
s_mble : MeasurableSet s
h_finite : ∃ δ > 0, Ne (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) (thickening δ s) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Tendsto (β := ℝ≥0∞) (fun (ε : ℝ≥0∞) ↦ ((ν : (a : Set Ω) → ℝ≥0∞) (thickening ε.toReal s) : ℝ≥0∞)) (𝓝[>] 0)
    (𝓝 ((ν : (a : Set Ω) → ℝ≥0∞) (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s)) : Filter ℝ≥0∞)

Tactic:
have key : Tendsto (fun ε ↦ ν (thickening ε.toReal s)) (𝓝[>] (0 : ℝ≥0∞)) (𝓝 (ν (closure s))) := by
    have aux : Tendsto ENNReal.toReal (𝓝[>] 0) (𝓝[>] 0) := by
      apply tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within (s := Ioi 0) ENNReal.toReal
      · exact tendsto_nhdsWithin_of_tendsto_nhds (continuousAt_toReal zero_ne_top).tendsto
      · filter_upwards [Ioo_mem_nhdsGT zero_lt_one] with x hx
        exact toReal_pos hx.1.ne' <| ne_top_of_lt hx.2
    exact (tendsto_measure_thickening h_finite).comp aux
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ ν : Measure Ω
hLP : levyProkhorovEDist μ ν = 0
s : Set Ω
s_mble : MeasurableSet s
h_finite : ∃ δ > 0, Ne (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) (thickening δ s) : ℝ≥0∞) (∞ : ℝ≥0∞)
key :
  Tendsto (β := ℝ≥0∞) (fun (ε : ℝ≥0∞) ↦ ((ν : (a : Set Ω) → ℝ≥0∞) (thickening ε.toReal s) : ℝ≥0∞)) (𝓝[>] 0)
    (𝓝 ((ν : (a : Set Ω) → ℝ≥0∞) (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s)) : Filter ℝ≥0∞)
⊢ Tendsto (fun (x : ℝ≥0∞) ↦ HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) (thickening x.toReal s) : ℝ≥0∞) (id x))
    (𝓝[>] 0)
    (𝓝
      (HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞)
        ((ν : (a : Set Ω) → ℝ≥0∞) (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) : ℝ≥0∞) (0 : ℝ≥0∞)))

Tactic:
have obs := Tendsto.add key (tendsto_nhdsWithin_of_tendsto_nhds tendsto_id)
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ ν : Measure Ω
hLP : levyProkhorovEDist μ ν = 0
s : Set Ω
s_mble : MeasurableSet s
h_finite : ∃ δ > 0, Ne (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) (thickening δ s) : ℝ≥0∞) (∞ : ℝ≥0∞)
key :
  Tendsto (β := ℝ≥0∞) (fun (ε : ℝ≥0∞) ↦ ((ν : (a : Set Ω) → ℝ≥0∞) (thickening ε.toReal s) : ℝ≥0∞)) (𝓝[>] 0)
    (𝓝 ((ν : (a : Set Ω) → ℝ≥0∞) (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s)) : Filter ℝ≥0∞)
obs :
  Tendsto (fun (x : ℝ≥0∞) ↦ HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) (thickening x.toReal s) : ℝ≥0∞) (id x))
    (𝓝[>] 0)
    (𝓝
      (HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞)
        ((ν : (a : Set Ω) → ℝ≥0∞) (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) : ℝ≥0∞) (0 : ℝ≥0∞)))
⊢ Tendsto (β := ℝ≥0∞)
    (fun (x : ℝ≥0∞) ↦ HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) (thickening x.toReal s) : ℝ≥0∞) x) (𝓝[>] 0)
    (𝓝 ((ν : (a : Set Ω) → ℝ≥0∞) (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s)) : Filter ℝ≥0∞)

Tactic:
simp only [id_eq, add_zero] at obs

Premises used: add_zero, id_eq
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ ν : Measure Ω
hLP : levyProkhorovEDist μ ν = 0
s : Set Ω
s_mble : MeasurableSet s
h_finite : ∃ δ > 0, Ne (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) (thickening δ s) : ℝ≥0∞) (∞ : ℝ≥0∞)
key :
  Tendsto (β := ℝ≥0∞) (fun (ε : ℝ≥0∞) ↦ ((ν : (a : Set Ω) → ℝ≥0∞) (thickening ε.toReal s) : ℝ≥0∞)) (𝓝[>] 0)
    (𝓝 ((ν : (a : Set Ω) → ℝ≥0∞) (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s)) : Filter ℝ≥0∞)
obs :
  Tendsto (β := ℝ≥0∞)
    (fun (x : ℝ≥0∞) ↦ HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) (thickening x.toReal s) : ℝ≥0∞) x) (𝓝[>] 0)
    (𝓝 ((ν : (a : Set Ω) → ℝ≥0∞) (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s)) : Filter ℝ≥0∞)
apply :
  ∀ᶠ (c : ℝ≥0∞) in 𝓝[>] 0,
    (μ : (a : Set Ω) → ℝ≥0∞) s ≤ HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) (thickening c.toReal s) : ℝ≥0∞) c
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
    ((ν : (a : Set Ω) → ℝ≥0∞) (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) : ℝ≥0∞)

Tactic:
apply ge_of_tendsto (b := μ s) obs

Premises used: ge_of_tendsto
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ ν : Measure Ω
hLP : levyProkhorovEDist μ ν = 0
s : Set Ω
s_mble : MeasurableSet s
h_finite : ∃ δ > 0, Ne (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) (thickening δ s) : ℝ≥0∞) (∞ : ℝ≥0∞)
key :
  Tendsto (β := ℝ≥0∞) (fun (ε : ℝ≥0∞) ↦ ((ν : (a : Set Ω) → ℝ≥0∞) (thickening ε.toReal s) : ℝ≥0∞)) (𝓝[>] 0)
    (𝓝 ((ν : (a : Set Ω) → ℝ≥0∞) (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s)) : Filter ℝ≥0∞)
obs :
  Tendsto (β := ℝ≥0∞)
    (fun (x : ℝ≥0∞) ↦ HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) (thickening x.toReal s) : ℝ≥0∞) x) (𝓝[>] 0)
    (𝓝 ((ν : (a : Set Ω) → ℝ≥0∞) (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s)) : Filter ℝ≥0∞)
h :
  ∀ (ε : ℝ≥0∞) (ε_pos : Membership.mem (γ := Set ℝ≥0∞) (Ioi 0) ε),
    (μ : (a : Set Ω) → ℝ≥0∞) s ≤ HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) (thickening ε.toReal s) : ℝ≥0∞) ε
⊢ ∀ᶠ (c : ℝ≥0∞) in 𝓝[>] 0,
    (μ : (a : Set Ω) → ℝ≥0∞) s ≤ HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) (thickening c.toReal s) : ℝ≥0∞) c

Tactic:
filter_upwards [self_mem_nhdsWithin] with ε ε_pos

Premises used: self_mem_nhdsWithin
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoEMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ ν : Measure Ω
hLP : levyProkhorovEDist μ ν = 0
s : Set Ω
s_mble : MeasurableSet s
h_finite : ∃ δ > 0, Ne (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) (thickening δ s) : ℝ≥0∞) (∞ : ℝ≥0∞)
key :
  Tendsto (β := ℝ≥0∞) (fun (ε : ℝ≥0∞) ↦ ((ν : (a : Set Ω) → ℝ≥0∞) (thickening ε.toReal s) : ℝ≥0∞)) (𝓝[>] 0)
    (𝓝 ((ν : (a : Set Ω) → ℝ≥0∞) (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s)) : Filter ℝ≥0∞)
obs :
  Tendsto (β := ℝ≥0∞)
    (fun (x : ℝ≥0∞) ↦ HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) (thickening x.toReal s) : ℝ≥0∞) x) (𝓝[>] 0)
    (𝓝 ((ν : (a : Set Ω) → ℝ≥0∞) (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s)) : Filter ℝ≥0∞)
ε : ℝ≥0∞
ε_pos : Membership.mem (γ := Set ℝ≥0∞) (Ioi 0) ε
⊢ (μ : (a : Set Ω) → ℝ≥0∞) s ≤ HAdd.hAdd (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) (thickening ε.toReal s) : ℝ≥0∞) ε

Tactic:
left_measure_le_of_levyProkhorovEDist_lt (B_mble := s_mble) (hLP ▸ ε_pos)

Premises used: MeasureTheory.left_measure_le_of_levyProkhorovEDist_lt