case inl
ι : Sort ?u.155566
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ ε✝ : ℝ
s✝ t : Set α
x : α
ε : ℝ
hδ : 0 ≤ δ
s : Set α
hε : ε ≤ 0
⊢ thickening ε (cthickening δ s) ⊆ thickening (ε + δ) s

case inr
ι : Sort ?u.155566
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ ε✝ : ℝ
s✝ t : Set α
x : α
ε : ℝ
hδ : 0 ≤ δ
s : Set α
hε : 0 ≤ ε
⊢ thickening ε (cthickening δ s) ⊆ thickening (ε + δ) s
ι : Sort ?u.155566
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ ε✝ : ℝ
s✝ t : Set α
x : α
ε : ℝ
hδ : 0 ≤ δ
s : Set α
⊢ thickening ε (cthickening δ s) ⊆ thickening (ε + δ) s
obtain hε | hε := le_total ε 0
case inr
ι : Sort ?u.155566
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ ε✝ : ℝ
s✝ t : Set α
x✝ : α
ε : ℝ
hδ : 0 ≤ δ
s : Set α
hε : 0 ≤ ε
x : α
⊢ x ∈ thickening ε (cthickening δ s) → x ∈ thickening (ε + δ) s
case inr
ι : Sort ?u.155566
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ ε✝ : ℝ
s✝ t : Set α
x : α
ε : ℝ
hδ : 0 ≤ δ
s : Set α
hε : 0 ≤ ε
⊢ thickening ε (cthickening δ s) ⊆ thickening (ε + δ) s
intro x
case inr
ι : Sort ?u.155566
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ ε✝ : ℝ
s✝ t : Set α
x✝ : α
ε : ℝ
hδ : 0 ≤ δ
s : Set α
hε : 0 ≤ ε
x : α
⊢ (∃ z, infEdist z s ≤ ENNReal.ofReal δ ∧ edist x z < ENNReal.ofReal ε) →
    infEdist x s < ENNReal.ofReal ε + ENNReal.ofReal δ
case inr
ι : Sort ?u.155566
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ ε✝ : ℝ
s✝ t : Set α
x✝ : α
ε : ℝ
hδ : 0 ≤ δ
s : Set α
hε : 0 ≤ ε
x : α
⊢ x ∈ thickening ε (cthickening δ s) → x ∈ thickening (ε + δ) s
simp_rw [mem_thickening_iff_exists_edist_lt, mem_cthickening_iff, ← infEdist_lt_iff,
  ENNReal.ofReal_add hε hδ]
case inr.intro.intro
ι : Sort ?u.155566
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ ε✝ : ℝ
s✝ t : Set α
x✝ : α
ε : ℝ
hδ : 0 ≤ δ
s : Set α
hε : 0 ≤ ε
x y : α
hy : infEdist y s ≤ ENNReal.ofReal δ
hxy : edist x y < ENNReal.ofReal ε
⊢ infEdist x s < ENNReal.ofReal ε + ENNReal.ofReal δ
case inr
ι : Sort ?u.155566
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ ε✝ : ℝ
s✝ t : Set α
x✝ : α
ε : ℝ
hδ : 0 ≤ δ
s : Set α
hε : 0 ≤ ε
x : α
⊢ (∃ z, infEdist z s ≤ ENNReal.ofReal δ ∧ edist x z < ENNReal.ofReal ε) →
    infEdist x s < ENNReal.ofReal ε + ENNReal.ofReal δ
rintro ⟨y, hy, hxy⟩
no goals
case inr.intro.intro
ι : Sort ?u.155566
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ ε✝ : ℝ
s✝ t : Set α
x✝ : α
ε : ℝ
hδ : 0 ≤ δ
s : Set α
hε : 0 ≤ ε
x y : α
hy : infEdist y s ≤ ENNReal.ofReal δ
hxy : edist x y < ENNReal.ofReal ε
⊢ infEdist x s < ENNReal.ofReal ε + ENNReal.ofReal δ
exact infEdist_le_edist_add_infEdist.trans_lt
  (ENNReal.add_lt_add_of_lt_of_le (hy.trans_lt ENNReal.ofReal_lt_top).ne hxy hy)
no goals
case inl
ι : Sort ?u.155566
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ ε✝ : ℝ
s✝ t : Set α
x : α
ε : ℝ
hδ : 0 ≤ δ
s : Set α
hε : ε ≤ 0
⊢ thickening ε (cthickening δ s) ⊆ thickening (ε + δ) s
simp only [thickening_of_nonpos hε, empty_subset]