G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
n : ℕ
x : G
hx : x ∈ lowerCentralSeries G (n + 1)
⊢ x ∈ lowerCentralSeries G n
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
⊢ Antitone (lowerCentralSeries G)
refine' antitone_nat_of_succ_le fun n x hx => _
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
n : ℕ
x : G
hx : x ∈ closure {x | ∃ p, p ∈ lowerCentralSeries G n ∧ ∃ q, p * q * p⁻¹ * q⁻¹ = x}
⊢ x ∈ lowerCentralSeries G n
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
n : ℕ
x : G
hx : x ∈ lowerCentralSeries G (n + 1)
⊢ x ∈ lowerCentralSeries G n
simp only [mem_lowerCentralSeries_succ_iff, exists_prop, mem_top, exists_true_left,
  true_and_iff] at hx
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
n : ℕ
x : G
hx : x ∈ closure {x | ∃ p, p ∈ lowerCentralSeries G n ∧ ∃ q, p * q * p⁻¹ * q⁻¹ = x}
⊢ ∀ (x : G), x ∈ {x | ∃ p, p ∈ lowerCentralSeries G n ∧ ∃ q, p * q * p⁻¹ * q⁻¹ = x} → x ∈ lowerCentralSeries G n
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
n : ℕ
x : G
hx : x ∈ closure {x | ∃ p, p ∈ lowerCentralSeries G n ∧ ∃ q, p * q * p⁻¹ * q⁻¹ = x}
⊢ x ∈ lowerCentralSeries G n
refine'
  closure_induction hx _ (Subgroup.one_mem _) (@Subgroup.mul_mem _ _ _) (@Subgroup.inv_mem _ _ _)
case intro.intro.intro
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
n : ℕ
x : G
hx : x ∈ closure {x | ∃ p, p ∈ lowerCentralSeries G n ∧ ∃ q, p * q * p⁻¹ * q⁻¹ = x}
y z : G
hz : z ∈ lowerCentralSeries G n
a : G
ha : z * a * z⁻¹ * a⁻¹ = y
⊢ y ∈ lowerCentralSeries G n
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
n : ℕ
x : G
hx : x ∈ closure {x | ∃ p, p ∈ lowerCentralSeries G n ∧ ∃ q, p * q * p⁻¹ * q⁻¹ = x}
⊢ ∀ (x : G), x ∈ {x | ∃ p, p ∈ lowerCentralSeries G n ∧ ∃ q, p * q * p⁻¹ * q⁻¹ = x} → x ∈ lowerCentralSeries G n
rintro y ⟨z, hz, a, ha⟩
case intro.intro.intro
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
n : ℕ
x : G
hx : x ∈ closure {x | ∃ p, p ∈ lowerCentralSeries G n ∧ ∃ q, p * q * p⁻¹ * q⁻¹ = x}
y z : G
hz : z ∈ lowerCentralSeries G n
a : G
ha : z * a * z⁻¹ * a⁻¹ = y
⊢ z * (a * z⁻¹ * a⁻¹) ∈ lowerCentralSeries G n
case intro.intro.intro
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
n : ℕ
x : G
hx : x ∈ closure {x | ∃ p, p ∈ lowerCentralSeries G n ∧ ∃ q, p * q * p⁻¹ * q⁻¹ = x}
y z : G
hz : z ∈ lowerCentralSeries G n
a : G
ha : z * a * z⁻¹ * a⁻¹ = y
⊢ y ∈ lowerCentralSeries G n
rw [← ha, mul_assoc, mul_assoc, ← mul_assoc a z⁻¹ a⁻¹]
no goals
case intro.intro.intro
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
n : ℕ
x : G
hx : x ∈ closure {x | ∃ p, p ∈ lowerCentralSeries G n ∧ ∃ q, p * q * p⁻¹ * q⁻¹ = x}
y z : G
hz : z ∈ lowerCentralSeries G n
a : G
ha : z * a * z⁻¹ * a⁻¹ = y
⊢ z * (a * z⁻¹ * a⁻¹) ∈ lowerCentralSeries G n
exact mul_mem hz (Normal.conj_mem (lowerCentralSeries_normal n) z⁻¹ (inv_mem hz) a)