V : Type u_3
P : Type u_4
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
ι₁ : Type u_1
s₁ : Finset ι₁
w₁ : ι₁ → ℝ
p₁ : ι₁ → P
h₁ : ∑ i in s₁, w₁ i = 0
ι₂ : Type u_2
s₂ : Finset ι₂
w₂ : ι₂ → ℝ
p₂ : ι₂ → P
h₂ : ∑ i in s₂, w₂ i = 0
⊢ (-∑ i₁ in s₁,
          ∑ i₂ in s₂,
            w₁ i₁ * w₂ i₂ *
              (‖p₁ i₁ -ᵥ choice (_ : Nonempty P) - (p₂ i₂ -ᵥ choice (_ : Nonempty P))‖ *
                ‖p₁ i₁ -ᵥ choice (_ : Nonempty P) - (p₂ i₂ -ᵥ choice (_ : Nonempty P))‖)) /
      2 =
    (-∑ i₁ in s₁, ∑ i₂ in s₂, w₁ i₁ * w₂ i₂ * (dist (p₁ i₁) (p₂ i₂) * dist (p₁ i₁) (p₂ i₂))) / 2
V : Type u_3
P : Type u_4
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
ι₁ : Type u_1
s₁ : Finset ι₁
w₁ : ι₁ → ℝ
p₁ : ι₁ → P
h₁ : ∑ i in s₁, w₁ i = 0
ι₂ : Type u_2
s₂ : Finset ι₂
w₂ : ι₂ → ℝ
p₂ : ι₂ → P
h₂ : ∑ i in s₂, w₂ i = 0
⊢ inner (↑(Finset.weightedVSub s₁ p₁) w₁) (↑(Finset.weightedVSub s₂ p₂) w₂) =
    (-∑ i₁ in s₁, ∑ i₂ in s₂, w₁ i₁ * w₂ i₂ * (dist (p₁ i₁) (p₂ i₂) * dist (p₁ i₁) (p₂ i₂))) / 2
rw [Finset.weightedVSub_apply, Finset.weightedVSub_apply,
  inner_sum_smul_sum_smul_of_sum_eq_zero _ h₁ _ h₂]
V : Type u_3
P : Type u_4
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
ι₁ : Type u_1
s₁ : Finset ι₁
w₁ : ι₁ → ℝ
p₁ : ι₁ → P
h₁ : ∑ i in s₁, w₁ i = 0
ι₂ : Type u_2
s₂ : Finset ι₂
w₂ : ι₂ → ℝ
p₂ : ι₂ → P
h₂ : ∑ i in s₂, w₂ i = 0
⊢ (-∑ x in s₁, ∑ x_1 in s₂, w₁ x * w₂ x_1 * (‖p₁ x -ᵥ p₂ x_1‖ * ‖p₁ x -ᵥ p₂ x_1‖)) / 2 =
    (-∑ i₁ in s₁, ∑ i₂ in s₂, w₁ i₁ * w₂ i₂ * (dist (p₁ i₁) (p₂ i₂) * dist (p₁ i₁) (p₂ i₂))) / 2
V : Type u_3
P : Type u_4
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
ι₁ : Type u_1
s₁ : Finset ι₁
w₁ : ι₁ → ℝ
p₁ : ι₁ → P
h₁ : ∑ i in s₁, w₁ i = 0
ι₂ : Type u_2
s₂ : Finset ι₂
w₂ : ι₂ → ℝ
p₂ : ι₂ → P
h₂ : ∑ i in s₂, w₂ i = 0
⊢ (-∑ i₁ in s₁,
          ∑ i₂ in s₂,
            w₁ i₁ * w₂ i₂ *
              (‖p₁ i₁ -ᵥ choice (_ : Nonempty P) - (p₂ i₂ -ᵥ choice (_ : Nonempty P))‖ *
                ‖p₁ i₁ -ᵥ choice (_ : Nonempty P) - (p₂ i₂ -ᵥ choice (_ : Nonempty P))‖)) /
      2 =
    (-∑ i₁ in s₁, ∑ i₂ in s₂, w₁ i₁ * w₂ i₂ * (dist (p₁ i₁) (p₂ i₂) * dist (p₁ i₁) (p₂ i₂))) / 2
simp_rw [vsub_sub_vsub_cancel_right]
no goals
V : Type u_3
P : Type u_4
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
ι₁ : Type u_1
s₁ : Finset ι₁
w₁ : ι₁ → ℝ
p₁ : ι₁ → P
h₁ : ∑ i in s₁, w₁ i = 0
ι₂ : Type u_2
s₂ : Finset ι₂
w₂ : ι₂ → ℝ
p₂ : ι₂ → P
h₂ : ∑ i in s₂, w₂ i = 0
⊢ (-∑ x in s₁, ∑ x_1 in s₂, w₁ x * w₂ x_1 * (‖p₁ x -ᵥ p₂ x_1‖ * ‖p₁ x -ᵥ p₂ x_1‖)) / 2 =
    (-∑ i₁ in s₁, ∑ i₂ in s₂, w₁ i₁ * w₂ i₂ * (dist (p₁ i₁) (p₂ i₂) * dist (p₁ i₁) (p₂ i₂))) / 2
rcongr (i₁ i₂) <;> rw [dist_eq_norm_vsub V (p₁ i₁) (p₂ i₂)]