no goals
α : Type ?u.11520
R : Type u_1
k : Type ?u.11526
S : Type ?u.11529
M : Type u_2
M₂ : Type ?u.11535
M₃ : Type ?u.11538
ι : Type ?u.11541
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r s : R
x✝ y : M
a b : R
h : a + b = 1
x : M
⊢ a • x + b • x = x
rw [← add_smul, h, one_smul]