∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : Zero M] (f : α ≃ β) (l : α →₀ M),
  Finsupp.equivMapDomain f l =
    { support := Finset.map f.toEmbedding l.support, toFun := fun a => l (f.symm a), mem_support_toFun := ⋯ }