no goals
G : Type u_1
inst✝² : Group G
H : Subgroup G
inst✝¹ : Normal H
inst✝ : Group.IsNilpotent G
⊢ nilpotencyClass G = 0 ↔ Subsingleton G
rw [Group.nilpotencyClass, @Nat.find_eq_zero _ (Classical.decPred _), upperCentralSeries_zero,
  subsingleton_iff_bot_eq_top, Subgroup.subsingleton_iff]