no goals
𝕜 : Type u_1
E : Type u_2
F : Type ?u.117268
α : Type ?u.117271
β : Type u_3
ι : Type ?u.117277
inst✝⁶ : OrderedSemiring 𝕜
inst✝⁵ : AddCommMonoid E
inst✝⁴ : AddCommMonoid F
inst✝³ : OrderedAddCommMonoid α
inst✝² : OrderedAddCommMonoid β
inst✝¹ : Module 𝕜 E
inst✝ : SMul 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
c x : E
hx : x ∈ (fun z => c + z) ⁻¹' s
y : E
hy : y ∈ (fun z => c + z) ⁻¹' s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ f (c + (a • x + b • y)) = f (a • (c + x) + b • (c + y))
rw [smul_add, smul_add, add_add_add_comm, Convex.combo_self hab]