-- Mathlib/GroupTheory/Nilpotent.lean
theorem nilpotencyClass_le_of_ker_le_center {H : Type*} [Group H] (f : G →* H)
    (hf1 : f.ker ≤ center G) (hH : IsNilpotent H) :
    Group.nilpotencyClass (hG := isNilpotent_of_ker_le_center f hf1 hH) ≤
      Group.nilpotencyClass H + 1

Proof state:
case h
G : Type u_1
inst✝¹ : Group G
H : Type u_2
inst✝ : Group H
f : G →* H
hf1 : f.ker ≤ center G
hH : IsNilpotent H
this : IsNilpotent G
⊢ Subgroup.map f (lowerCentralSeries G (nilpotencyClass H)) = ⊥

Tactic:
rw [eq_bot_iff]

Result:
case h
G : Type u_1
inst✝¹ : Group G
H : Type u_2
inst✝ : Group H
f : G →* H
hf1 : f.ker ≤ center G
hH : IsNilpotent H
this : IsNilpotent G
⊢ Subgroup.map f (lowerCentralSeries G (nilpotencyClass H)) ≤ ⊥

Proof state:
G : Type u_1
inst✝¹ : Group G
H : Type u_2
inst✝ : Group H
f : G →* H
hf1 : f.ker ≤ center G
hH : IsNilpotent H
this : IsNilpotent G
⊢ Nat.find ⋯ ≤ nilpotencyClass H + 1

Tactic:
apply Nat.find_min'

Result:
case h
G : Type u_1
inst✝¹ : Group G
H : Type u_2
inst✝ : Group H
f : G →* H
hf1 : f.ker ≤ center G
hH : IsNilpotent H
this : IsNilpotent G
⊢ lowerCentralSeries G (nilpotencyClass H + 1) = ⊥

Proof state:
G : Type u_1
inst✝¹ : Group G
H : Type u_2
inst✝ : Group H
f : G →* H
hf1 : f.ker ≤ center G
hH : IsNilpotent H
this : IsNilpotent G
⊢ Nat.find ⋯ ≤ nilpotencyClass H + 1

Tactic:
classical apply Nat.find_min'

Result:
case h
G : Type u_1
inst✝¹ : Group G
H : Type u_2
inst✝ : Group H
f : G →* H
hf1 : f.ker ≤ center G
hH : IsNilpotent H
this : IsNilpotent G
⊢ lowerCentralSeries G (nilpotencyClass H + 1) = ⊥

Proof state:
case h
G : Type u_1
inst✝¹ : Group G
H : Type u_2
inst✝ : Group H
f : G →* H
hf1 : f.ker ≤ center G
hH : IsNilpotent H
this : IsNilpotent G
⊢ Subgroup.map f (lowerCentralSeries G (nilpotencyClass H)) ≤ ⊥

Tactic:
apply le_trans (lowerCentralSeries.map f _)

Result:
case h
G : Type u_1
inst✝¹ : Group G
H : Type u_2
inst✝ : Group H
f : G →* H
hf1 : f.ker ≤ center G
hH : IsNilpotent H
this : IsNilpotent G
⊢ lowerCentralSeries H (nilpotencyClass H) ≤ ⊥

Proof state:
G : Type u_1
inst✝¹ : Group G
H : Type u_2
inst✝ : Group H
f : G →* H
hf1 : f.ker ≤ center G
hH : IsNilpotent H
⊢ nilpotencyClass G ≤ nilpotencyClass H + 1

Tactic:
haveI : IsNilpotent G := isNilpotent_of_ker_le_center f hf1 hH

Result:
G : Type u_1
inst✝¹ : Group G
H : Type u_2
inst✝ : Group H
f : G →* H
hf1 : f.ker ≤ center G
hH : IsNilpotent H
this : IsNilpotent G
⊢ nilpotencyClass G ≤ nilpotencyClass H + 1

Proof state:
case h
G : Type u_1
inst✝¹ : Group G
H : Type u_2
inst✝ : Group H
f : G →* H
hf1 : f.ker ≤ center G
hH : IsNilpotent H
this : IsNilpotent G
⊢ lowerCentralSeries H (nilpotencyClass H) ≤ ⊥

Tactic:
simp only [lowerCentralSeries_nilpotencyClass, le_bot_iff]

Result:
no goals

Proof state:
G : Type u_1
inst✝¹ : Group G
H : Type u_2
inst✝ : Group H
f : G →* H
hf1 : f.ker ≤ center G
hH : IsNilpotent H
this : IsNilpotent G
⊢ nilpotencyClass G ≤ nilpotencyClass H + 1

Tactic:
rw [← lowerCentralSeries_length_eq_nilpotencyClass]

Result:
G : Type u_1
inst✝¹ : Group G
H : Type u_2
inst✝ : Group H
f : G →* H
hf1 : f.ker ≤ center G
hH : IsNilpotent H
this : IsNilpotent G
⊢ Nat.find ⋯ ≤ nilpotencyClass H + 1

Proof state:
case h
G : Type u_1
inst✝¹ : Group G
H : Type u_2
inst✝ : Group H
f : G →* H
hf1 : f.ker ≤ center G
hH : IsNilpotent H
this : IsNilpotent G
⊢ lowerCentralSeries G (nilpotencyClass H + 1) = ⊥

Tactic:
refine lowerCentralSeries_succ_eq_bot (le_trans ((Subgroup.map_eq_bot_iff _).mp ?_) hf1)

Result:
case h
G : Type u_1
inst✝¹ : Group G
H : Type u_2
inst✝ : Group H
f : G →* H
hf1 : f.ker ≤ center G
hH : IsNilpotent H
this : IsNilpotent G
⊢ Subgroup.map f (lowerCentralSeries G (nilpotencyClass H)) = ⊥