case zero
G : Type u_1
G' : Type ?u.4100
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
⊢ Normal (derivedSeries G Nat.zero)

case succ
G : Type u_1
G' : Type ?u.4100
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
n : ℕ
ih : Normal (derivedSeries G n)
⊢ Normal (derivedSeries G (Nat.succ n))
G : Type u_1
G' : Type ?u.4100
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
n : ℕ
⊢ Normal (derivedSeries G n)
induction' n with n ih
no goals
case zero
G : Type u_1
G' : Type ?u.4100
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
⊢ Normal (derivedSeries G Nat.zero)
exact (⊤ : Subgroup G).normal_of_characteristic
no goals
case succ
G : Type u_1
G' : Type ?u.4100
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
n : ℕ
ih : Normal (derivedSeries G n)
⊢ Normal (derivedSeries G (Nat.succ n))
exact @Subgroup.commutator_normal G _ (derivedSeries G n) (derivedSeries G n) ih ih