G : Type u_1
inst✝² : Group G
H : Subgroup G
inst✝¹ : Normal H
hH : Group.IsNilpotent G
inst✝ : Nontrivial G
⊢ nilpotencyClass G = nilpotencyClass G - 1 + 1
G : Type u_1
inst✝² : Group G
H : Subgroup G
inst✝¹ : Normal H
hH : Group.IsNilpotent G
inst✝ : Nontrivial G
⊢ nilpotencyClass G = nilpotencyClass (G ⧸ center G) + 1
rw [nilpotencyClass_quotient_center]
case zero
G : Type u_1
inst✝² : Group G
H : Subgroup G
inst✝¹ : Normal H
hH : Group.IsNilpotent G
inst✝ : Nontrivial G
h : nilpotencyClass G = Nat.zero
⊢ Nat.zero = Nat.zero - 1 + 1

case succ
G : Type u_1
inst✝² : Group G
H : Subgroup G
inst✝¹ : Normal H
hH : Group.IsNilpotent G
inst✝ : Nontrivial G
n✝ : ℕ
h : nilpotencyClass G = Nat.succ n✝
⊢ Nat.succ n✝ = Nat.succ n✝ - 1 + 1
G : Type u_1
inst✝² : Group G
H : Subgroup G
inst✝¹ : Normal H
hH : Group.IsNilpotent G
inst✝ : Nontrivial G
⊢ nilpotencyClass G = nilpotencyClass G - 1 + 1
rcases h : Group.nilpotencyClass G with ⟨⟩
case zero.h
G : Type u_1
inst✝² : Group G
H : Subgroup G
inst✝¹ : Normal H
hH : Group.IsNilpotent G
inst✝ : Nontrivial G
h : nilpotencyClass G = Nat.zero
⊢ False
case zero
G : Type u_1
inst✝² : Group G
H : Subgroup G
inst✝¹ : Normal H
hH : Group.IsNilpotent G
inst✝ : Nontrivial G
h : nilpotencyClass G = Nat.zero
⊢ Nat.zero = Nat.zero - 1 + 1
exfalso
case zero.h
G : Type u_1
inst✝² : Group G
H : Subgroup G
inst✝¹ : Normal H
hH : Group.IsNilpotent G
inst✝ : Nontrivial G
h : Subsingleton G
⊢ False
case zero.h
G : Type u_1
inst✝² : Group G
H : Subgroup G
inst✝¹ : Normal H
hH : Group.IsNilpotent G
inst✝ : Nontrivial G
h : nilpotencyClass G = Nat.zero
⊢ False
rw [nilpotencyClass_zero_iff_subsingleton] at h
case zero.h
G : Type u_1
inst✝² : Group G
H : Subgroup G
inst✝¹ : Normal H
hH : Group.IsNilpotent G
inst✝ : Nontrivial G
h : Subsingleton G
⊢ False
case zero.h
G : Type u_1
inst✝² : Group G
H : Subgroup G
inst✝¹ : Normal H
hH : Group.IsNilpotent G
inst✝ : Nontrivial G
h : Subsingleton G
⊢ False
skip
no goals
case zero.h
G : Type u_1
inst✝² : Group G
H : Subgroup G
inst✝¹ : Normal H
hH : Group.IsNilpotent G
inst✝ : Nontrivial G
h : Subsingleton G
⊢ False
apply false_of_nontrivial_of_subsingleton G
no goals
case succ
G : Type u_1
inst✝² : Group G
H : Subgroup G
inst✝¹ : Normal H
hH : Group.IsNilpotent G
inst✝ : Nontrivial G
n✝ : ℕ
h : nilpotencyClass G = Nat.succ n✝
⊢ Nat.succ n✝ = Nat.succ n✝ - 1 + 1
simp