G : Type u_2
inst✝² : Group G
H✝ : Subgroup G
inst✝¹ : Normal H✝
H : Type u_1
inst✝ : Group H
f : G →* H
hf1 : MonoidHom.ker f ≤ center G
hH : ∃ n, lowerCentralSeries H n = ⊥
⊢ ∃ n, lowerCentralSeries G n = ⊥
G : Type u_2
inst✝² : Group G
H✝ : Subgroup G
inst✝¹ : Normal H✝
H : Type u_1
inst✝ : Group H
f : G →* H
hf1 : MonoidHom.ker f ≤ center G
hH : Group.IsNilpotent H
⊢ Group.IsNilpotent G
rw [nilpotent_iff_lowerCentralSeries] at *
case intro
G : Type u_2
inst✝² : Group G
H✝ : Subgroup G
inst✝¹ : Normal H✝
H : Type u_1
inst✝ : Group H
f : G →* H
hf1 : MonoidHom.ker f ≤ center G
n : ℕ
hn : lowerCentralSeries H n = ⊥
⊢ ∃ n, lowerCentralSeries G n = ⊥
G : Type u_2
inst✝² : Group G
H✝ : Subgroup G
inst✝¹ : Normal H✝
H : Type u_1
inst✝ : Group H
f : G →* H
hf1 : MonoidHom.ker f ≤ center G
hH : ∃ n, lowerCentralSeries H n = ⊥
⊢ ∃ n, lowerCentralSeries G n = ⊥
rcases hH with ⟨n, hn⟩
case intro
G : Type u_2
inst✝² : Group G
H✝ : Subgroup G
inst✝¹ : Normal H✝
H : Type u_1
inst✝ : Group H
f : G →* H
hf1 : MonoidHom.ker f ≤ center G
n : ℕ
hn : lowerCentralSeries H n = ⊥
⊢ lowerCentralSeries G (n + 1) = ⊥
case intro
G : Type u_2
inst✝² : Group G
H✝ : Subgroup G
inst✝¹ : Normal H✝
H : Type u_1
inst✝ : Group H
f : G →* H
hf1 : MonoidHom.ker f ≤ center G
n : ℕ
hn : lowerCentralSeries H n = ⊥
⊢ ∃ n, lowerCentralSeries G n = ⊥
use n + 1
case intro
G : Type u_2
inst✝² : Group G
H✝ : Subgroup G
inst✝¹ : Normal H✝
H : Type u_1
inst✝ : Group H
f : G →* H
hf1 : MonoidHom.ker f ≤ center G
n : ℕ
hn : lowerCentralSeries H n = ⊥
⊢ Subgroup.map f (lowerCentralSeries G n) = ⊥
case intro
G : Type u_2
inst✝² : Group G
H✝ : Subgroup G
inst✝¹ : Normal H✝
H : Type u_1
inst✝ : Group H
f : G →* H
hf1 : MonoidHom.ker f ≤ center G
n : ℕ
hn : lowerCentralSeries H n = ⊥
⊢ lowerCentralSeries G (n + 1) = ⊥
refine' lowerCentralSeries_succ_eq_bot (le_trans ((Subgroup.map_eq_bot_iff _).mp _) hf1)
no goals
case intro
G : Type u_2
inst✝² : Group G
H✝ : Subgroup G
inst✝¹ : Normal H✝
H : Type u_1
inst✝ : Group H
f : G →* H
hf1 : MonoidHom.ker f ≤ center G
n : ℕ
hn : lowerCentralSeries H n = ⊥
⊢ Subgroup.map f (lowerCentralSeries G n) = ⊥
exact eq_bot_iff.mpr (hn ▸ lowerCentralSeries.map f n)