α : Type u
β : Type v
X : Type ?u.535752
ι : Type ?u.535755
inst✝ : PseudoMetricSpace α
s : Set α
x y z : α
t : Set α
xs : x ∈ s
yt : y ∈ t
⊢ ENNReal.toReal (EMetric.diam (s ∪ t)) ≤
    ENNReal.toReal (EMetric.diam s) + ENNReal.toReal (edist x y) + ENNReal.toReal (EMetric.diam t)
α : Type u
β : Type v
X : Type ?u.535752
ι : Type ?u.535755
inst✝ : PseudoMetricSpace α
s : Set α
x y z : α
t : Set α
xs : x ∈ s
yt : y ∈ t
⊢ diam (s ∪ t) ≤ diam s + dist x y + diam t
simp only [diam, dist_edist]
case refine_1
α : Type u
β : Type v
X : Type ?u.535752
ι : Type ?u.535755
inst✝ : PseudoMetricSpace α
s : Set α
x y z : α
t : Set α
xs : x ∈ s
yt : y ∈ t
⊢ EMetric.diam s + edist x y = ⊤ → EMetric.diam (s ∪ t) = ⊤

case refine_2
α : Type u
β : Type v
X : Type ?u.535752
ι : Type ?u.535755
inst✝ : PseudoMetricSpace α
s : Set α
x y z : α
t : Set α
xs : x ∈ s
yt : y ∈ t
⊢ EMetric.diam t = ⊤ → EMetric.diam (s ∪ t) = ⊤
α : Type u
β : Type v
X : Type ?u.535752
ι : Type ?u.535755
inst✝ : PseudoMetricSpace α
s : Set α
x y z : α
t : Set α
xs : x ∈ s
yt : y ∈ t
⊢ ENNReal.toReal (EMetric.diam (s ∪ t)) ≤
    ENNReal.toReal (EMetric.diam s) + ENNReal.toReal (edist x y) + ENNReal.toReal (EMetric.diam t)
refine (ENNReal.toReal_le_add' (EMetric.diam_union xs yt) ?_ ?_).trans
  (add_le_add_right ENNReal.toReal_add_le _)
case refine_1
α : Type u
β : Type v
X : Type ?u.535752
ι : Type ?u.535755
inst✝ : PseudoMetricSpace α
s : Set α
x y z : α
t : Set α
xs : x ∈ s
yt : y ∈ t
⊢ EMetric.diam s = ⊤ → EMetric.diam (s ∪ t) = ⊤
case refine_1
α : Type u
β : Type v
X : Type ?u.535752
ι : Type ?u.535755
inst✝ : PseudoMetricSpace α
s : Set α
x y z : α
t : Set α
xs : x ∈ s
yt : y ∈ t
⊢ EMetric.diam s + edist x y = ⊤ → EMetric.diam (s ∪ t) = ⊤
simp only [ENNReal.add_eq_top, edist_ne_top, or_false]
no goals
case refine_1
α : Type u
β : Type v
X : Type ?u.535752
ι : Type ?u.535755
inst✝ : PseudoMetricSpace α
s : Set α
x y z : α
t : Set α
xs : x ∈ s
yt : y ∈ t
⊢ EMetric.diam s = ⊤ → EMetric.diam (s ∪ t) = ⊤
exact fun h ↦ top_unique <| h ▸ EMetric.diam_mono (subset_union_left _ _)
no goals
case refine_2
α : Type u
β : Type v
X : Type ?u.535752
ι : Type ?u.535755
inst✝ : PseudoMetricSpace α
s : Set α
x y z : α
t : Set α
xs : x ∈ s
yt : y ∈ t
⊢ EMetric.diam t = ⊤ → EMetric.diam (s ∪ t) = ⊤
exact fun h ↦ top_unique <| h ▸ EMetric.diam_mono (subset_union_right _ _)