simp only [and_imp, exists_prop, exists_imp]
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, ∃ (_ : ∀ y ∈ s, 0 ≤ w y) (_ : ∑ y ∈ s, w y = 1) (_ : ∃ y ∈ s, w y = 0), s.centerMass w id = x) →
    ∃ i, ∃ (_ : 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
⊢ ∀ (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