case zero
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
⊢ comap (mk' (center G)) (upperCentralSeries (G ⧸ center G) Nat.zero) = upperCentralSeries G (Nat.succ Nat.zero)

case succ
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
n : ℕ
ih : comap (mk' (center G)) (upperCentralSeries (G ⧸ center G) n) = upperCentralSeries G (Nat.succ n)
⊢ comap (mk' (center G)) (upperCentralSeries (G ⧸ center G) (Nat.succ n)) = upperCentralSeries G (Nat.succ (Nat.succ n))
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
n : ℕ
⊢ comap (mk' (center G)) (upperCentralSeries (G ⧸ center G) n) = upperCentralSeries G (Nat.succ n)
induction' n with n ih
no goals
case zero
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
⊢ comap (mk' (center G)) (upperCentralSeries (G ⧸ center G) Nat.zero) = upperCentralSeries G (Nat.succ Nat.zero)
simp only [Nat.zero_eq, upperCentralSeries_zero, MonoidHom.comap_bot, ker_mk',
  (upperCentralSeries_one G).symm]
case succ
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
n : ℕ
ih : comap (mk' (center G)) (upperCentralSeries (G ⧸ center G) n) = upperCentralSeries G (Nat.succ n)
Hn : Subgroup (G ⧸ center G) := upperCentralSeries (G ⧸ center G) n
⊢ comap (mk' (center G)) (upperCentralSeries (G ⧸ center G) (Nat.succ n)) = upperCentralSeries G (Nat.succ (Nat.succ n))
case succ
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
n : ℕ
ih : comap (mk' (center G)) (upperCentralSeries (G ⧸ center G) n) = upperCentralSeries G (Nat.succ n)
⊢ comap (mk' (center G)) (upperCentralSeries (G ⧸ center G) (Nat.succ n)) = upperCentralSeries G (Nat.succ (Nat.succ n))
let Hn := upperCentralSeries (G ⧸ center G) n
no goals
case succ
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
n : ℕ
ih : comap (mk' (center G)) (upperCentralSeries (G ⧸ center G) n) = upperCentralSeries G (Nat.succ n)
Hn : Subgroup (G ⧸ center G) := upperCentralSeries (G ⧸ center G) n
⊢ comap (mk' (center G)) (upperCentralSeries (G ⧸ center G) (Nat.succ n)) = upperCentralSeries G (Nat.succ (Nat.succ n))
calc
  comap (mk' (center G)) (upperCentralSeriesStep Hn) =
      comap (mk' (center G)) (comap (mk' Hn) (center ((G ⧸ center G) ⧸ Hn))) :=
    by rw [upperCentralSeriesStep_eq_comap_center]
  _ = comap (mk' (comap (mk' (center G)) Hn)) (center (G ⧸ comap (mk' (center G)) Hn)) :=
    QuotientGroup.comap_comap_center
  _ = comap (mk' (upperCentralSeries G n.succ)) (center (G ⧸ upperCentralSeries G n.succ)) :=
    (comap_center_subst ih)
  _ = upperCentralSeriesStep (upperCentralSeries G n.succ) :=
    symm (upperCentralSeriesStep_eq_comap_center _)
no goals
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
n : ℕ
ih : comap (mk' (center G)) (upperCentralSeries (G ⧸ center G) n) = upperCentralSeries G (Nat.succ n)
Hn : Subgroup (G ⧸ center G) := upperCentralSeries (G ⧸ center G) n
⊢ comap (mk' (center G)) (upperCentralSeriesStep Hn) =
    comap (mk' (center G)) (comap (mk' Hn) (center ((G ⧸ center G) ⧸ Hn)))
rw [upperCentralSeriesStep_eq_comap_center]