G : Type u_1
inst✝¹ : Group G
H✝ : Subgroup G
inst✝ : Normal H✝
H : ℕ → Subgroup G
hH : IsAscendingCentralSeries H
n : ℕ
x : G
hx : x ∈ H (n + 1)
⊢ x ∈ upperCentralSeries G (n + 1)
G : Type u_1
inst✝¹ : Group G
H✝ : Subgroup G
inst✝ : Normal H✝
H : ℕ → Subgroup G
hH : IsAscendingCentralSeries H
n : ℕ
⊢ H (n + 1) ≤ upperCentralSeries G (n + 1)
intro x hx
G : Type u_1
inst✝¹ : Group G
H✝ : Subgroup G
inst✝ : Normal H✝
H : ℕ → Subgroup G
hH : IsAscendingCentralSeries H
n : ℕ
x : G
hx : x ∈ H (n + 1)
⊢ ∀ (y : G), x * y * x⁻¹ * y⁻¹ ∈ upperCentralSeries G n
G : Type u_1
inst✝¹ : Group G
H✝ : Subgroup G
inst✝ : Normal H✝
H : ℕ → Subgroup G
hH : IsAscendingCentralSeries H
n : ℕ
x : G
hx : x ∈ H (n + 1)
⊢ x ∈ upperCentralSeries G (n + 1)
rw [mem_upperCentralSeries_succ_iff]
no goals
G : Type u_1
inst✝¹ : Group G
H✝ : Subgroup G
inst✝ : Normal H✝
H : ℕ → Subgroup G
hH : IsAscendingCentralSeries H
n : ℕ
x : G
hx : x ∈ H (n + 1)
⊢ ∀ (y : G), x * y * x⁻¹ * y⁻¹ ∈ upperCentralSeries G n
exact fun y => ascending_central_series_le_upper H hH n (hH.2 x n hx y)