case intro.intro
α : Type u
β : Type v
X : Type ?u.537111
ι : Type ?u.537114
inst✝ : PseudoMetricSpace α
s : Set α
x✝ y z : α
t : Set α
x : α
xs : x ∈ s
xt : x ∈ t
⊢ diam (s ∪ t) ≤ diam s + diam t
α : Type u
β : Type v
X : Type ?u.537111
ι : Type ?u.537114
inst✝ : PseudoMetricSpace α
s : Set α
x y z : α
t : Set α
h : Set.Nonempty (s ∩ t)
⊢ diam (s ∪ t) ≤ diam s + diam t
rcases h with ⟨x, ⟨xs, xt⟩⟩
no goals
case intro.intro
α : Type u
β : Type v
X : Type ?u.537111
ι : Type ?u.537114
inst✝ : PseudoMetricSpace α
s : Set α
x✝ y z : α
t : Set α
x : α
xs : x ∈ s
xt : x ∈ t
⊢ diam (s ∪ t) ≤ diam s + diam t
simpa using diam_union xs xt