R : Type u_2
E : Type u_3
F : Type ?u.18158
ι : Type u_1
ι' : Type ?u.18164
α : Type ?u.18167
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
ha : ¬i ∈ t
hw : ∑ j in t, w j ≠ 0
⊢ (w i / (w i + ∑ i in t, w i)) • z i + (w i + ∑ i in t, w i)⁻¹ • ∑ i in t, w i • z i =
    (w i / (w i + ∑ i in t, w i)) • z i +
      ((∑ i in t, w i) / (w i + ∑ i in t, w i) * (∑ i in t, w i)⁻¹) • ∑ i in t, w i • z i
R : Type u_2
E : Type u_3
F : Type ?u.18158
ι : Type u_1
ι' : Type ?u.18164
α : Type ?u.18167
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
ha : ¬i ∈ t
hw : ∑ j in t, w j ≠ 0
⊢ centerMass (insert i t) w z =
    (w i / (w i + ∑ j in t, w j)) • z i + ((∑ j in t, w j) / (w i + ∑ j in t, w j)) • centerMass t w z
simp only [centerMass, sum_insert ha, smul_add, (mul_smul _ _ _).symm, ← div_eq_inv_mul]
case e_a.e_a
R : Type u_2
E : Type u_3
F : Type ?u.18158
ι : Type u_1
ι' : Type ?u.18164
α : Type ?u.18167
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
ha : ¬i ∈ t
hw : ∑ j in t, w j ≠ 0
⊢ (w i + ∑ i in t, w i)⁻¹ = (∑ i in t, w i) / (w i + ∑ i in t, w i) * (∑ i in t, w i)⁻¹
R : Type u_2
E : Type u_3
F : Type ?u.18158
ι : Type u_1
ι' : Type ?u.18164
α : Type ?u.18167
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
ha : ¬i ∈ t
hw : ∑ j in t, w j ≠ 0
⊢ (w i / (w i + ∑ i in t, w i)) • z i + (w i + ∑ i in t, w i)⁻¹ • ∑ i in t, w i • z i =
    (w i / (w i + ∑ i in t, w i)) • z i +
      ((∑ i in t, w i) / (w i + ∑ i in t, w i) * (∑ i in t, w i)⁻¹) • ∑ i in t, w i • z i
congr 2
no goals
case e_a.e_a
R : Type u_2
E : Type u_3
F : Type ?u.18158
ι : Type u_1
ι' : Type ?u.18164
α : Type ?u.18167
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
ha : ¬i ∈ t
hw : ∑ j in t, w j ≠ 0
⊢ (w i + ∑ i in t, w i)⁻¹ = (∑ i in t, w i) / (w i + ∑ i in t, w i) * (∑ i in t, w i)⁻¹
rw [div_mul_eq_mul_div, mul_inv_cancel hw, one_div]