no goals
G : Type u_1
inst✝² : Group G
H : Subgroup G
A : Type u_2
inst✝¹ : CommGroup A
ϕ : { x // x ∈ H } →* A
T : ↑(leftTransversals ↑H)
inst✝ : FiniteIndex H
g : G
⊢ ↑(transfer ϕ) g = diff ϕ T (g • T)
rw [transfer, ← diff_mul_diff, ← smul_diff_smul, mul_comm, diff_mul_diff] <;> rfl