-- Mathlib/MeasureTheory/Measure/LevyProkhorovMetric.lean
lemma ProbabilityMeasure.toMeasure_add_pos_gt_mem_nhds (P : ProbabilityMeasure Ω)
    {G : Set Ω} (G_open : IsOpen G) {ε : ℝ≥0∞} (ε_pos : 0 < ε) :
    {Q | P.toMeasure G < Q.toMeasure G + ε} ∈ 𝓝 P

Proof state:
Ω : Type u_1
inst✝² : PseudoMetricSpace Ω
inst✝¹ : MeasurableSpace Ω
inst✝ : OpensMeasurableSpace Ω
P : ProbabilityMeasure Ω
G : Set Ω
G_open : IsOpen G
ε : ℝ≥0∞
ε_pos : 0 < ε
ε_top : ¬ε = ⊤
easy : ε ≤ ↑P G
⊢ ↑P G - ε < liminf (fun Q => ↑Q G) (𝓝 P)

Tactic:
apply lt_of_lt_of_le (ENNReal.sub_lt_self (measure_lt_top _ _).ne _ _)
    <| ProbabilityMeasure.le_liminf_measure_open_of_tendsto tendsto_id G_open

Result:
Ω : Type u_1
inst✝² : PseudoMetricSpace Ω
inst✝¹ : MeasurableSpace Ω
inst✝ : OpensMeasurableSpace Ω
P : ProbabilityMeasure Ω
G : Set Ω
G_open : IsOpen G
ε : ℝ≥0∞
ε_pos : 0 < ε
ε_top : ¬ε = ⊤
easy : ε ≤ ↑P G
⊢ ↑P G ≠ 0

Ω : Type u_1
inst✝² : PseudoMetricSpace Ω
inst✝¹ : MeasurableSpace Ω
inst✝ : OpensMeasurableSpace Ω
P : ProbabilityMeasure Ω
G : Set Ω
G_open : IsOpen G
ε : ℝ≥0∞
ε_pos : 0 < ε
ε_top : ¬ε = ⊤
easy : ε ≤ ↑P G
⊢ ε ≠ 0

Proof state:
case pos
Ω : Type u_1
inst✝² : PseudoMetricSpace Ω
inst✝¹ : MeasurableSpace Ω
inst✝ : OpensMeasurableSpace Ω
P : ProbabilityMeasure Ω
G : Set Ω
G_open : IsOpen G
ε : ℝ≥0∞
ε_pos : 0 < ε
easy : ¬↑P G < ε
ε_top : ε = ⊤
⊢ {Q | ↑P G < ↑Q G + ε} ∈ 𝓝 P

Tactic:
simp [ε_top, measure_lt_top]

Result:
no goals

Proof state:
case neg
Ω : Type u_1
inst✝² : PseudoMetricSpace Ω
inst✝¹ : MeasurableSpace Ω
inst✝ : OpensMeasurableSpace Ω
P : ProbabilityMeasure Ω
G : Set Ω
G_open : IsOpen G
ε : ℝ≥0∞
ε_pos : 0 < ε
ε_top : ¬ε = ⊤
easy : ε ≤ ↑P G
aux : ↑P G - ε < liminf (fun Q => ↑Q G) (𝓝 P)
⊢ {Q | ↑P G < ↑Q G + ε} ∈ 𝓝 P

Tactic:
filter_upwards [gt_mem_sets_of_limsInf_gt (α := ℝ≥0∞) isBounded_ge_of_bot
    (show P.toMeasure G - ε < limsInf ((𝓝 P).map (fun Q ↦ Q.toMeasure G)) from aux)] with Q hQ

Result:
case h
Ω : Type u_1
inst✝² : PseudoMetricSpace Ω
inst✝¹ : MeasurableSpace Ω
inst✝ : OpensMeasurableSpace Ω
P : ProbabilityMeasure Ω
G : Set Ω
G_open : IsOpen G
ε : ℝ≥0∞
ε_pos : 0 < ε
ε_top : ¬ε = ⊤
easy : ε ≤ ↑P G
aux : ↑P G - ε < liminf (fun Q => ↑Q G) (𝓝 P)
Q : ProbabilityMeasure Ω
hQ : Q ∈ (fun Q => ↑Q G) ⁻¹' {x | ↑P G - ε < x}
⊢ ↑P G < ↑Q G + ε

Proof state:
case pos
Ω : Type u_1
inst✝² : PseudoMetricSpace Ω
inst✝¹ : MeasurableSpace Ω
inst✝ : OpensMeasurableSpace Ω
P : ProbabilityMeasure Ω
G : Set Ω
G_open : IsOpen G
ε : ℝ≥0∞
ε_pos : 0 < ε
easy : ↑P G < ε
⊢ {Q | ↑P G < ↑Q G + ε} ∈ 𝓝 P

