∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G} {A : Type u_2} [inst_1 : AddCommGroup A] (ϕ : ↥H →+ A)
  [inst_2 : H.FiniteIndex],
  ϕ.transfer =
    { toFun := fun g => AddSubgroup.leftTransversals.diff ϕ default (g +ᵥ default), map_zero' := ⋯, map_add' := ⋯ }