no goals
G : Type u
inst✝ : Group G
H : Subgroup G
g : G
q : orbitRel.Quotient { x // x ∈ zpowers g } (G ⧸ H)
k : ℤ
⊢ ↑(quotientEquivSigmaZMod H g) (g ^ k • Quotient.out' q) = { fst := q, snd := ↑k }
rw [apply_eq_iff_eq_symm_apply, quotientEquivSigmaZMod_symm_apply, ZMod.coe_int_cast,
  zpow_smul_mod_minimalPeriod]