rfl
case neg
𝕜 : 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
t : Finset E
ts : t ⊂ s
w : E → 𝕜
hw₀ : ∀ y ∈ t, 0 ≤ w y
hw₁ : ∑ y ∈ t, w y = 1
hx : t.centerMass w id = x
y✝ : E
hys : y✝ ∈ s
hyt : y✝ ∉ t
w' : E → 𝕜 := fun z => if z ∈ t then w z else 0
hw'₁ : s.sum w' = 1
y : E
h✝ : y ∉ t
⊢ 0 ≤ 0
no goals