no goals
𝕜 : Type u_1
E : Type u_2
F : Type ?u.724295
α : Type ?u.724298
β : Type u_3
ι : Type ?u.724304
inst✝⁵ : OrderedCommSemiring 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : OrderedAddCommMonoid β
inst✝² : SMul 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
c : 𝕜
hc : 0 ≤ c
hf : ConvexOn 𝕜 s f
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ c • (a • f x + b • f y) = a • c • f x + b • c • f y
rw [smul_add, smul_comm c, smul_comm c]