rw [Finset.centerMass_segment _ _ _ _ hv₁ hw₁ _ _ h]
case intro.intro.intro.intro.intro.intro.refine'_3
𝕜 : 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
v : E → 𝕜
hv₀ : ∀ y ∈ s, 0 < v y
hv₁ : ∑ y ∈ s, v y = 1
w : E → 𝕜
hw₀ : ∀ y ∈ s, 0 < w y
hw₁ : ∑ y ∈ s, w y = 1
a b : 𝕜
ha : 0 < a
hb : 0 < b
h : a + b = 1
⊢ s.centerMass (fun x => a * v x + b * w x) id = a • s.centerMass v id + b • s.centerMass w id
no goals