G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
hH : Group.IsNilpotent G
n : ℕ
hn : nilpotencyClass G = n
⊢ nilpotencyClass (G ⧸ center G) = n - 1
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
hH : Group.IsNilpotent G
⊢ nilpotencyClass (G ⧸ center G) = nilpotencyClass G - 1
generalize hn : Group.nilpotencyClass G = n
case zero
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
hH : Group.IsNilpotent G
hn : nilpotencyClass G = Nat.zero
⊢ nilpotencyClass (G ⧸ center G) = Nat.zero - 1

case succ
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
hH : Group.IsNilpotent G
n : ℕ
hn : nilpotencyClass G = Nat.succ n
⊢ nilpotencyClass (G ⧸ center G) = Nat.succ n - 1
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
hH : Group.IsNilpotent G
n : ℕ
hn : nilpotencyClass G = n
⊢ nilpotencyClass (G ⧸ center G) = n - 1
rcases n with (rfl | n)
case zero
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
hH : Group.IsNilpotent G
hn : Subsingleton G
⊢ Subsingleton (G ⧸ center G)
case zero
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
hH : Group.IsNilpotent G
hn : nilpotencyClass G = Nat.zero
⊢ nilpotencyClass (G ⧸ center G) = Nat.zero - 1
simp [nilpotencyClass_zero_iff_subsingleton] at *
no goals
case zero
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
hH : Group.IsNilpotent G
hn : Subsingleton G
⊢ Subsingleton (G ⧸ center G)
exact Quotient.instSubsingletonQuotient (leftRel (center G))
case succ
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
hH : Group.IsNilpotent G
n : ℕ
hn : nilpotencyClass G = Nat.succ n
⊢ nilpotencyClass (G ⧸ center G) = n
case succ
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
hH : Group.IsNilpotent G
n : ℕ
hn : nilpotencyClass G = Nat.succ n
⊢ nilpotencyClass (G ⧸ center G) = Nat.succ n - 1
suffices Group.nilpotencyClass (G ⧸ center G) = n by simpa
case succ.a
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
hH : Group.IsNilpotent G
n : ℕ
hn : nilpotencyClass G = Nat.succ n
⊢ nilpotencyClass (G ⧸ center G) ≤ n

case succ.a
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
hH : Group.IsNilpotent G
n : ℕ
hn : nilpotencyClass G = Nat.succ n
⊢ n ≤ nilpotencyClass (G ⧸ center G)
case succ
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
hH : Group.IsNilpotent G
n : ℕ
hn : nilpotencyClass G = Nat.succ n
⊢ nilpotencyClass (G ⧸ center G) = n
apply le_antisymm
no goals
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
hH : Group.IsNilpotent G
n : ℕ
hn : nilpotencyClass G = Nat.succ n
this : nilpotencyClass (G ⧸ center G) = n
⊢ nilpotencyClass (G ⧸ center G) = Nat.succ n - 1
simpa
case succ.a
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
hH : Group.IsNilpotent G
n : ℕ
hn : nilpotencyClass G = Nat.succ n
⊢ upperCentralSeries (G ⧸ center G) n = ⊤
case succ.a
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
hH : Group.IsNilpotent G
n : ℕ
hn : nilpotencyClass G = Nat.succ n
⊢ nilpotencyClass (G ⧸ center G) ≤ n
apply upperCentralSeries_eq_top_iff_nilpotencyClass_le.mp
case succ.a.a
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
hH : Group.IsNilpotent G
n : ℕ
hn : nilpotencyClass G = Nat.succ n
⊢ comap (mk' (center G)) (upperCentralSeries (G ⧸ center G) n) = comap (mk' (center G)) ⊤
case succ.a
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
hH : Group.IsNilpotent G
n : ℕ
hn : nilpotencyClass G = Nat.succ n
⊢ upperCentralSeries (G ⧸ center G) n = ⊤
apply @comap_injective G _ _ _ (mk' (center G)) (surjective_quot_mk _)
case succ.a.a
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
hH : Group.IsNilpotent G
n : ℕ
hn : nilpotencyClass G = Nat.succ n
⊢ upperCentralSeries G (nilpotencyClass G) = ⊤
case succ.a.a
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
hH : Group.IsNilpotent G
n : ℕ
hn : nilpotencyClass G = Nat.succ n
⊢ comap (mk' (center G)) (upperCentralSeries (G ⧸ center G) n) = comap (mk' (center G)) ⊤
rw [comap_upperCentralSeries_quotient_center, comap_top, ← hn]
no goals
case succ.a.a
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
hH : Group.IsNilpotent G
n : ℕ
hn : nilpotencyClass G = Nat.succ n
⊢ upperCentralSeries G (nilpotencyClass G) = ⊤
exact upperCentralSeries_nilpotencyClass
case succ.a.bc
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
hH : Group.IsNilpotent G
n : ℕ
hn : nilpotencyClass G = Nat.succ n
⊢ n + ?succ.a.a ≤ nilpotencyClass (G ⧸ center G) + ?succ.a.a

case succ.a.a
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
hH : Group.IsNilpotent G
n : ℕ
hn : nilpotencyClass G = Nat.succ n
⊢ ℕ
case succ.a
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
hH : Group.IsNilpotent G
n : ℕ
hn : nilpotencyClass G = Nat.succ n
⊢ n ≤ nilpotencyClass (G ⧸ center G)
apply le_of_add_le_add_right
no goals
case succ.a.bc
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
hH : Group.IsNilpotent G
n : ℕ
hn : nilpotencyClass G = Nat.succ n
⊢ n + ?succ.a.a ≤ nilpotencyClass (G ⧸ center G) + ?succ.a.a

case succ.a.a
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
hH : Group.IsNilpotent G
n : ℕ
hn : nilpotencyClass G = Nat.succ n
⊢ ℕ
calc
  n + 1 = n.succ := rfl
  _ = Group.nilpotencyClass G := (symm hn)
  _ ≤ Group.nilpotencyClass (G ⧸ center G) + 1 :=
    nilpotencyClass_le_of_ker_le_center _ (le_of_eq (ker_mk' _)) _