Tactic:
exact Eventually.of_forall (fun _ ↦ lt_of_lt_of_le easy le_add_self)

Result:
no goals

Proof state:
case h.e'_3
Ω : Type u_1
inst✝² : PseudoMetricSpace Ω
inst✝¹ : MeasurableSpace Ω
inst✝ : OpensMeasurableSpace Ω
P : ProbabilityMeasure Ω
G : Set Ω
G_open : IsOpen G
ε : ℝ≥0∞
ε_pos : 0 < ε
ε_top : ¬ε = ⊤
easy : ε ≤ ↑P G
aux : ↑P G - ε < liminf (fun Q => ↑Q G) (𝓝 P)
Q : ProbabilityMeasure Ω
hQ : ↑P G - ε < ↑Q G
⊢ ↑P G = ↑P G - ε + ε

Tactic:
exact (tsub_add_cancel_of_le easy).symm

Result:
no goals

Proof state:
Ω : Type u_1
inst✝² : PseudoMetricSpace Ω
inst✝¹ : MeasurableSpace Ω
inst✝ : OpensMeasurableSpace Ω
P : ProbabilityMeasure Ω
G : Set Ω
G_open : IsOpen G
ε : ℝ≥0∞
ε_pos : 0 < ε
ε_top : ¬ε = ⊤
easy : ε ≤ ↑P G
⊢ ε ≠ 0

Tactic:
exact ε_pos.ne.symm

Result:
no goals

Proof state:
Ω : Type u_1
inst✝² : PseudoMetricSpace Ω
inst✝¹ : MeasurableSpace Ω
inst✝ : OpensMeasurableSpace Ω
P : ProbabilityMeasure Ω
G : Set Ω
G_open : IsOpen G
ε : ℝ≥0∞
ε_pos : 0 < ε
⊢ {Q | ↑P G < ↑Q G + ε} ∈ 𝓝 P

Tactic:
by_cases easy : P.toMeasure G < ε

Result:
case pos
Ω : Type u_1
inst✝² : PseudoMetricSpace Ω
inst✝¹ : MeasurableSpace Ω
inst✝ : OpensMeasurableSpace Ω
P : ProbabilityMeasure Ω
G : Set Ω
G_open : IsOpen G
ε : ℝ≥0∞
ε_pos : 0 < ε
easy : ↑P G < ε
⊢ {Q | ↑P G < ↑Q G + ε} ∈ 𝓝 P

case neg
Ω : Type u_1
inst✝² : PseudoMetricSpace Ω
inst✝¹ : MeasurableSpace Ω
inst✝ : OpensMeasurableSpace Ω
P : ProbabilityMeasure Ω
G : Set Ω
G_open : IsOpen G
ε : ℝ≥0∞
ε_pos : 0 < ε
easy : ¬↑P G < ε
⊢ {Q | ↑P G < ↑Q G + ε} ∈ 𝓝 P

Proof state:
Ω : Type u_1
inst✝² : PseudoMetricSpace Ω
inst✝¹ : MeasurableSpace Ω
inst✝ : OpensMeasurableSpace Ω
P : ProbabilityMeasure Ω
G : Set Ω
G_open : IsOpen G
ε : ℝ≥0∞
ε_pos : 0 < ε
ε_top : ¬ε = ⊤
easy : ε ≤ ↑P G
⊢ ↑P G ≠ 0

Tactic:
exact (lt_of_lt_of_le ε_pos easy).ne.symm

Result:
no goals

Proof state:
case h
Ω : Type u_1
inst✝² : PseudoMetricSpace Ω
inst✝¹ : MeasurableSpace Ω
inst✝ : OpensMeasurableSpace Ω
P : ProbabilityMeasure Ω
G : Set Ω
G_open : IsOpen G
ε : ℝ≥0∞
ε_pos : 0 < ε
ε_top : ¬ε = ⊤
easy : ε ≤ ↑P G
aux : ↑P G - ε < liminf (fun Q => ↑Q G) (𝓝 P)
Q : ProbabilityMeasure Ω
hQ : ↑P G - ε < ↑Q G
⊢ ↑P G < ↑Q G + ε

Tactic:
convert ENNReal.add_lt_add_right ε_top hQ

