case mp
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
hG : Group.IsNilpotent G
n : ℕ
⊢ upperCentralSeries 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 → upperCentralSeries G n = ⊤
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
hG : Group.IsNilpotent G
n : ℕ
⊢ upperCentralSeries 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 : upperCentralSeries 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 : ℕ
⊢ upperCentralSeries G n = ⊤ → nilpotencyClass G ≤ n
intro h
no goals
case mp
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
hG : Group.IsNilpotent G
n : ℕ
h : upperCentralSeries G n = ⊤
⊢ nilpotencyClass G ≤ 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
⊢ upperCentralSeries 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 → upperCentralSeries 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
⊢ ⊤ ≤ upperCentralSeries 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
⊢ upperCentralSeries G n = ⊤
apply eq_top_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
⊢ upperCentralSeries G (nilpotencyClass G) ≤ upperCentralSeries 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
⊢ ⊤ ≤ upperCentralSeries G n
rw [← upperCentralSeries_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
⊢ upperCentralSeries G (nilpotencyClass G) ≤ upperCentralSeries G n
exact upperCentralSeries_mono _ h