-- Mathlib/MeasureTheory/Measure/LevyProkhorovMetric.lean
lemma measure_le_measure_closure_of_levyProkhorovEDist_eq_zero {μ ν : Measure Ω}
    (hLP : levyProkhorovEDist μ ν = 0) {s : Set Ω} (s_mble : MeasurableSet s)
    (h_finite : ∃ δ > 0, ν (thickening δ s) ≠ ∞) :
    μ s ≤ ν (closure s)

Proof state:
case h2
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : PseudoEMetricSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ ν : Measure Ω
hLP : levyProkhorovEDist μ ν = 0
s : Set Ω
s_mble : MeasurableSet s
h_finite : ∃ δ > 0, ν (thickening δ s) ≠ ⊤
⊢ ∀ᶠ (x : ℝ≥0∞) in 𝓝[>] 0, x.toReal ∈ Ioi 0

Tactic:
filter_upwards [Ioo_mem_nhdsGT zero_lt_one] with x hx

Result:
case h
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : PseudoEMetricSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ ν : Measure Ω
hLP : levyProkhorovEDist μ ν = 0
s : Set Ω
s_mble : MeasurableSet s
h_finite : ∃ δ > 0, ν (thickening δ s) ≠ ⊤
x : ℝ≥0∞
hx : x ∈ Ioo 0 1
⊢ x.toReal ∈ Ioi 0

Proof state:
case h1
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : PseudoEMetricSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ ν : Measure Ω
hLP : levyProkhorovEDist μ ν = 0
s : Set Ω
s_mble : MeasurableSet s
h_finite : ∃ δ > 0, ν (thickening δ s) ≠ ⊤
⊢ Tendsto ENNReal.toReal (𝓝[>] 0) (𝓝 0)

Tactic:
exact tendsto_nhdsWithin_of_tendsto_nhds (continuousAt_toReal zero_ne_top).tendsto

Result:
no goals

Proof state:
case h
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : PseudoEMetricSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ ν : Measure Ω
hLP : levyProkhorovEDist μ ν = 0
s : Set Ω
s_mble : MeasurableSet s
h_finite : ∃ δ > 0, ν (thickening δ s) ≠ ⊤
x : ℝ≥0∞
hx : x ∈ Ioo 0 1
⊢ x.toReal ∈ Ioi 0

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

Result:
no goals

Proof state:
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : PseudoEMetricSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ ν : Measure Ω
hLP : levyProkhorovEDist μ ν = 0
s : Set Ω
s_mble : MeasurableSet s
h_finite : ∃ δ > 0, ν (thickening δ s) ≠ ⊤
key : Tendsto (fun ε => ν (thickening ε.toReal s)) (𝓝[>] 0) (𝓝 (ν (closure s)))
obs : Tendsto (fun x => ν (thickening x.toReal s) + id x) (𝓝[>] 0) (𝓝 (ν (closure s) + 0))
⊢ μ s ≤ ν (closure s)

Tactic:
simp only [id_eq, add_zero] at obs

Result:
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : PseudoEMetricSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ ν : Measure Ω
hLP : levyProkhorovEDist μ ν = 0
s : Set Ω
s_mble : MeasurableSet s
h_finite : ∃ δ > 0, ν (thickening δ s) ≠ ⊤
key : Tendsto (fun ε => ν (thickening ε.toReal s)) (𝓝[>] 0) (𝓝 (ν (closure s)))
obs : Tendsto (fun x => ν (thickening x.toReal s) + x) (𝓝[>] 0) (𝓝 (ν (closure s)))
⊢ μ s ≤ ν (closure s)

Proof state:
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : PseudoEMetricSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ ν : Measure Ω
hLP : levyProkhorovEDist μ ν = 0
s : Set Ω
s_mble : MeasurableSet s
h_finite : ∃ δ > 0, ν (thickening δ s) ≠ ⊤
key : Tendsto (fun ε => ν (thickening ε.toReal s)) (𝓝[>] 0) (𝓝 (ν (closure s)))
obs : Tendsto (fun x => ν (thickening x.toReal s) + x) (𝓝[>] 0) (𝓝 (ν (closure s)))
⊢ ∀ᶠ (c : ℝ≥0∞) in 𝓝[>] 0, μ s ≤ ν (thickening c.toReal s) + c

Tactic:
filter_upwards [self_mem_nhdsWithin] with ε ε_pos

Result:
case h
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : PseudoEMetricSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ ν : Measure Ω
hLP : levyProkhorovEDist μ ν = 0
s : Set Ω
s_mble : MeasurableSet s
h_finite : ∃ δ > 0, ν (thickening δ s) ≠ ⊤
key : Tendsto (fun ε => ν (thickening ε.toReal s)) (𝓝[>] 0) (𝓝 (ν (closure s)))
obs : Tendsto (fun x => ν (thickening x.toReal s) + x) (𝓝[>] 0) (𝓝 (ν (closure s)))
ε : ℝ≥0∞
ε_pos : ε ∈ Ioi 0
⊢ μ s ≤ ν (thickening ε.toReal s) + ε

