no goals
R : Type u_2
E : Type u_1
F : Type ?u.407254
ι : Type ?u.407257
ι' : Type ?u.407260
α : Type ?u.407263
inst✝⁷ : LinearOrderedField R
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup F
inst✝⁴ : LinearOrderedAddCommGroup α
inst✝³ : Module R E
inst✝² : Module R F
inst✝¹ : Module R α
inst✝ : OrderedSMul R α
s✝ : Set E
i j : ι
c : R
t✝ : Finset ι
w : ι → R
z : ι → E
s t : Set E
⊢ ↑(convexHull R).toOrderHom (s + t) = ↑(convexHull R).toOrderHom s + ↑(convexHull R).toOrderHom t
simp_rw [← image2_add, ← image_prod, IsLinearMap.isLinearMap_add.convexHull_image,
  convexHull_prod]