case h
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
x✝ : G
⊢ x✝ ∈ upperCentralSeriesStep H ↔ x✝ ∈ comap (mk' H) (center (G ⧸ H))
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
⊢ upperCentralSeriesStep H = comap (mk' H) (center (G ⧸ H))
ext
case h
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
x✝ : G
⊢ x✝ ∈ upperCentralSeriesStep H ↔ ∀ (x : G), ↑x * ↑(mk' H) x✝ = ↑(mk' H) x✝ * ↑x
case h
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
x✝ : G
⊢ x✝ ∈ upperCentralSeriesStep H ↔ x✝ ∈ comap (mk' H) (center (G ⧸ H))
rw [mem_comap, mem_center_iff, forall_mk]
case h.h
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
x✝ : G
⊢ ∀ (a : G), x✝ * a * x✝⁻¹ * a⁻¹ ∈ H ↔ ↑a * ↑(mk' H) x✝ = ↑(mk' H) x✝ * ↑a
case h
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
x✝ : G
⊢ x✝ ∈ upperCentralSeriesStep H ↔ ∀ (x : G), ↑x * ↑(mk' H) x✝ = ↑(mk' H) x✝ * ↑x
apply forall_congr'
case h.h
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
x✝ y : G
⊢ x✝ * y * x✝⁻¹ * y⁻¹ ∈ H ↔ ↑y * ↑(mk' H) x✝ = ↑(mk' H) x✝ * ↑y
case h.h
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
x✝ : G
⊢ ∀ (a : G), x✝ * a * x✝⁻¹ * a⁻¹ ∈ H ↔ ↑a * ↑(mk' H) x✝ = ↑(mk' H) x✝ * ↑a
intro y
no goals
case h.h
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Normal H
x✝ y : G
⊢ x✝ * y * x✝⁻¹ * y⁻¹ ∈ H ↔ ↑y * ↑(mk' H) x✝ = ↑(mk' H) x✝ * ↑y
rw [coe_mk', ← QuotientGroup.mk_mul, ← QuotientGroup.mk_mul, eq_comm, eq_iff_div_mem,
  div_eq_mul_inv, mul_inv_rev, mul_assoc]