case intro
ι : Sort ?u.123224
α✝ : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α✝
δ : ℝ
s✝ t : Set α✝
x : α✝
α : Type u_1
inst✝ : PseudoMetricSpace α
s : Set α
ε : ℝ≥0
⊢ diam (cthickening (↑ε) s) ≤ diam s + 2 * ↑ε
ι : Sort ?u.123224
α✝ : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α✝
δ ε : ℝ
s✝ t : Set α✝
x : α✝
α : Type u_1
inst✝ : PseudoMetricSpace α
s : Set α
hε : 0 ≤ ε
⊢ diam (cthickening ε s) ≤ diam s + 2 * ε
lift ε to ℝ≥0 using hε
case intro.refine_1
ι : Sort ?u.123224
α✝ : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α✝
δ : ℝ
s✝ t : Set α✝
x : α✝
α : Type u_1
inst✝ : PseudoMetricSpace α
s : Set α
ε : ℝ≥0
⊢ EMetric.diam s = ⊤ → EMetric.diam (cthickening (↑ε) s) = ⊤

case intro.refine_2
ι : Sort ?u.123224
α✝ : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α✝
δ : ℝ
s✝ t : Set α✝
x : α✝
α : Type u_1
inst✝ : PseudoMetricSpace α
s : Set α
ε : ℝ≥0
⊢ 2 * ↑ε = ⊤ → EMetric.diam (cthickening (↑ε) s) = ⊤

case intro.refine_3
ι : Sort ?u.123224
α✝ : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α✝
δ : ℝ
s✝ t : Set α✝
x : α✝
α : Type u_1
inst✝ : PseudoMetricSpace α
s : Set α
ε : ℝ≥0
⊢ ENNReal.toReal (EMetric.diam s) + ENNReal.toReal (2 * ↑ε) = diam s + 2 * ↑ε
case intro
ι : Sort ?u.123224
α✝ : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α✝
δ : ℝ
s✝ t : Set α✝
x : α✝
α : Type u_1
inst✝ : PseudoMetricSpace α
s : Set α
ε : ℝ≥0
⊢ diam (cthickening (↑ε) s) ≤ diam s + 2 * ↑ε
refine (toReal_le_add' (ediam_cthickening_le _) ?_ ?_).trans_eq ?_
no goals
case intro.refine_1
ι : Sort ?u.123224
α✝ : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α✝
δ : ℝ
s✝ t : Set α✝
x : α✝
α : Type u_1
inst✝ : PseudoMetricSpace α
s : Set α
ε : ℝ≥0
⊢ EMetric.diam s = ⊤ → EMetric.diam (cthickening (↑ε) s) = ⊤
exact fun h ↦ top_unique <| h ▸ EMetric.diam_mono (self_subset_cthickening _)
no goals
case intro.refine_2
ι : Sort ?u.123224
α✝ : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α✝
δ : ℝ
s✝ t : Set α✝
x : α✝
α : Type u_1
inst✝ : PseudoMetricSpace α
s : Set α
ε : ℝ≥0
⊢ 2 * ↑ε = ⊤ → EMetric.diam (cthickening (↑ε) s) = ⊤
simp [mul_eq_top]
no goals
case intro.refine_3
ι : Sort ?u.123224
α✝ : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α✝
δ : ℝ
s✝ t : Set α✝
x : α✝
α : Type u_1
inst✝ : PseudoMetricSpace α
s : Set α
ε : ℝ≥0
⊢ ENNReal.toReal (EMetric.diam s) + ENNReal.toReal (2 * ↑ε) = diam s + 2 * ↑ε
simp [diam]