case left
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
⊢ lowerCentralSeries G 0 = ⊤

case right
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
⊢ ∀ (x : G) (n : ℕ), x ∈ lowerCentralSeries G n → ∀ (g : G), x * g * x⁻¹ * g⁻¹ ∈ lowerCentralSeries G (n + 1)
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
⊢ IsDescendingCentralSeries (lowerCentralSeries G)
constructor
case right
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
⊢ ∀ (x : G) (n : ℕ), x ∈ lowerCentralSeries G n → ∀ (g : G), x * g * x⁻¹ * g⁻¹ ∈ lowerCentralSeries G (n + 1)
case left
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
⊢ lowerCentralSeries G 0 = ⊤

case right
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
⊢ ∀ (x : G) (n : ℕ), x ∈ lowerCentralSeries G n → ∀ (g : G), x * g * x⁻¹ * g⁻¹ ∈ lowerCentralSeries G (n + 1)
rfl
case right
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
x : G
n : ℕ
hxn : x ∈ lowerCentralSeries G n
g : G
⊢ x * g * x⁻¹ * g⁻¹ ∈ lowerCentralSeries G (n + 1)
case right
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
⊢ ∀ (x : G) (n : ℕ), x ∈ lowerCentralSeries G n → ∀ (g : G), x * g * x⁻¹ * g⁻¹ ∈ lowerCentralSeries G (n + 1)
intro x n hxn g
no goals
case right
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
x : G
n : ℕ
hxn : x ∈ lowerCentralSeries G n
g : G
⊢ x * g * x⁻¹ * g⁻¹ ∈ lowerCentralSeries G (n + 1)
exact commutator_mem_commutator hxn (mem_top g)