no goals
G : Type u_1
inst✝² : Group G
H : Subgroup G
A : Type ?u.848720
inst✝¹ : CommGroup A
ϕ : { x // x ∈ H } →* A
T : ↑(leftTransversals ↑H)
inst✝ : FiniteIndex (center G)
g : G
k : ℕ
x✝ : G
hk : x✝⁻¹ * g ^ k * x✝ ∈ center G
⊢ x✝⁻¹ * g ^ k * x✝ = g ^ k
rw [← mul_right_inj, hk, mul_inv_cancel_right]