-- Mathlib/Geometry/Euclidean/Basic.lean
theorem inner_weightedVSub {ι₁ : Type*} {s₁ : Finset ι₁} {w₁ : ι₁ → ℝ} (p₁ : ι₁ → P)
    (h₁ : ∑ i ∈ s₁, w₁ i = 0) {ι₂ : Type*} {s₂ : Finset ι₂} {w₂ : ι₂ → ℝ} (p₂ : ι₂ → P)
    (h₂ : ∑ i ∈ s₂, w₂ i = 0) :
    ⟪s₁.weightedVSub p₁ w₁, s₂.weightedVSub p₂ w₂⟫ =
      (-∑ i₁ ∈ s₁, ∑ i₂ ∈ s₂, w₁ i₁ * w₂ i₂ * (dist (p₁ i₁) (p₂ i₂) * dist (p₁ i₁) (p₂ i₂))) /
        2

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
ι₁ : Type u_3
s₁ : Finset ι₁
w₁ : ι₁ → ℝ
p₁ : ι₁ → P
h₁ : ∑ i ∈ s₁, w₁ i = 0
ι₂ : Type u_4
s₂ : Finset ι₂
w₂ : ι₂ → ℝ
p₂ : ι₂ → P
h₂ : ∑ i ∈ s₂, w₂ i = 0
⊢ (-∑ x ∈ s₁, ∑ x_1 ∈ s₂, w₁ x * w₂ x_1 * (‖p₁ x -ᵥ p₂ x_1‖ * ‖p₁ x -ᵥ p₂ x_1‖)) / 2 =
    (-∑ i₁ ∈ s₁, ∑ i₂ ∈ s₂, w₁ i₁ * w₂ i₂ * (dist (p₁ i₁) (p₂ i₂) * dist (p₁ i₁) (p₂ i₂))) / 2

Tactic:
rcongr (i₁ i₂) <;> rw [dist_eq_norm_vsub V (p₁ i₁) (p₂ i₂)]

Result:
no goals

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
ι₁ : Type u_3
s₁ : Finset ι₁
w₁ : ι₁ → ℝ
p₁ : ι₁ → P
h₁ : ∑ i ∈ s₁, w₁ i = 0
ι₂ : Type u_4
s₂ : Finset ι₂
w₂ : ι₂ → ℝ
p₂ : ι₂ → P
h₂ : ∑ i ∈ s₂, w₂ i = 0
⊢ inner ((s₁.weightedVSub p₁) w₁) ((s₂.weightedVSub p₂) w₂) =
    (-∑ i₁ ∈ s₁, ∑ i₂ ∈ s₂, w₁ i₁ * w₂ i₂ * (dist (p₁ i₁) (p₂ i₂) * dist (p₁ i₁) (p₂ i₂))) / 2

Tactic:
rw [Finset.weightedVSub_apply, Finset.weightedVSub_apply,
  inner_sum_smul_sum_smul_of_sum_eq_zero _ h₁ _ h₂]

Result:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
ι₁ : Type u_3
s₁ : Finset ι₁
w₁ : ι₁ → ℝ
p₁ : ι₁ → P
h₁ : ∑ i ∈ s₁, w₁ i = 0
ι₂ : Type u_4
s₂ : Finset ι₂
w₂ : ι₂ → ℝ
p₂ : ι₂ → P
h₂ : ∑ i ∈ s₂, w₂ i = 0
⊢ (-∑ i₁ ∈ s₁,
          ∑ i₂ ∈ s₂,
            w₁ i₁ * w₂ i₂ *
              (‖p₁ i₁ -ᵥ Classical.choice ⋯ - (p₂ i₂ -ᵥ Classical.choice ⋯)‖ *
                ‖p₁ i₁ -ᵥ Classical.choice ⋯ - (p₂ i₂ -ᵥ Classical.choice ⋯)‖)) /
      2 =
    (-∑ i₁ ∈ s₁, ∑ i₂ ∈ s₂, w₁ i₁ * w₂ i₂ * (dist (p₁ i₁) (p₂ i₂) * dist (p₁ i₁) (p₂ i₂))) / 2

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
ι₁ : Type u_3
s₁ : Finset ι₁
w₁ : ι₁ → ℝ
p₁ : ι₁ → P
h₁ : ∑ i ∈ s₁, w₁ i = 0
ι₂ : Type u_4
s₂ : Finset ι₂
w₂ : ι₂ → ℝ
p₂ : ι₂ → P
h₂ : ∑ i ∈ s₂, w₂ i = 0
⊢ (-∑ i₁ ∈ s₁,
          ∑ i₂ ∈ s₂,
            w₁ i₁ * w₂ i₂ *
              (‖p₁ i₁ -ᵥ Classical.choice ⋯ - (p₂ i₂ -ᵥ Classical.choice ⋯)‖ *
                ‖p₁ i₁ -ᵥ Classical.choice ⋯ - (p₂ i₂ -ᵥ Classical.choice ⋯)‖)) /
      2 =
    (-∑ i₁ ∈ s₁, ∑ i₂ ∈ s₂, w₁ i₁ * w₂ i₂ * (dist (p₁ i₁) (p₂ i₂) * dist (p₁ i₁) (p₂ i₂))) / 2

Tactic:
simp_rw [vsub_sub_vsub_cancel_right]

Result:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
ι₁ : Type u_3
s₁ : Finset ι₁
w₁ : ι₁ → ℝ
p₁ : ι₁ → P
h₁ : ∑ i ∈ s₁, w₁ i = 0
ι₂ : Type u_4
s₂ : Finset ι₂
w₂ : ι₂ → ℝ
p₂ : ι₂ → P
h₂ : ∑ i ∈ s₂, w₂ i = 0
⊢ (-∑ x ∈ s₁, ∑ x_1 ∈ s₂, w₁ x * w₂ x_1 * (‖p₁ x -ᵥ p₂ x_1‖ * ‖p₁ x -ᵥ p₂ x_1‖)) / 2 =
    (-∑ i₁ ∈ s₁, ∑ i₂ ∈ s₂, w₁ i₁ * w₂ i₂ * (dist (p₁ i₁) (p₂ i₂) * dist (p₁ i₁) (p₂ i₂))) / 2