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

case succ
G : Type u_2
G' : Type u_1
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
n : ℕ
ih : map f (derivedSeries G n) ≤ derivedSeries G' n
⊢ map f (derivedSeries G (Nat.succ n)) ≤ derivedSeries G' (Nat.succ n)
G : Type u_2
G' : Type u_1
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
n : ℕ
⊢ map f (derivedSeries G n) ≤ derivedSeries G' n
induction' n with n ih
no goals
case zero
G : Type u_2
G' : Type u_1
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
⊢ map f (derivedSeries G Nat.zero) ≤ derivedSeries G' Nat.zero
exact le_top
no goals
case succ
G : Type u_2
G' : Type u_1
inst✝¹ : Group G
inst✝ : Group G'
f : G →* G'
n : ℕ
ih : map f (derivedSeries G n) ≤ derivedSeries G' n
⊢ map f (derivedSeries G (Nat.succ n)) ≤ derivedSeries G' (Nat.succ n)
simp only [derivedSeries_succ, map_commutator, commutator_mono, ih]