rw [Finset.centerMass_eq_of_sum_1 _ _ hv₁, Finset.centerMass_eq_of_sum_1 _ _ hw₁] at hw₂
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x✝ : E
hs : AffineIndependent 𝕜 Subtype.val
x : E
w : E → 𝕜
hw₀ : ∀ y ∈ s, 0 < w y
hw₁ : ∑ y ∈ s, w y = 1
v : E → 𝕜
hw₂ : s.centerMass w id = s.centerMass v id
hv₀ : ∀ y ∈ s, 0 ≤ v y
hv₁ : ∑ y ∈ s, v y = 1
y : E
hy : y ∈ s
hvy : v y = 0
hv₂ : s.centerMass v id = x
⊢ w y = 0
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x✝ : E
hs : AffineIndependent 𝕜 Subtype.val
x : E
w : E → 𝕜
hw₀ : ∀ y ∈ s, 0 < w y
hw₁ : ∑ y ∈ s, w y = 1
v : E → 𝕜
hw₂ : ∑ i ∈ s, w i • id i = ∑ i ∈ s, v i • id i
hv₀ : ∀ y ∈ s, 0 ≤ v y
hv₁ : ∑ y ∈ s, v y = 1
y : E
hy : y ∈ s
hvy : v y = 0
hv₂ : s.centerMass v id = x
⊢ w y = 0