no goals
α : Type u
β : Type v
X : Type ?u.314784
inst✝¹ : PseudoEMetricSpace α
γ : Type w
inst✝ : EMetricSpace γ
s : Set γ
⊢ 0 < diam s ↔ ∃ x, x ∈ s ∧ ∃ y, y ∈ s ∧ x ≠ y
simp only [diam_pos_iff, Set.Nontrivial, exists_prop]