G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
n : ℕ
h : lowerCentralSeries G n ≤ center G
⊢ ∀ (y : G), y ∈ {x | ∃ p, p ∈ lowerCentralSeries G n ∧ ∃ q, q ∈ ⊤ ∧ p * q * p⁻¹ * q⁻¹ = x} → y = 1
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
n : ℕ
h : lowerCentralSeries G n ≤ center G
⊢ lowerCentralSeries G (n + 1) = ⊥
rw [lowerCentralSeries_succ, closure_eq_bot_iff, Set.subset_singleton_iff]
case intro.intro.intro.intro.intro
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
n : ℕ
h : lowerCentralSeries G n ≤ center G
y : G
hy1 : y ∈ lowerCentralSeries G n
z : G
⊢ y * z * y⁻¹ * z⁻¹ = 1
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
n : ℕ
h : lowerCentralSeries G n ≤ center G
⊢ ∀ (y : G), y ∈ {x | ∃ p, p ∈ lowerCentralSeries G n ∧ ∃ q, q ∈ ⊤ ∧ p * q * p⁻¹ * q⁻¹ = x} → y = 1
rintro x ⟨y, hy1, z, ⟨⟩, rfl⟩
case intro.intro.intro.intro.intro
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
n : ℕ
h : lowerCentralSeries G n ≤ center G
y : G
hy1 : y ∈ lowerCentralSeries G n
z : G
⊢ z * y = y * z
case intro.intro.intro.intro.intro
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
n : ℕ
h : lowerCentralSeries G n ≤ center G
y : G
hy1 : y ∈ lowerCentralSeries G n
z : G
⊢ y * z * y⁻¹ * z⁻¹ = 1
rw [mul_assoc, ← mul_inv_rev, mul_inv_eq_one, eq_comm]
no goals
case intro.intro.intro.intro.intro
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
n : ℕ
h : lowerCentralSeries G n ≤ center G
y : G
hy1 : y ∈ lowerCentralSeries G n
z : G
⊢ z * y = y * z
exact mem_center_iff.mp (h hy1) z