case mp
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
hG : Group.IsNilpotent G
n : ℕ
⊢ lowerCentralSeries G n = ⊥ → nilpotencyClass G ≤ n

case mpr
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
hG : Group.IsNilpotent G
n : ℕ
⊢ nilpotencyClass G ≤ n → lowerCentralSeries G n = ⊥
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
hG : Group.IsNilpotent G
n : ℕ
⊢ lowerCentralSeries G n = ⊥ ↔ nilpotencyClass G ≤ n
constructor
case mp
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
hG : Group.IsNilpotent G
n : ℕ
h : lowerCentralSeries G n = ⊥
⊢ nilpotencyClass G ≤ n
case mp
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
hG : Group.IsNilpotent G
n : ℕ
⊢ lowerCentralSeries G n = ⊥ → nilpotencyClass G ≤ n
intro h
case mp
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
hG : Group.IsNilpotent G
n : ℕ
h : lowerCentralSeries G n = ⊥
⊢ Nat.find (_ : ∃ n, lowerCentralSeries G n = ⊥) ≤ n
case mp
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
hG : Group.IsNilpotent G
n : ℕ
h : lowerCentralSeries G n = ⊥
⊢ nilpotencyClass G ≤ n
rw [← lowerCentralSeries_length_eq_nilpotencyClass]
no goals
case mp
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
hG : Group.IsNilpotent G
n : ℕ
h : lowerCentralSeries G n = ⊥
⊢ Nat.find (_ : ∃ n, lowerCentralSeries G n = ⊥) ≤ n
exact Nat.find_le h
case mpr
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
hG : Group.IsNilpotent G
n : ℕ
h : nilpotencyClass G ≤ n
⊢ lowerCentralSeries G n = ⊥
case mpr
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
hG : Group.IsNilpotent G
n : ℕ
⊢ nilpotencyClass G ≤ n → lowerCentralSeries G n = ⊥
intro h
case mpr
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
hG : Group.IsNilpotent G
n : ℕ
h : nilpotencyClass G ≤ n
⊢ lowerCentralSeries G n ≤ ⊥
case mpr
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
hG : Group.IsNilpotent G
n : ℕ
h : nilpotencyClass G ≤ n
⊢ lowerCentralSeries G n = ⊥
apply eq_bot_iff.mpr
case mpr
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
hG : Group.IsNilpotent G
n : ℕ
h : nilpotencyClass G ≤ n
⊢ lowerCentralSeries G n ≤ lowerCentralSeries G (nilpotencyClass G)
case mpr
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
hG : Group.IsNilpotent G
n : ℕ
h : nilpotencyClass G ≤ n
⊢ lowerCentralSeries G n ≤ ⊥
rw [← lowerCentralSeries_nilpotencyClass]
no goals
case mpr
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
hG : Group.IsNilpotent G
n : ℕ
h : nilpotencyClass G ≤ n
⊢ lowerCentralSeries G n ≤ lowerCentralSeries G (nilpotencyClass G)
exact lowerCentralSeries_antitone h