G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
hG : Group.IsNilpotent G
⊢ lowerCentralSeries G (Nat.find (_ : ∃ n, lowerCentralSeries G n = ⊥)) = ⊥
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
hG : Group.IsNilpotent G
⊢ lowerCentralSeries G (nilpotencyClass G) = ⊥
rw [← lowerCentralSeries_length_eq_nilpotencyClass]
no goals
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
hG : Group.IsNilpotent G
⊢ lowerCentralSeries G (Nat.find (_ : ∃ n, lowerCentralSeries G n = ⊥)) = ⊥
exact Nat.find_spec (nilpotent_iff_lowerCentralSeries.mp hG)