no goals
α : Type u
β : Type v
X : Type ?u.293762
inst✝ : PseudoEMetricSpace α
x y z : α
ε ε₁ ε₂ : ℝ≥0∞
s t : Set α
d : ℝ≥0∞
⊢ diam (insert x s) ≤ d ↔ max (⨆ (y : α) (_ : y ∈ s), edist x y) (diam s) ≤ d
simp only [diam_le_iff, ball_insert_iff, edist_self, edist_comm x, max_le_iff, iSup_le_iff,
  zero_le, true_and_iff, forall_and, and_self_iff, ← and_assoc]