no goals
𝕜 : Type ?u.3253936
E : Type ?u.3253939
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
dec_E : DecidableEq E
ι₁ : Type u_1
s₁ : Finset ι₁
w₁ : ι₁ → ℝ
v₁ : ι₁ → F
h₁ : ∑ i in s₁, w₁ i = 0
ι₂ : Type u_2
s₂ : Finset ι₂
w₂ : ι₂ → ℝ
v₂ : ι₂ → F
h₂ : ∑ i in s₂, w₂ i = 0
⊢ inner (∑ i₁ in s₁, w₁ i₁ • v₁ i₁) (∑ i₂ in s₂, w₂ i₂ • v₂ i₂) =
    (-∑ i₁ in s₁, ∑ i₂ in s₂, w₁ i₁ * w₂ i₂ * (‖v₁ i₁ - v₂ i₂‖ * ‖v₁ i₁ - v₂ i₂‖)) / 2
simp_rw [sum_inner, inner_sum, real_inner_smul_left, real_inner_smul_right,
  real_inner_eq_norm_mul_self_add_norm_mul_self_sub_norm_sub_mul_self_div_two, ← div_sub_div_same,
  ← div_add_div_same, mul_sub_left_distrib, left_distrib, Finset.sum_sub_distrib,
  Finset.sum_add_distrib, ← Finset.mul_sum, ← Finset.sum_mul, h₁, h₂, MulZeroClass.zero_mul,
  MulZeroClass.mul_zero, Finset.sum_const_zero, zero_add, zero_sub, Finset.mul_sum, neg_div,
  Finset.sum_div, mul_div_assoc, mul_assoc]