no goals
R : Type u_2
E : Type u_1
F : Type ?u.232358
ι : Type ?u.232361
ι' : Type ?u.232364
α : Type ?u.232367
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 : Finset E
x : E
⊢ x ∈ ↑(convexHull R).toOrderHom ↑s ↔ ∃ w x_1 x_2, centerMass s w id = x
rw [Finset.convexHull_eq, Set.mem_setOf_eq]