intro w hw₁ hw₂ y hy₁ hy₂ hy₃
case h.mpr
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x✝ x : E
⊢ ∀ (x_1 : E → 𝕜),
    (∀ y ∈ s, 0 ≤ x_1 y) →
      ∑ y ∈ s, x_1 y = 1 → ∀ x_2 ∈ s, x_1 x_2 = 0 → s.centerMass x_1 id = x → ∃ i ⊂ s, x ∈ (convexHull 𝕜) ↑i
case h.mpr
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x✝ x : E
w : E → 𝕜
hw₁ : ∀ y ∈ s, 0 ≤ w y
hw₂ : ∑ y ∈ s, w y = 1
y : E
hy₁ : y ∈ s
hy₂ : w y = 0
hy₃ : s.centerMass w id = x
⊢ ∃ i ⊂ s, x ∈ (convexHull 𝕜) ↑i