Proof state:
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : PseudoEMetricSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ ν : Measure Ω
hLP : levyProkhorovEDist μ ν = 0
s : Set Ω
s_mble : MeasurableSet s
h_finite : ∃ δ > 0, ν (thickening δ s) ≠ ⊤
⊢ Tendsto ENNReal.toReal (𝓝[>] 0) (𝓝[>] 0)

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

Result:
case h1
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : PseudoEMetricSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ ν : Measure Ω
hLP : levyProkhorovEDist μ ν = 0
s : Set Ω
s_mble : MeasurableSet s
h_finite : ∃ δ > 0, ν (thickening δ s) ≠ ⊤
⊢ Tendsto ENNReal.toReal (𝓝[>] 0) (𝓝 0)

case h2
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : PseudoEMetricSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ ν : Measure Ω
hLP : levyProkhorovEDist μ ν = 0
s : Set Ω
s_mble : MeasurableSet s
h_finite : ∃ δ > 0, ν (thickening δ s) ≠ ⊤
⊢ ∀ᶠ (x : ℝ≥0∞) in 𝓝[>] 0, x.toReal ∈ Ioi 0

Proof state:
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : PseudoEMetricSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ ν : Measure Ω
hLP : levyProkhorovEDist μ ν = 0
s : Set Ω
s_mble : MeasurableSet s
h_finite : ∃ δ > 0, ν (thickening δ s) ≠ ⊤
aux : Tendsto ENNReal.toReal (𝓝[>] 0) (𝓝[>] 0)
⊢ Tendsto (fun ε => ν (thickening ε.toReal s)) (𝓝[>] 0) (𝓝 (ν (closure s)))

Tactic:
exact (tendsto_measure_thickening h_finite).comp aux

Result:
no goals

Proof state:
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : PseudoEMetricSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ ν : Measure Ω
hLP : levyProkhorovEDist μ ν = 0
s : Set Ω
s_mble : MeasurableSet s
h_finite : ∃ δ > 0, ν (thickening δ s) ≠ ⊤
key : Tendsto (fun ε => ν (thickening ε.toReal s)) (𝓝[>] 0) (𝓝 (ν (closure s)))
obs : Tendsto (fun x => ν (thickening x.toReal s) + x) (𝓝[>] 0) (𝓝 (ν (closure s)))
⊢ μ s ≤ ν (closure s)

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

Result:
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : PseudoEMetricSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ ν : Measure Ω
hLP : levyProkhorovEDist μ ν = 0
s : Set Ω
s_mble : MeasurableSet s
h_finite : ∃ δ > 0, ν (thickening δ s) ≠ ⊤
key : Tendsto (fun ε => ν (thickening ε.toReal s)) (𝓝[>] 0) (𝓝 (ν (closure s)))
obs : Tendsto (fun x => ν (thickening x.toReal s) + x) (𝓝[>] 0) (𝓝 (ν (closure s)))
⊢ ∀ᶠ (c : ℝ≥0∞) in 𝓝[>] 0, μ s ≤ ν (thickening c.toReal s) + c

Proof state:
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : PseudoEMetricSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ ν : Measure Ω
hLP : levyProkhorovEDist μ ν = 0
s : Set Ω
s_mble : MeasurableSet s
h_finite : ∃ δ > 0, ν (thickening δ s) ≠ ⊤
key : Tendsto (fun ε => ν (thickening ε.toReal s)) (𝓝[>] 0) (𝓝 (ν (closure s)))
⊢ μ s ≤ ν (closure s)

Tactic:
have obs := Tendsto.add key (tendsto_nhdsWithin_of_tendsto_nhds tendsto_id)

Result:
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : PseudoEMetricSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ ν : Measure Ω
hLP : levyProkhorovEDist μ ν = 0
s : Set Ω
s_mble : MeasurableSet s
h_finite : ∃ δ > 0, ν (thickening δ s) ≠ ⊤
key : Tendsto (fun ε => ν (thickening ε.toReal s)) (𝓝[>] 0) (𝓝 (ν (closure s)))
obs : Tendsto (fun x => ν (thickening x.toReal s) + id x) (𝓝[>] 0) (𝓝 (ν (closure s) + 0))
⊢ μ s ≤ ν (closure s)

Proof state:
case h
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : PseudoEMetricSpace Ω
inst✝ : OpensMeasurableSpace Ω
μ ν : Measure Ω
hLP : levyProkhorovEDist μ ν = 0
s : Set Ω
s_mble : MeasurableSet s
h_finite : ∃ δ > 0, ν (thickening δ s) ≠ ⊤
key : Tendsto (fun ε => ν (thickening ε.toReal s)) (𝓝[>] 0) (𝓝 (ν (closure s)))
obs : Tendsto (fun x => ν (thickening x.toReal s) + x) (𝓝[>] 0) (𝓝 (ν (closure s)))
ε : ℝ≥0∞
ε_pos : ε ∈ Ioi 0
⊢ μ s ≤ ν (thickening ε.toReal s) + ε

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

Result:
no goals