no goals
α : Type ?u.85204
R : Type u_1
k : Type ?u.85210
S : Type ?u.85213
M : Type u_2
M₂ : Type ?u.85219
M₃ : Type ?u.85222
ι : Type ?u.85225
inst✝² : Semiring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
a b : R
h : a + b = 1
⊢ a • x + b • y = b • y - b • x + (a • x + b • x)
abel
no goals
α : Type ?u.85204
R : Type u_1
k : Type ?u.85210
S : Type ?u.85213
M : Type u_2
M₂ : Type ?u.85219
M₃ : Type ?u.85222
ι : Type ?u.85225
inst✝² : Semiring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x y : M
a b : R
h : a + b = 1
⊢ b • y - b • x + (a • x + b • x) = b • (y - x) + x
rw [smul_sub, Convex.combo_self h]