∀ (M : Type u_1) (R : Type u_2) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (X : Type u_3)
  (x y : X → M), (Finsupp.lift M R X).toFun (x + y) = (Finsupp.lift M R X).toFun x + (Finsupp.lift M R X).toFun y