-- Mathlib/Topology/MetricSpace/HausdorffDistance.lean
theorem infEdist_le_infEdist_add_hausdorffEdist :
    infEdist x t ≤ infEdist x s + hausdorffEdist s t :=
  ENNReal.le_of_forall_pos_le_add fun ε εpos h => by
    have ε0 : (ε / 2 : ℝ≥0∞) ≠ 0

Proof state:
case intro.intro.intro.intro
α : Type u
inst✝ : PseudoEMetricSpace α
x : α
s t : Set α
ε : ℝ≥0
εpos : 0 < ε
h : infEdist x s + hausdorffEdist s t < ⊤
ε0 : ↑ε / 2 ≠ 0
this✝ : infEdist x s < infEdist x s + ↑ε / 2
y : α
ys : y ∈ s
dxy : edist x y < infEdist x s + ↑ε / 2
this : hausdorffEdist s t < hausdorffEdist s t + ↑ε / 2
z : α
zt : z ∈ t
dyz : edist y z < hausdorffEdist s t + ↑ε / 2
⊢ infEdist x t ≤ infEdist x s + hausdorffEdist s t + ↑ε

Tactic:
calc
  infEdist x t ≤ edist x z := infEdist_le_edist_of_mem zt
  _ ≤ edist x y + edist y z := edist_triangle _ _ _
  _ ≤ infEdist x s + ε / 2 + (hausdorffEdist s t + ε / 2) := add_le_add dxy.le dyz.le
  _ = infEdist x s + hausdorffEdist s t + ε := by
    simp [ENNReal.add_halves, add_comm, add_left_comm]

Result:
no goals

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
x : α
s t : Set α
ε : ℝ≥0
εpos : 0 < ε
h : infEdist x s + hausdorffEdist s t < ⊤
ε0 : ↑ε / 2 ≠ 0
⊢ infEdist x t ≤ infEdist x s + hausdorffEdist s t + ↑ε

Tactic:
have : infEdist x s < infEdist x s + ε / 2 :=
  ENNReal.lt_add_right (ENNReal.add_lt_top.1 h).1.ne ε0

Result:
α : Type u
inst✝ : PseudoEMetricSpace α
x : α
s t : Set α
ε : ℝ≥0
εpos : 0 < ε
h : infEdist x s + hausdorffEdist s t < ⊤
ε0 : ↑ε / 2 ≠ 0
this : infEdist x s < infEdist x s + ↑ε / 2
⊢ infEdist x t ≤ infEdist x s + hausdorffEdist s t + ↑ε

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
x : α
s t : Set α
ε : ℝ≥0
εpos : 0 < ε
h : infEdist x s + hausdorffEdist s t < ⊤
⊢ ↑ε / 2 ≠ 0

Tactic:
simpa [pos_iff_ne_zero] using εpos

Result:
no goals

Proof state:
case intro.intro
α : Type u
inst✝ : PseudoEMetricSpace α
x : α
s t : Set α
ε : ℝ≥0
εpos : 0 < ε
h : infEdist x s + hausdorffEdist s t < ⊤
ε0 : ↑ε / 2 ≠ 0
this : infEdist x s < infEdist x s + ↑ε / 2
y : α
ys : y ∈ s
dxy : edist x y < infEdist x s + ↑ε / 2
⊢ infEdist x t ≤ infEdist x s + hausdorffEdist s t + ↑ε

Tactic:
have : hausdorffEdist s t < hausdorffEdist s t + ε / 2 :=
  ENNReal.lt_add_right (ENNReal.add_lt_top.1 h).2.ne ε0

Result:
case intro.intro
α : Type u
inst✝ : PseudoEMetricSpace α
x : α
s t : Set α
ε : ℝ≥0
εpos : 0 < ε
h : infEdist x s + hausdorffEdist s t < ⊤
ε0 : ↑ε / 2 ≠ 0
this✝ : infEdist x s < infEdist x s + ↑ε / 2
y : α
ys : y ∈ s
dxy : edist x y < infEdist x s + ↑ε / 2
this : hausdorffEdist s t < hausdorffEdist s t + ↑ε / 2
⊢ infEdist x t ≤ infEdist x s + hausdorffEdist s t + ↑ε

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
x : α
s t : Set α
ε : ℝ≥0
εpos : 0 < ε
h : infEdist x s + hausdorffEdist s t < ⊤
⊢ infEdist x t ≤ infEdist x s + hausdorffEdist s t + ↑ε

