refine' ⟨w, fun y hy => _, hw₂, hw₃⟩
𝕜 : 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
hw₃ : s.centerMass w id = x
q : ∀ (x_1 : E → 𝕜), (∀ y ∈ s, 0 ≤ x_1 y) → ∑ y ∈ s, x_1 y = 1 → ∀ x_4 ∈ s, x_1 x_4 = 0 → ¬s.centerMass x_1 id = x
⊢ ∃ w, ∃ (_ : ∀ y ∈ s, 0 < w y) (_ : ∑ y ∈ s, w y = 1), s.centerMass w id = x
𝕜 : 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
hw₃ : s.centerMass w id = x
q : ∀ (x_1 : E → 𝕜), (∀ y ∈ s, 0 ≤ x_1 y) → ∑ y ∈ s, x_1 y = 1 → ∀ x_4 ∈ s, x_1 x_4 = 0 → ¬s.centerMass x_1 id = x
y : E
hy : y ∈ s
⊢ 0 < w y