G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
⊢ ∀ (n : ℕ), upperCentralSeries G n ≤ upperCentralSeries G (n + 1)
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
⊢ Monotone (upperCentralSeries G)
refine' monotone_nat_of_le_succ _
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
n : ℕ
x : G
hx : x ∈ upperCentralSeries G n
y : G
⊢ x * y * x⁻¹ * y⁻¹ ∈ (upperCentralSeriesAux G (Nat.add n 0)).fst
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
⊢ ∀ (n : ℕ), upperCentralSeries G n ≤ upperCentralSeries G (n + 1)
intro n x hx y
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
n : ℕ
x : G
hx : x ∈ upperCentralSeries G n
y : G
⊢ x * (y * x⁻¹ * y⁻¹) ∈ (upperCentralSeriesAux G (Nat.add n 0)).fst
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
n : ℕ
x : G
hx : x ∈ upperCentralSeries G n
y : G
⊢ x * y * x⁻¹ * y⁻¹ ∈ (upperCentralSeriesAux G (Nat.add n 0)).fst
rw [mul_assoc, mul_assoc, ← mul_assoc y x⁻¹ y⁻¹]
no goals
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
n : ℕ
x : G
hx : x ∈ upperCentralSeries G n
y : G
⊢ x * (y * x⁻¹ * y⁻¹) ∈ (upperCentralSeriesAux G (Nat.add n 0)).fst
exact mul_mem hx (Normal.conj_mem (upperCentralSeries_normal G n) x⁻¹ (inv_mem hx) y)