no goals
α : Type ?u.65153
R : Type u_1
k : Type ?u.65159
S : Type ?u.65162
M : Type u_2
M₂ : Type ?u.65168
M₃ : Type ?u.65171
ι : Type ?u.65174
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r s : R
x y : M
zero_eq_one : 0 = 1
⊢ x = 0
rw [← one_smul R x, ← zero_eq_one, zero_smul]