α : Type u
β : Type v
X : Type ?u.302983
inst✝ : PseudoEMetricSpace α
x✝ y z : α
ε ε₁ ε₂ : ℝ≥0∞
s t✝ t : Set α
h : Set.Nonempty (s ∩ t)
x : α
xs : x ∈ s
xt : x ∈ t
⊢ diam (s ∪ t) ≤ diam s + diam t
α : Type u
β : Type v
X : Type ?u.302983
inst✝ : PseudoEMetricSpace α
x y z : α
ε ε₁ ε₂ : ℝ≥0∞
s t✝ t : Set α
h : Set.Nonempty (s ∩ t)
⊢ diam (s ∪ t) ≤ diam s + diam t
let ⟨x, ⟨xs, xt⟩⟩ := h
no goals
α : Type u
β : Type v
X : Type ?u.302983
inst✝ : PseudoEMetricSpace α
x✝ y z : α
ε ε₁ ε₂ : ℝ≥0∞
s t✝ t : Set α
h : Set.Nonempty (s ∩ t)
x : α
xs : x ∈ s
xt : x ∈ t
⊢ diam (s ∪ t) ≤ diam s + diam t
simpa using diam_union xs xt