no goals
G : Type u
inst✝ : Group G
H : Subgroup G
g : G
q : G ⧸ H
⊢ ↑(transferFunction H g q) = q
rw [transferFunction_apply, ← smul_eq_mul, Quotient.coe_smul_out',
  ← quotientEquivSigmaZMod_symm_apply, Sigma.eta, symm_apply_apply]