no goals
R : Type u_2
E : Type u_1
F : Type ?u.235303
ι : Type ?u.235306
ι' : Type ?u.235309
α : Type ?u.235312
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 : Set E
hs : Set.Finite s
⊢ ↑(convexHull R).toOrderHom s = {x | ∃ w x_1 x_2, centerMass (Finite.toFinset hs) w id = x}
simpa only [Set.Finite.coe_toFinset, Set.Finite.mem_toFinset, exists_prop] using
  hs.toFinset.convexHull_eq