no goals
α : Type ?u.15019
R : Type u_2
k : Type ?u.15025
S : Type ?u.15028
M : Type u_1
M₂ : Type ?u.15034
M₃ : Type ?u.15037
ι : Type ?u.15040
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r s : R
x y : M
⊢ 2 • x = x + x
rw [← one_add_one_eq_two, add_smul, one_smul]