no goals
R : Type u_1
E : Type u_3
F : Type ?u.30257
ι : Type u_2
ι' : Type ?u.30263
α : Type ?u.30266
inst✝⁷ : LinearOrderedField R
inst✝⁶ : AddCommGroup E
inst✝⁵ : AddCommGroup F
inst✝⁴ : LinearOrderedAddCommGroup α
inst✝³ : Module R E
inst✝² : Module R F
inst✝¹ : Module R α
inst✝ : OrderedSMul R α
s : Set E
i j : ι
c : R
t : Finset ι
w : ι → R
z : ι → E
hw : ∑ i in t, w i = 1
⊢ centerMass t w z = ∑ i in t, w i • z i
simp only [Finset.centerMass, hw, inv_one, one_smul]