no goals
α : Type ?u.67416
R✝ : Type ?u.67419
k : Type ?u.67422
S : Type ?u.67425
M : Type u_2
M₂ : Type ?u.67431
M₃ : Type ?u.67434
ι : Type ?u.67437
inst✝⁴ : Semiring R✝
inst✝³ : AddCommMonoid M
inst✝² : Module R✝ M
r✝ s : R✝
x y : M
R : Type u_1
inst✝¹ : Ring R
inst✝ : Module R M
r : R
m : M
⊢ r • m + (1 - r) • m = m
rw [← add_smul, add_sub_cancel'_right, one_smul]