case zero
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
hf : Function.Surjective ↑f
⊢ derivedSeries G' Nat.zero ≤ map f (derivedSeries G Nat.zero)

case succ
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
hf : Function.Surjective ↑f
n : ℕ
ih : derivedSeries G' n ≤ map f (derivedSeries G n)
⊢ derivedSeries G' (Nat.succ n) ≤ map f (derivedSeries G (Nat.succ n))
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
hf : Function.Surjective ↑f
n : ℕ
⊢ derivedSeries G' n ≤ map f (derivedSeries G n)
induction' n with n ih
no goals
case zero
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
hf : Function.Surjective ↑f
⊢ derivedSeries G' Nat.zero ≤ map f (derivedSeries G Nat.zero)
exact (map_top_of_surjective f hf).ge
no goals
case succ
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
hf : Function.Surjective ↑f
n : ℕ
ih : derivedSeries G' n ≤ map f (derivedSeries G n)
⊢ derivedSeries G' (Nat.succ n) ≤ map f (derivedSeries G (Nat.succ n))
exact commutator_le_map_commutator ih ih