case h
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
x✝ : G
⊢ x✝ ∈ upperCentralSeries G 1 ↔ x✝ ∈ center G
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
⊢ upperCentralSeries G 1 = center G
ext
case h
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
x✝ : G
⊢ (∀ (y : G), x✝ * y * x✝⁻¹ * y⁻¹ = 1) ↔ ∀ (m : G), m * x✝ = x✝ * m
case h
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
x✝ : G
⊢ x✝ ∈ upperCentralSeries G 1 ↔ x✝ ∈ center G
simp only [upperCentralSeries, upperCentralSeriesAux, upperCentralSeriesStep, center, Set.center,
  mem_mk, mem_bot, Set.mem_setOf_eq]
no goals
case h
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
x✝ : G
⊢ (∀ (y : G), x✝ * y * x✝⁻¹ * y⁻¹ = 1) ↔ ∀ (m : G), m * x✝ = x✝ * m
exact forall_congr' fun y => by rw [mul_inv_eq_one, mul_inv_eq_iff_eq_mul, eq_comm]
no goals
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
x✝ y : G
⊢ x✝ * y * x✝⁻¹ * y⁻¹ = 1 ↔ y * x✝ = x✝ * y
rw [mul_inv_eq_one, mul_inv_eq_iff_eq_mul, eq_comm]