case mk.intro
G : Type u_3
G'✝ : Type ?u.45008
inst✝³ : Group G
inst✝² : Group G'✝
f✝ : G →* G'✝
G' : Type u_1
G'' : Type u_2
inst✝¹ : Group G'
inst✝ : Group G''
f : G' →* G
g : G →* G''
hfg : MonoidHom.ker g ≤ MonoidHom.range f
hG' : IsSolvable G'
hG'' : IsSolvable G''
n : ℕ
hn : derivedSeries G'' n = ⊥
⊢ IsSolvable G
G : Type u_3
G'✝ : Type ?u.45008
inst✝³ : Group G
inst✝² : Group G'✝
f✝ : G →* G'✝
G' : Type u_1
G'' : Type u_2
inst✝¹ : Group G'
inst✝ : Group G''
f : G' →* G
g : G →* G''
hfg : MonoidHom.ker g ≤ MonoidHom.range f
hG' : IsSolvable G'
hG'' : IsSolvable G''
⊢ IsSolvable G
obtain ⟨n, hn⟩ := id hG''
case mk.intro.mk.intro
G : Type u_3
G'✝ : Type ?u.45008
inst✝³ : Group G
inst✝² : Group G'✝
f✝ : G →* G'✝
G' : Type u_1
G'' : Type u_2
inst✝¹ : Group G'
inst✝ : Group G''
f : G' →* G
g : G →* G''
hfg : MonoidHom.ker g ≤ MonoidHom.range f
hG' : IsSolvable G'
hG'' : IsSolvable G''
n : ℕ
hn : derivedSeries G'' n = ⊥
m : ℕ
hm : derivedSeries G' m = ⊥
⊢ IsSolvable G
case mk.intro
G : Type u_3
G'✝ : Type ?u.45008
inst✝³ : Group G
inst✝² : Group G'✝
f✝ : G →* G'✝
G' : Type u_1
G'' : Type u_2
inst✝¹ : Group G'
inst✝ : Group G''
f : G' →* G
g : G →* G''
hfg : MonoidHom.ker g ≤ MonoidHom.range f
hG' : IsSolvable G'
hG'' : IsSolvable G''
n : ℕ
hn : derivedSeries G'' n = ⊥
⊢ IsSolvable G
obtain ⟨m, hm⟩ := id hG'
case mk.intro.mk.intro
G : Type u_3
G'✝ : Type ?u.45008
inst✝³ : Group G
inst✝² : Group G'✝
f✝ : G →* G'✝
G' : Type u_1
G'' : Type u_2
inst✝¹ : Group G'
inst✝ : Group G''
f : G' →* G
g : G →* G''
hfg : MonoidHom.ker g ≤ MonoidHom.range f
hG' : IsSolvable G'
hG'' : IsSolvable G''
n : ℕ
hn : derivedSeries G'' n = ⊥
m : ℕ
hm : derivedSeries G' m = ⊥
⊢ derivedSeries G (n + m) ≤ map f (derivedSeries G' m)
case mk.intro.mk.intro
G : Type u_3
G'✝ : Type ?u.45008
inst✝³ : Group G
inst✝² : Group G'✝
f✝ : G →* G'✝
G' : Type u_1
G'' : Type u_2
inst✝¹ : Group G'
inst✝ : Group G''
f : G' →* G
g : G →* G''
hfg : MonoidHom.ker g ≤ MonoidHom.range f
hG' : IsSolvable G'
hG'' : IsSolvable G''
n : ℕ
hn : derivedSeries G'' n = ⊥
m : ℕ
hm : derivedSeries G' m = ⊥
⊢ IsSolvable G
refine' ⟨⟨n + m, le_bot_iff.mp (map_bot f ▸ hm ▸ _)⟩⟩
case mk.intro.mk.intro
G : Type u_3
G'✝ : Type ?u.45008
inst✝³ : Group G
inst✝² : Group G'✝
f✝ : G →* G'✝
G' : Type u_1
G'' : Type u_2
inst✝¹ : Group G'
inst✝ : Group G''
f : G' →* G
g : G →* G''
hfg : MonoidHom.ker g ≤ MonoidHom.range f
hG' : IsSolvable G'
hG'' : IsSolvable G''
n : ℕ
hn : derivedSeries G'' n = ⊥
m : ℕ
⊢ derivedSeries G (n + m) ≤ map f (derivedSeries G' m)
case mk.intro.mk.intro
G : Type u_3
G'✝ : Type ?u.45008
inst✝³ : Group G
inst✝² : Group G'✝
f✝ : G →* G'✝
G' : Type u_1
G'' : Type u_2
inst✝¹ : Group G'
inst✝ : Group G''
f : G' →* G
g : G →* G''
hfg : MonoidHom.ker g ≤ MonoidHom.range f
hG' : IsSolvable G'
hG'' : IsSolvable G''
n : ℕ
hn : derivedSeries G'' n = ⊥
m : ℕ
hm : derivedSeries G' m = ⊥
⊢ derivedSeries G (n + m) ≤ map f (derivedSeries G' m)
clear hm
case mk.intro.mk.intro.zero
G : Type u_3
G'✝ : Type ?u.45008
inst✝³ : Group G
inst✝² : Group G'✝
f✝ : G →* G'✝
G' : Type u_1
G'' : Type u_2
inst✝¹ : Group G'
inst✝ : Group G''
f : G' →* G
g : G →* G''
hfg : MonoidHom.ker g ≤ MonoidHom.range f
hG' : IsSolvable G'
hG'' : IsSolvable G''
n : ℕ
hn : derivedSeries G'' n = ⊥
⊢ derivedSeries G (n + Nat.zero) ≤ map f (derivedSeries G' Nat.zero)

case mk.intro.mk.intro.succ
G : Type u_3
G'✝ : Type ?u.45008
inst✝³ : Group G
inst✝² : Group G'✝
f✝ : G →* G'✝
G' : Type u_1
G'' : Type u_2
inst✝¹ : Group G'
inst✝ : Group G''
f : G' →* G
g : G →* G''
hfg : MonoidHom.ker g ≤ MonoidHom.range f
hG' : IsSolvable G'
hG'' : IsSolvable G''
n : ℕ
hn : derivedSeries G'' n = ⊥
m : ℕ
hm : derivedSeries G (n + m) ≤ map f (derivedSeries G' m)
⊢ derivedSeries G (n + Nat.succ m) ≤ map f (derivedSeries G' (Nat.succ m))
case mk.intro.mk.intro
G : Type u_3
G'✝ : Type ?u.45008
inst✝³ : Group G
inst✝² : Group G'✝
f✝ : G →* G'✝
G' : Type u_1
G'' : Type u_2
inst✝¹ : Group G'
inst✝ : Group G''
f : G' →* G
g : G →* G''
hfg : MonoidHom.ker g ≤ MonoidHom.range f
hG' : IsSolvable G'
hG'' : IsSolvable G''
n : ℕ
hn : derivedSeries G'' n = ⊥
m : ℕ
⊢ derivedSeries G (n + m) ≤ map f (derivedSeries G' m)
induction' m with m hm
no goals
case mk.intro.mk.intro.zero
G : Type u_3
G'✝ : Type ?u.45008
inst✝³ : Group G
inst✝² : Group G'✝
f✝ : G →* G'✝
G' : Type u_1
G'' : Type u_2
inst✝¹ : Group G'
inst✝ : Group G''
f : G' →* G
g : G →* G''
hfg : MonoidHom.ker g ≤ MonoidHom.range f
hG' : IsSolvable G'
hG'' : IsSolvable G''
n : ℕ
hn : derivedSeries G'' n = ⊥
⊢ derivedSeries G (n + Nat.zero) ≤ map f (derivedSeries G' Nat.zero)
exact f.range_eq_map ▸ ((derivedSeries G n).map_eq_bot_iff.mp
  (le_bot_iff.mp ((map_derivedSeries_le_derivedSeries g n).trans hn.le))).trans hfg
no goals
case mk.intro.mk.intro.succ
G : Type u_3
G'✝ : Type ?u.45008
inst✝³ : Group G
inst✝² : Group G'✝
f✝ : G →* G'✝
G' : Type u_1
G'' : Type u_2
inst✝¹ : Group G'
inst✝ : Group G''
f : G' →* G
g : G →* G''
hfg : MonoidHom.ker g ≤ MonoidHom.range f
hG' : IsSolvable G'
hG'' : IsSolvable G''
n : ℕ
hn : derivedSeries G'' n = ⊥
m : ℕ
hm : derivedSeries G (n + m) ≤ map f (derivedSeries G' m)
⊢ derivedSeries G (n + Nat.succ m) ≤ map f (derivedSeries G' (Nat.succ m))
exact commutator_le_map_commutator hm hm