∀ {α : Type u_1} {R : Type u_2} [inst : Monoid α] [inst_1 : Ring R] (f : α →* R) (x y : FreeAbelianGroup α),
  (↑(FreeAbelianGroup.lift ⇑f)).toFun (x + y) =
    (↑(FreeAbelianGroup.lift ⇑f)).toFun x + (↑(FreeAbelianGroup.lift ⇑f)).toFun y