Result:
case h.e'_3
Ω : Type u_1
inst✝² : PseudoMetricSpace Ω
inst✝¹ : MeasurableSpace Ω
inst✝ : OpensMeasurableSpace Ω
P : ProbabilityMeasure Ω
G : Set Ω
G_open : IsOpen G
ε : ℝ≥0∞
ε_pos : 0 < ε
ε_top : ¬ε = ⊤
easy : ε ≤ ↑P G
aux : ↑P G - ε < liminf (fun Q => ↑Q G) (𝓝 P)
Q : ProbabilityMeasure Ω
hQ : ↑P G - ε < ↑Q G
⊢ ↑P G = ↑P G - ε + ε

Proof state:
case neg
Ω : Type u_1
inst✝² : PseudoMetricSpace Ω
inst✝¹ : MeasurableSpace Ω
inst✝ : OpensMeasurableSpace Ω
P : ProbabilityMeasure Ω
G : Set Ω
G_open : IsOpen G
ε : ℝ≥0∞
ε_pos : 0 < ε
easy : ¬↑P G < ε
⊢ {Q | ↑P G < ↑Q G + ε} ∈ 𝓝 P

Tactic:
by_cases ε_top : ε = ∞

Result:
case pos
Ω : Type u_1
inst✝² : PseudoMetricSpace Ω
inst✝¹ : MeasurableSpace Ω
inst✝ : OpensMeasurableSpace Ω
P : ProbabilityMeasure Ω
G : Set Ω
G_open : IsOpen G
ε : ℝ≥0∞
ε_pos : 0 < ε
easy : ¬↑P G < ε
ε_top : ε = ⊤
⊢ {Q | ↑P G < ↑Q G + ε} ∈ 𝓝 P

case neg
Ω : Type u_1
inst✝² : PseudoMetricSpace Ω
inst✝¹ : MeasurableSpace Ω
inst✝ : OpensMeasurableSpace Ω
P : ProbabilityMeasure Ω
G : Set Ω
G_open : IsOpen G
ε : ℝ≥0∞
ε_pos : 0 < ε
easy : ¬↑P G < ε
ε_top : ¬ε = ⊤
⊢ {Q | ↑P G < ↑Q G + ε} ∈ 𝓝 P

Proof state:
case neg
Ω : Type u_1
inst✝² : PseudoMetricSpace Ω
inst✝¹ : MeasurableSpace Ω
inst✝ : OpensMeasurableSpace Ω
P : ProbabilityMeasure Ω
G : Set Ω
G_open : IsOpen G
ε : ℝ≥0∞
ε_pos : 0 < ε
easy : ¬↑P G < ε
ε_top : ¬ε = ⊤
⊢ {Q | ↑P G < ↑Q G + ε} ∈ 𝓝 P

Tactic:
simp only [not_lt] at easy

Result:
case neg
Ω : Type u_1
inst✝² : PseudoMetricSpace Ω
inst✝¹ : MeasurableSpace Ω
inst✝ : OpensMeasurableSpace Ω
P : ProbabilityMeasure Ω
G : Set Ω
G_open : IsOpen G
ε : ℝ≥0∞
ε_pos : 0 < ε
ε_top : ¬ε = ⊤
easy : ε ≤ ↑P G
⊢ {Q | ↑P G < ↑Q G + ε} ∈ 𝓝 P

Proof state:
case h
Ω : Type u_1
inst✝² : PseudoMetricSpace Ω
inst✝¹ : MeasurableSpace Ω
inst✝ : OpensMeasurableSpace Ω
P : ProbabilityMeasure Ω
G : Set Ω
G_open : IsOpen G
ε : ℝ≥0∞
ε_pos : 0 < ε
ε_top : ¬ε = ⊤
easy : ε ≤ ↑P G
aux : ↑P G - ε < liminf (fun Q => ↑Q G) (𝓝 P)
Q : ProbabilityMeasure Ω
hQ : Q ∈ (fun Q => ↑Q G) ⁻¹' {x | ↑P G - ε < x}
⊢ ↑P G < ↑Q G + ε

Tactic:
simp only [preimage_setOf_eq, mem_setOf_eq] at hQ

Result:
case h
Ω : Type u_1
inst✝² : PseudoMetricSpace Ω
inst✝¹ : MeasurableSpace Ω
inst✝ : OpensMeasurableSpace Ω
P : ProbabilityMeasure Ω
G : Set Ω
G_open : IsOpen G
ε : ℝ≥0∞
ε_pos : 0 < ε
ε_top : ¬ε = ⊤
easy : ε ≤ ↑P G
aux : ↑P G - ε < liminf (fun Q => ↑Q G) (𝓝 P)
Q : ProbabilityMeasure Ω
hQ : ↑P G - ε < ↑Q G
⊢ ↑P G < ↑Q G + ε