ι : Sort ?u.150279
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ ε : ℝ
s t : Set α
x : α
r : ℝ≥0∞
h : infEdist x (cthickening δ s) + ENNReal.ofReal δ < r
⊢ infEdist x s < r
ι : Sort ?u.150279
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ ε : ℝ
s t : Set α
x : α
⊢ infEdist x s ≤ infEdist x (cthickening δ s) + ENNReal.ofReal δ
refine' le_of_forall_lt' fun r h => _
ι : Sort ?u.150279
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ ε : ℝ
s t : Set α
x : α
r : ℝ≥0∞
h : ∃ y, infEdist y s ≤ ENNReal.ofReal δ ∧ edist x y < r - ENNReal.ofReal δ
⊢ infEdist x s < r
ι : Sort ?u.150279
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ ε : ℝ
s t : Set α
x : α
r : ℝ≥0∞
h : infEdist x (cthickening δ s) + ENNReal.ofReal δ < r
⊢ infEdist x s < r
simp_rw [← lt_tsub_iff_right, infEdist_lt_iff, mem_cthickening_iff] at h
case intro.intro
ι : Sort ?u.150279
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ ε : ℝ
s t : Set α
x : α
r : ℝ≥0∞
y : α
hy : infEdist y s ≤ ENNReal.ofReal δ
hxy : edist x y < r - ENNReal.ofReal δ
⊢ infEdist x s < r
ι : Sort ?u.150279
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ ε : ℝ
s t : Set α
x : α
r : ℝ≥0∞
h : ∃ y, infEdist y s ≤ ENNReal.ofReal δ ∧ edist x y < r - ENNReal.ofReal δ
⊢ infEdist x s < r
obtain ⟨y, hy, hxy⟩ := h
no goals
case intro.intro
ι : Sort ?u.150279
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ ε : ℝ
s t : Set α
x : α
r : ℝ≥0∞
y : α
hy : infEdist y s ≤ ENNReal.ofReal δ
hxy : edist x y < r - ENNReal.ofReal δ
⊢ infEdist x s < r
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).trans_eq
    (tsub_add_cancel_of_le <| le_self_add.trans (lt_tsub_iff_left.1 hxy).le))