apply if_neg ‹y ∉ t›
case h.mp.intro.intro.intro.intro.intro.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
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
⊢ w' y = 0
no goals