apply hw₂
case h.mpr.refine'_1
𝕜 : 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
y : E
hy₁ : y ∈ s
hy₂ : w y = 0
hy₃ : s.centerMass w id = x
⊢ ∑ x ∈ s, w x = 1

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
y : E
hy₁ : y ∈ s
hy₂ : w y = 0
hy₃ : s.centerMass w id = x
⊢ (s.erase y).centerMass w id = x
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
y : E
hy₁ : y ∈ s
hy₂ : w y = 0
hy₃ : s.centerMass w id = x
⊢ (s.erase y).centerMass w id = x