R : Type u_2
E : Type u_3
F : Type ?u.126038
ι✝ : Type ?u.126041
ι' : Type ?u.126044
α : Type ?u.126047
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
ι : Type u_1
t : Finset ι
p : ι → E
w : ι → R
hw₂ : ∑ i in t, w i = 1
⊢ ∑ i in t, w i • (p i -ᵥ 0) = ∑ i in t, w i • p i
R : Type u_2
E : Type u_3
F : Type ?u.126038
ι✝ : Type ?u.126041
ι' : Type ?u.126044
α : Type ?u.126047
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
ι : Type u_1
t : Finset ι
p : ι → E
w : ι → R
hw₂ : ∑ i in t, w i = 1
⊢ ↑(affineCombination R t p) w = centerMass t w p
rw [affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one _ w _ hw₂ (0 : E),
  Finset.weightedVSubOfPoint_apply, vadd_eq_add, add_zero, t.centerMass_eq_of_sum_1 _ hw₂]
no goals
R : Type u_2
E : Type u_3
F : Type ?u.126038
ι✝ : Type ?u.126041
ι' : Type ?u.126044
α : Type ?u.126047
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
ι : Type u_1
t : Finset ι
p : ι → E
w : ι → R
hw₂ : ∑ i in t, w i = 1
⊢ ∑ i in t, w i • (p i -ᵥ 0) = ∑ i in t, w i • p i
simp_rw [vsub_eq_sub, sub_zero]