ι : Sort ?u.116888
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ ε✝ : ℝ
s t : Set α
x✝¹ : α
ε : ℝ≥0
x : α
hx : x ∈ cthickening (↑ε) s
y : α
hy : y ∈ cthickening (↑ε) s
δ : ℝ≥0
hδ : 0 < δ
x✝ : EMetric.diam s + 2 * ↑ε < ⊤
⊢ edist x y ≤ EMetric.diam s + 2 * ↑ε + ↑δ
ι : Sort ?u.116888
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ ε✝ : ℝ
s t : Set α
x : α
ε : ℝ≥0
⊢ EMetric.diam (cthickening (↑ε) s) ≤ EMetric.diam s + 2 * ↑ε
refine' diam_le fun x hx y hy => ENNReal.le_of_forall_pos_le_add fun δ hδ _ => _
ι : Sort ?u.116888
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ ε✝ : ℝ
s t : Set α
x✝¹ : α
ε : ℝ≥0
x : α
hx : infEdist x s ≤ ↑ε
y : α
hy : infEdist y s ≤ ↑ε
δ : ℝ≥0
hδ : 0 < δ
x✝ : EMetric.diam s + 2 * ↑ε < ⊤
⊢ edist x y ≤ EMetric.diam s + 2 * ↑ε + ↑δ
ι : Sort ?u.116888
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ ε✝ : ℝ
s t : Set α
x✝¹ : α
ε : ℝ≥0
x : α
hx : x ∈ cthickening (↑ε) s
y : α
hy : y ∈ cthickening (↑ε) s
δ : ℝ≥0
hδ : 0 < δ
x✝ : EMetric.diam s + 2 * ↑ε < ⊤
⊢ edist x y ≤ EMetric.diam s + 2 * ↑ε + ↑δ
rw [mem_cthickening_iff, ENNReal.ofReal_coe_nnreal] at hx hy
ι : Sort ?u.116888
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ ε✝ : ℝ
s t : Set α
x✝¹ : α
ε : ℝ≥0
x : α
hx : infEdist x s ≤ ↑ε
y : α
hy : infEdist y s ≤ ↑ε
δ : ℝ≥0
hδ : 0 < δ
x✝ : EMetric.diam s + 2 * ↑ε < ⊤
hε : ↑ε < ↑ε + ↑δ
⊢ edist x y ≤ EMetric.diam s + 2 * ↑ε + ↑δ
ι : Sort ?u.116888
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ ε✝ : ℝ
s t : Set α
x✝¹ : α
ε : ℝ≥0
x : α
hx : infEdist x s ≤ ↑ε
y : α
hy : infEdist y s ≤ ↑ε
δ : ℝ≥0
hδ : 0 < δ
x✝ : EMetric.diam s + 2 * ↑ε < ⊤
⊢ edist x y ≤ EMetric.diam s + 2 * ↑ε + ↑δ
have hε : (ε : ℝ≥0∞) < ε + δ := ENNReal.coe_lt_coe.2 (lt_add_of_pos_right _ hδ)
ι : Sort ?u.116888
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ ε✝ : ℝ
s t : Set α
x✝¹ : α
ε : ℝ≥0
x y : α
hy : infEdist y s ≤ ↑ε
δ : ℝ≥0
hδ : 0 < δ
x✝ : EMetric.diam s + 2 * ↑ε < ⊤
hε : ↑ε < ↑ε + ↑δ
hx : infEdist x s < ↑ε + ↑δ
⊢ edist x y ≤ EMetric.diam s + 2 * ↑ε + ↑δ
ι : Sort ?u.116888
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ ε✝ : ℝ
s t : Set α
x✝¹ : α
ε : ℝ≥0
x : α
hx : infEdist x s ≤ ↑ε
y : α
hy : infEdist y s ≤ ↑ε
δ : ℝ≥0
hδ : 0 < δ
x✝ : EMetric.diam s + 2 * ↑ε < ⊤
hε : ↑ε < ↑ε + ↑δ
⊢ edist x y ≤ EMetric.diam s + 2 * ↑ε + ↑δ
replace hx := hx.trans_lt hε
case intro.intro
ι : Sort ?u.116888
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ ε✝ : ℝ
s t : Set α
x✝¹ : α
ε : ℝ≥0
x y : α
hy : infEdist y s ≤ ↑ε
δ : ℝ≥0
hδ : 0 < δ
x✝ : EMetric.diam s + 2 * ↑ε < ⊤
hε : ↑ε < ↑ε + ↑δ
hx : infEdist x s < ↑ε + ↑δ
x' : α
hx' : x' ∈ s
hxx' : edist x x' < ↑ε + ↑δ
⊢ edist x y ≤ EMetric.diam s + 2 * ↑ε + ↑δ
ι : Sort ?u.116888
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ ε✝ : ℝ
s t : Set α
x✝¹ : α
ε : ℝ≥0
x y : α
hy : infEdist y s ≤ ↑ε
δ : ℝ≥0
hδ : 0 < δ
x✝ : EMetric.diam s + 2 * ↑ε < ⊤
hε : ↑ε < ↑ε + ↑δ
hx : infEdist x s < ↑ε + ↑δ
⊢ edist x y ≤ EMetric.diam s + 2 * ↑ε + ↑δ
obtain ⟨x', hx', hxx'⟩ := infEdist_lt_iff.mp hx
no goals
case intro.intro
ι : Sort ?u.116888
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ ε✝ : ℝ
s t : Set α
x✝¹ : α
ε : ℝ≥0
x y : α
hy : infEdist y s ≤ ↑ε
δ : ℝ≥0
hδ : 0 < δ
x✝ : EMetric.diam s + 2 * ↑ε < ⊤
hε : ↑ε < ↑ε + ↑δ
hx : infEdist x s < ↑ε + ↑δ
x' : α
hx' : x' ∈ s
hxx' : edist x x' < ↑ε + ↑δ
⊢ edist x y ≤ EMetric.diam s + 2 * ↑ε + ↑δ
calc
  edist x y ≤ edist x x' + edist y x' := edist_triangle_right _ _ _
  _ ≤ ε + δ + (infEdist y s + EMetric.diam s) :=
    add_le_add hxx'.le (edist_le_infEdist_add_ediam hx')
  _ ≤ ε + δ + (ε + EMetric.diam s) := add_le_add_left (add_le_add_right hy _) _
  _ = _ := by rw [two_mul]; ac_rfl
