no goals
α : Type ?u.115990
R : Type u_2
k : Type ?u.115996
S : Type ?u.115999
M : Type u_1
M₂ : Type ?u.116005
M₃ : Type ?u.116008
ι : Type ?u.116011
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r✝ s✝ : R
x y✝ : M
r s : R
y : M
⊢ (r - s) • y = r • y - s • y
simp [add_smul, sub_eq_add_neg]