no goals
G : Type u
inst✝ : Group G
H : Subgroup G
g : G
q : orbitRel.Quotient { x // x ∈ zpowers g } (G ⧸ H)
k : ZMod (minimalPeriod ((fun x x_1 => x • x_1) g) (Quotient.out' q))
⊢ ↑(↑(toEquiv (_ : ↑(transferTransversal H g) ∈ leftTransversals ↑H)) (g ^ ↑k • Quotient.out' q)) =
    g ^ ↑k * Quotient.out' (Quotient.out' q)
rw [transferTransversal_apply, transferFunction_apply, ← quotientEquivSigmaZMod_symm_apply,
  apply_symm_apply]