G✝ : Type ?u.323424
inst✝² : Group G✝
H : Subgroup G✝
inst✝¹ : Normal H
G : Type u_1
inst✝ : CommGroup G
⊢ upperCentralSeries G 1 = ⊤
G✝ : Type ?u.323424
inst✝² : Group G✝
H : Subgroup G✝
inst✝¹ : Normal H
G : Type u_1
inst✝ : CommGroup G
⊢ nilpotencyClass G ≤ 1
apply upperCentralSeries_eq_top_iff_nilpotencyClass_le.mp
G✝ : Type ?u.323424
inst✝² : Group G✝
H : Subgroup G✝
inst✝¹ : Normal H
G : Type u_1
inst✝ : CommGroup G
⊢ center G = ⊤
G✝ : Type ?u.323424
inst✝² : Group G✝
H : Subgroup G✝
inst✝¹ : Normal H
G : Type u_1
inst✝ : CommGroup G
⊢ upperCentralSeries G 1 = ⊤
rw [upperCentralSeries_one]
no goals
G✝ : Type ?u.323424
inst✝² : Group G✝
H : Subgroup G✝
inst✝¹ : Normal H
G : Type u_1
inst✝ : CommGroup G
⊢ center G = ⊤
apply CommGroup.center_eq_top