apply hy₂
case h.mpr.refine'_2
𝕜 : 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
hy₃ : s.centerMass w id = x
i : E
hi₁ hy₁ : i ∈ s
hy₂ : w i = 0
⊢ w i = 0
no goals