ι : Sort ?u.116888
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ ε✝ : ℝ
s t : Set α
x✝¹ : α
ε : ℝ≥0
x y : α
hy : infEdist y s ≤ ↑ε
δ : ℝ≥0
hδ : 0 < δ
x✝ : EMetric.diam s + 2 * ↑ε < ⊤
hε : ↑ε < ↑ε + ↑δ
hx : infEdist x s < ↑ε + ↑δ
x' : α
hx' : x' ∈ s
hxx' : edist x x' < ↑ε + ↑δ
⊢ ↑ε + ↑δ + (↑ε + EMetric.diam s) = EMetric.diam s + (↑ε + ↑ε) + ↑δ
ι : Sort ?u.116888
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ ε✝ : ℝ
s t : Set α
x✝¹ : α
ε : ℝ≥0
x y : α
hy : infEdist y s ≤ ↑ε
δ : ℝ≥0
hδ : 0 < δ
x✝ : EMetric.diam s + 2 * ↑ε < ⊤
hε : ↑ε < ↑ε + ↑δ
hx : infEdist x s < ↑ε + ↑δ
x' : α
hx' : x' ∈ s
hxx' : edist x x' < ↑ε + ↑δ
⊢ ↑ε + ↑δ + (↑ε + EMetric.diam s) = EMetric.diam s + 2 * ↑ε + ↑δ
rw [two_mul]
no goals
ι : Sort ?u.116888
α : Type u
β : Type v
inst✝ : PseudoEMetricSpace α
δ✝ ε✝ : ℝ
s t : Set α
x✝¹ : α
ε : ℝ≥0
x y : α
hy : infEdist y s ≤ ↑ε
δ : ℝ≥0
hδ : 0 < δ
x✝ : EMetric.diam s + 2 * ↑ε < ⊤
hε : ↑ε < ↑ε + ↑δ
hx : infEdist x s < ↑ε + ↑δ
x' : α
hx' : x' ∈ s
hxx' : edist x x' < ↑ε + ↑δ
⊢ ↑ε + ↑δ + (↑ε + EMetric.diam s) = EMetric.diam s + (↑ε + ↑ε) + ↑δ
ac_rfl