Tactic:
have ε0 : (ε / 2 : ℝ≥0∞) ≠ 0 := by simpa [pos_iff_ne_zero] using εpos

Result:
α : Type u
inst✝ : PseudoEMetricSpace α
x : α
s t : Set α
ε : ℝ≥0
εpos : 0 < ε
h : infEdist x s + hausdorffEdist s t < ⊤
ε0 : ↑ε / 2 ≠ 0
⊢ infEdist x t ≤ infEdist x s + hausdorffEdist s t + ↑ε

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
x : α
s t : Set α
ε : ℝ≥0
εpos : 0 < ε
h : infEdist x s + hausdorffEdist s t < ⊤
ε0 : ↑ε / 2 ≠ 0
this✝ : infEdist x s < infEdist x s + ↑ε / 2
y : α
ys : y ∈ s
dxy : edist x y < infEdist x s + ↑ε / 2
this : hausdorffEdist s t < hausdorffEdist s t + ↑ε / 2
z : α
zt : z ∈ t
dyz : edist y z < hausdorffEdist s t + ↑ε / 2
⊢ infEdist x s + ↑ε / 2 + (hausdorffEdist s t + ↑ε / 2) = infEdist x s + hausdorffEdist s t + ↑ε

Tactic:
simp [ENNReal.add_halves, add_comm, add_left_comm]

Result:
no goals

Proof state:
case intro.intro
α : Type u
inst✝ : PseudoEMetricSpace α
x : α
s t : Set α
ε : ℝ≥0
εpos : 0 < ε
h : infEdist x s + hausdorffEdist s t < ⊤
ε0 : ↑ε / 2 ≠ 0
this✝ : infEdist x s < infEdist x s + ↑ε / 2
y : α
ys : y ∈ s
dxy : edist x y < infEdist x s + ↑ε / 2
this : hausdorffEdist s t < hausdorffEdist s t + ↑ε / 2
⊢ infEdist x t ≤ infEdist x s + hausdorffEdist s t + ↑ε

Tactic:
obtain ⟨z : α, zt : z ∈ t, dyz : edist y z < hausdorffEdist s t + ↑ε / 2⟩ :=
  exists_edist_lt_of_hausdorffEdist_lt ys this

Result:
case intro.intro.intro.intro
α : Type u
inst✝ : PseudoEMetricSpace α
x : α
s t : Set α
ε : ℝ≥0
εpos : 0 < ε
h : infEdist x s + hausdorffEdist s t < ⊤
ε0 : ↑ε / 2 ≠ 0
this✝ : infEdist x s < infEdist x s + ↑ε / 2
y : α
ys : y ∈ s
dxy : edist x y < infEdist x s + ↑ε / 2
this : hausdorffEdist s t < hausdorffEdist s t + ↑ε / 2
z : α
zt : z ∈ t
dyz : edist y z < hausdorffEdist s t + ↑ε / 2
⊢ infEdist x t ≤ infEdist x s + hausdorffEdist s t + ↑ε

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
x : α
s t : Set α
ε : ℝ≥0
εpos : 0 < ε
h : infEdist x s + hausdorffEdist s t < ⊤
ε0 : ↑ε / 2 ≠ 0
this : infEdist x s < infEdist x s + ↑ε / 2
⊢ infEdist x t ≤ infEdist x s + hausdorffEdist s t + ↑ε

Tactic:
obtain ⟨y : α, ys : y ∈ s, dxy : edist x y < infEdist x s + ↑ε / 2⟩ := infEdist_lt_iff.mp this

Result:
case intro.intro
α : Type u
inst✝ : PseudoEMetricSpace α
x : α
s t : Set α
ε : ℝ≥0
εpos : 0 < ε
h : infEdist x s + hausdorffEdist s t < ⊤
ε0 : ↑ε / 2 ≠ 0
this : infEdist x s < infEdist x s + ↑ε / 2
y : α
ys : y ∈ s
dxy : edist x y < infEdist x s + ↑ε / 2
⊢ infEdist x t ≤ infEdist x s + hausdorffEdist s t + ↑ε