R : Type u_2
E : Type u_3
F : Type ?u.49319
ι : Type u_1
ι' : Type ?u.49325
α : Type ?u.49328
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
s : Finset ι
w₁ w₂ : ι → R
z : ι → E
hw₁ : ∑ i in s, w₁ i = 1
hw₂ : ∑ i in s, w₂ i = 1
a b : R
hab : a + b = 1
hw : ∑ i in s, (a * w₁ i + b * w₂ i) = 1
⊢ a • centerMass s w₁ z + b • centerMass s w₂ z = centerMass s (fun i => a * w₁ i + b * w₂ i) z
R : Type u_2
E : Type u_3
F : Type ?u.49319
ι : Type u_1
ι' : Type ?u.49325
α : Type ?u.49328
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
s : Finset ι
w₁ w₂ : ι → R
z : ι → E
hw₁ : ∑ i in s, w₁ i = 1
hw₂ : ∑ i in s, w₂ i = 1
a b : R
hab : a + b = 1
⊢ a • centerMass s w₁ z + b • centerMass s w₂ z = centerMass s (fun i => a * w₁ i + b * w₂ i) z
have hw : (∑ i in s, (a * w₁ i + b * w₂ i)) = 1 := by
  simp only [mul_sum.symm, sum_add_distrib, mul_one, *]
no goals
R : Type u_2
E : Type u_3
F : Type ?u.49319
ι : Type u_1
ι' : Type ?u.49325
α : Type ?u.49328
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
s : Finset ι
w₁ w₂ : ι → R
z : ι → E
hw₁ : ∑ i in s, w₁ i = 1
hw₂ : ∑ i in s, w₂ i = 1
a b : R
hab : a + b = 1
hw : ∑ i in s, (a * w₁ i + b * w₂ i) = 1
⊢ a • centerMass s w₁ z + b • centerMass s w₂ z = centerMass s (fun i => a * w₁ i + b * w₂ i) z
simp only [Finset.centerMass_eq_of_sum_1, Finset.centerMass_eq_of_sum_1 _ _ hw,
  smul_sum, sum_add_distrib, add_smul, mul_smul, *]
no goals
R : Type u_2
E : Type u_3
F : Type ?u.49319
ι : Type u_1
ι' : Type ?u.49325
α : Type ?u.49328
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
s : Finset ι
w₁ w₂ : ι → R
z : ι → E
hw₁ : ∑ i in s, w₁ i = 1
hw₂ : ∑ i in s, w₂ i = 1
a b : R
hab : a + b = 1
⊢ ∑ i in s, (a * w₁ i + b * w₂ i) = 1
simp only [mul_sum.symm, sum_add_distrib, mul_one, *]