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
this : Group.IsNilpotent G
⊢ nilpotencyClass G ≤ nilpotencyClass H + 1
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
⊢ nilpotencyClass G ≤ nilpotencyClass H + 1
haveI : IsNilpotent G := isNilpotent_of_ker_le_center f hf1 hH
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
this : Group.IsNilpotent G
⊢ Nat.find (_ : ∃ n, lowerCentralSeries G n = ⊥) ≤ nilpotencyClass H + 1
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
this : Group.IsNilpotent G
⊢ nilpotencyClass G ≤ nilpotencyClass H + 1
rw [← lowerCentralSeries_length_eq_nilpotencyClass]
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
this : Group.IsNilpotent G
⊢ lowerCentralSeries G (nilpotencyClass H + 1) = ⊥
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
this : Group.IsNilpotent G
⊢ Nat.find (_ : ∃ n, lowerCentralSeries G n = ⊥) ≤ nilpotencyClass H + 1
refine @Nat.find_min' _ (Classical.decPred _) _ _ ?_
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
this : Group.IsNilpotent G
⊢ Subgroup.map f (lowerCentralSeries G (nilpotencyClass H)) = ⊥
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
this : Group.IsNilpotent G
⊢ lowerCentralSeries G (nilpotencyClass H + 1) = ⊥
refine lowerCentralSeries_succ_eq_bot (le_trans ((Subgroup.map_eq_bot_iff _).mp ?_) hf1)
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
this : Group.IsNilpotent G
⊢ Subgroup.map f (lowerCentralSeries G (nilpotencyClass H)) ≤ ⊥
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
this : Group.IsNilpotent G
⊢ Subgroup.map f (lowerCentralSeries G (nilpotencyClass H)) = ⊥
apply eq_bot_iff.mpr
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
this : Group.IsNilpotent G
⊢ lowerCentralSeries H (nilpotencyClass H) ≤ ⊥
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
this : Group.IsNilpotent G
⊢ Subgroup.map f (lowerCentralSeries G (nilpotencyClass H)) ≤ ⊥
apply le_trans (lowerCentralSeries.map f _)
no goals
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
this : Group.IsNilpotent G
⊢ lowerCentralSeries H (nilpotencyClass H) ≤ ⊥
simp only [lowerCentralSeries_nilpotencyClass, le_bot_iff]