-- Mathlib/GroupTheory/Nilpotent.lean
theorem nilpotencyClass_quotient_center [hH : IsNilpotent G] :
    Group.nilpotencyClass (G ⧸ center G) = Group.nilpotencyClass G - 1

Proof state:
case zero
G : Type u_1
inst✝ : Group G
hH : IsNilpotent G
hn : nilpotencyClass G = 0
⊢ nilpotencyClass (G ⧸ center G) = 0 - 1

Tactic:
simp [nilpotencyClass_zero_iff_subsingleton] at *

Result:
case zero
G : Type u_1
inst✝ : Group G
hH : IsNilpotent G
hn : Subsingleton G
⊢ Subsingleton (G ⧸ center G)

Proof state:
case succ
G : Type u_1
inst✝ : Group G
hH : IsNilpotent G
n : ℕ
hn : nilpotencyClass G = n + 1
⊢ nilpotencyClass (G ⧸ center G) = n + 1 - 1

Tactic:
suffices Group.nilpotencyClass (G ⧸ center G) = n by simpa

Result:
case succ
G : Type u_1
inst✝ : Group G
hH : IsNilpotent G
n : ℕ
hn : nilpotencyClass G = n + 1
⊢ nilpotencyClass (G ⧸ center G) = n

Proof state:
G : Type u_1
inst✝ : Group G
hH : IsNilpotent G
⊢ nilpotencyClass (G ⧸ center G) = nilpotencyClass G - 1

Tactic:
generalize hn : Group.nilpotencyClass G = n

Result:
G : Type u_1
inst✝ : Group G
hH : IsNilpotent G
n : ℕ
hn : nilpotencyClass G = n
⊢ nilpotencyClass (G ⧸ center G) = n - 1

Proof state:
case zero
G : Type u_1
inst✝ : Group G
hH : IsNilpotent G
hn : Subsingleton G
⊢ Subsingleton (G ⧸ center G)

Tactic:
exact Quotient.instSubsingletonQuotient (leftRel (center G))

Result:
no goals

Proof state:
case succ
G : Type u_1
inst✝ : Group G
hH : IsNilpotent G
n : ℕ
hn : nilpotencyClass G = n + 1
⊢ nilpotencyClass (G ⧸ center G) = n

Tactic:
apply le_antisymm

Result:
case succ.a
G : Type u_1
inst✝ : Group G
hH : IsNilpotent G
n : ℕ
hn : nilpotencyClass G = n + 1
⊢ nilpotencyClass (G ⧸ center G) ≤ n

case succ.a
G : Type u_1
inst✝ : Group G
hH : IsNilpotent G
n : ℕ
hn : nilpotencyClass G = n + 1
⊢ n ≤ nilpotencyClass (G ⧸ center G)

Proof state:
case succ.a.a
G : Type u_1
inst✝ : Group G
hH : IsNilpotent G
n : ℕ
hn : nilpotencyClass G = n + 1
⊢ comap (mk' (center G)) (upperCentralSeries (G ⧸ center G) n) = comap (mk' (center G)) ⊤

Tactic:
rw [comap_upperCentralSeries_quotient_center, comap_top, Nat.succ_eq_add_one, ← hn]

Result:
case succ.a.a
G : Type u_1
inst✝ : Group G
hH : IsNilpotent G
n : ℕ
hn : nilpotencyClass G = n + 1
⊢ upperCentralSeries G (nilpotencyClass G) = ⊤

Proof state:
case succ.a.bc
G : Type u_1
inst✝ : Group G
hH : IsNilpotent G
n : ℕ
hn : nilpotencyClass G = n + 1
⊢ n + ?succ.a.a ≤ nilpotencyClass (G ⧸ center G) + ?succ.a.a

case succ.a.a
G : Type u_1
inst✝ : Group G
hH : IsNilpotent G
n : ℕ
hn : nilpotencyClass G = n + 1
⊢ ℕ

Tactic:
calc
  n + 1 = Group.nilpotencyClass G := hn.symm
  _ ≤ Group.nilpotencyClass (G ⧸ center G) + 1 :=
    nilpotencyClass_le_of_ker_le_center _ (le_of_eq (ker_mk' _)) _

Result:
no goals

Proof state:
case succ.a
G : Type u_1
inst✝ : Group G
hH : IsNilpotent G
n : ℕ
hn : nilpotencyClass G = n + 1
⊢ nilpotencyClass (G ⧸ center G) ≤ n

Tactic:
apply upperCentralSeries_eq_top_iff_nilpotencyClass_le.mp

Result:
case succ.a
G : Type u_1
inst✝ : Group G
hH : IsNilpotent G
n : ℕ
hn : nilpotencyClass G = n + 1
⊢ upperCentralSeries (G ⧸ center G) n = ⊤

Proof state:
case succ.a.a
G : Type u_1
inst✝ : Group G
hH : IsNilpotent G
n : ℕ
hn : nilpotencyClass G = n + 1
⊢ upperCentralSeries G (nilpotencyClass G) = ⊤

Tactic:
exact upperCentralSeries_nilpotencyClass

Result:
no goals

Proof state:
case succ.a
G : Type u_1
inst✝ : Group G
hH : IsNilpotent G
n : ℕ
hn : nilpotencyClass G = n + 1
⊢ upperCentralSeries (G ⧸ center G) n = ⊤

Tactic:
apply comap_injective (f := (mk' (center G))) Quot.mk_surjective

Result:
case succ.a.a
G : Type u_1
inst✝ : Group G
hH : IsNilpotent G
n : ℕ
hn : nilpotencyClass G = n + 1
⊢ comap (mk' (center G)) (upperCentralSeries (G ⧸ center G) n) = comap (mk' (center G)) ⊤

Proof state:
case succ.a
G : Type u_1
inst✝ : Group G
hH : IsNilpotent G
n : ℕ
hn : nilpotencyClass G = n + 1
⊢ n ≤ nilpotencyClass (G ⧸ center G)

Tactic:
apply le_of_add_le_add_right

Result:
case succ.a.bc
G : Type u_1
inst✝ : Group G
hH : IsNilpotent G
n : ℕ
hn : nilpotencyClass G = n + 1
⊢ n + ?succ.a.a ≤ nilpotencyClass (G ⧸ center G) + ?succ.a.a

case succ.a.a
G : Type u_1
inst✝ : Group G
hH : IsNilpotent G
n : ℕ
hn : nilpotencyClass G = n + 1
⊢ ℕ

Proof state:
G : Type u_1
inst✝ : Group G
hH : IsNilpotent G
n : ℕ
hn : nilpotencyClass G = n
⊢ nilpotencyClass (G ⧸ center G) = n - 1

Tactic:
rcases n with (rfl | n)

Result:
case zero
G : Type u_1
inst✝ : Group G
hH : IsNilpotent G
hn : nilpotencyClass G = 0
⊢ nilpotencyClass (G ⧸ center G) = 0 - 1

case succ
G : Type u_1
inst✝ : Group G
hH : IsNilpotent G
n : ℕ
hn : nilpotencyClass G = n + 1
⊢ nilpotencyClass (G ⧸ center G) = n + 1 - 1

Proof state:
G : Type u_1
inst✝ : Group G
hH : IsNilpotent G
n : ℕ
hn : nilpotencyClass G = n + 1
this : nilpotencyClass (G ⧸ center G) = n
⊢ nilpotencyClass (G ⧸ center G) = n + 1 - 1

Tactic:
simpa

Result:
no goals