case pos
ι : Sort ?u.126772
α✝ : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α✝
δ ε : ℝ
s✝ t : Set α✝
x : α✝
α : Type u_1
inst✝ : PseudoMetricSpace α
s : Set α
hε : 0 ≤ ε
hs : Bounded s
⊢ diam (thickening ε s) ≤ diam s + 2 * ε

case neg
ι : Sort ?u.126772
α✝ : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α✝
δ ε : ℝ
s✝ t : Set α✝
x : α✝
α : Type u_1
inst✝ : PseudoMetricSpace α
s : Set α
hε : 0 ≤ ε
hs : ¬Bounded s
⊢ diam (thickening ε s) ≤ diam s + 2 * ε
ι : Sort ?u.126772
α✝ : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α✝
δ ε : ℝ
s✝ t : Set α✝
x : α✝
α : Type u_1
inst✝ : PseudoMetricSpace α
s : Set α
hε : 0 ≤ ε
⊢ diam (thickening ε s) ≤ diam s + 2 * ε
by_cases hs : Bounded s
case neg.inl
ι : Sort ?u.126772
α✝ : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α✝
δ : ℝ
s✝ t : Set α✝
x : α✝
α : Type u_1
inst✝ : PseudoMetricSpace α
s : Set α
hs : ¬Bounded s
hε : 0 ≤ 0
⊢ diam (thickening 0 s) ≤ diam s + 2 * 0

case neg.inr
ι : Sort ?u.126772
α✝ : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α✝
δ ε : ℝ
s✝ t : Set α✝
x : α✝
α : Type u_1
inst✝ : PseudoMetricSpace α
s : Set α
hε✝ : 0 ≤ ε
hs : ¬Bounded s
hε : 0 < ε
⊢ diam (thickening ε s) ≤ diam s + 2 * ε
case neg
ι : Sort ?u.126772
α✝ : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α✝
δ ε : ℝ
s✝ t : Set α✝
x : α✝
α : Type u_1
inst✝ : PseudoMetricSpace α
s : Set α
hε : 0 ≤ ε
hs : ¬Bounded s
⊢ diam (thickening ε s) ≤ diam s + 2 * ε
obtain rfl | hε := hε.eq_or_lt
no goals
case pos
ι : Sort ?u.126772
α✝ : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α✝
δ ε : ℝ
s✝ t : Set α✝
x : α✝
α : Type u_1
inst✝ : PseudoMetricSpace α
s : Set α
hε : 0 ≤ ε
hs : Bounded s
⊢ diam (thickening ε s) ≤ diam s + 2 * ε
exact (diam_mono (thickening_subset_cthickening _ _) hs.cthickening).trans
  (diam_cthickening_le _ hε)
no goals
case neg.inl
ι : Sort ?u.126772
α✝ : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α✝
δ : ℝ
s✝ t : Set α✝
x : α✝
α : Type u_1
inst✝ : PseudoMetricSpace α
s : Set α
hs : ¬Bounded s
hε : 0 ≤ 0
⊢ diam (thickening 0 s) ≤ diam s + 2 * 0
simp [thickening_of_nonpos, diam_nonneg]
case neg.inr
ι : Sort ?u.126772
α✝ : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α✝
δ ε : ℝ
s✝ t : Set α✝
x : α✝
α : Type u_1
inst✝ : PseudoMetricSpace α
s : Set α
hε✝ : 0 ≤ ε
hs : ¬Bounded s
hε : 0 < ε
⊢ 0 ≤ diam s + 2 * ε
case neg.inr
ι : Sort ?u.126772
α✝ : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α✝
δ ε : ℝ
s✝ t : Set α✝
x : α✝
α : Type u_1
inst✝ : PseudoMetricSpace α
s : Set α
hε✝ : 0 ≤ ε
hs : ¬Bounded s
hε : 0 < ε
⊢ diam (thickening ε s) ≤ diam s + 2 * ε
rw [diam_eq_zero_of_unbounded (mt (Bounded.mono <| self_subset_thickening hε _) hs)]
no goals
case neg.inr
ι : Sort ?u.126772
α✝ : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α✝
δ ε : ℝ
s✝ t : Set α✝
x : α✝
α : Type u_1
inst✝ : PseudoMetricSpace α
s : Set α
hε✝ : 0 ≤ ε
hs : ¬Bounded s
hε : 0 < ε
⊢ 0 ≤ diam s + 2 * ε
positivity