∀ {α : Type u_1} {β : Type u_2} {M : Type u_3} {R : Type u_6} [inst : Zero M] [inst_1 : SMulZeroClass R M] {f : α → β}
  (r : R) (v : β →₀ M) (hfv : Set.InjOn f (f ⁻¹' ↑v.support))
  (hfrv : optParam (Set.InjOn f (f ⁻¹' ↑(r • v).support)) ⋯),
  Finsupp.comapDomain f (r • v) hfrv = r • Finsupp.comapDomain f v hfv