no goals
α : Type u_1
β : Type ?u.9191
inst✝¹ : LT α
inst✝ : LT β
s t : Set α
l : List α
a : α
⊢ chainHeight s = 0 ↔ s = ∅
rw [← not_iff_not, ← Ne.def, ← ENat.one_le_iff_ne_zero, one_le_chainHeight_iff,
  nonempty_iff_ne_empty]