-- Lean 4 proof step from Mathlib.Geometry.Euclidean.MongePoint (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P (n + 2)
i₁ i₂ : Fin (n + 3)
h : ¬i₁ = i₂
hs :
  Eq (α := ℝ)
    (∑ i : PointsWithCircumcenterIndex (n + 2), (pointWeightsWithCircumcenter i₁ - pointWeightsWithCircumcenter i₂) i) 0
fs : Finset (Fin (n + 3)) := {i₁, i₂}
hfs : ∀ i ∉ fs, i ≠ i₁ ∧ i ≠ i₂
neg :
  -(∑ x ∈ fs,
                (if True ∨ i₁ = i₂ then (↑(n + 1) : ℝ)⁻¹ else 0) *
                    HSub.hSub (α := ℝ) (if x = i₁ then 1 else 0) (if x = i₂ then 1 else 0) *
                  (dist (s.points i₁) (s.points x) * dist (s.points i₁) (s.points x)) +
              (if True ∨ i₁ = i₂ then (↑(n + 1) : ℝ)⁻¹ else 0) * HSub.hSub (α := ℝ) 0 0 *
                (dist (s.points i₁) s.circumcenter * dist (s.points i₁) s.circumcenter) +
            (∑ x : Fin (n + 2 + 1),
                (if i₂ = i₁ ∨ True then (↑(n + 1) : ℝ)⁻¹ else 0) *
                    HSub.hSub (α := ℝ) (if x = i₁ then 1 else 0) (if x = i₂ then 1 else 0) *
                  (dist (s.points i₂) (s.points x) * dist (s.points i₂) (s.points x)) +
              (if i₂ = i₁ ∨ True then (↑(n + 1) : ℝ)⁻¹ else 0) * HSub.hSub (α := ℝ) 0 0 *
                (dist (s.points i₂) s.circumcenter * dist (s.points i₂) s.circumcenter)) +
          (HDiv.hDiv (α := ℝ) (-2) (↑(n + 1) : ℝ) *
                  HSub.hSub (α := ℝ) (if True then 1 else 0) (if i₁ = i₂ then 1 else 0) *
                (dist s.circumcenter (s.points i₁) * dist s.circumcenter (s.points i₁)) +
              HDiv.hDiv (α := ℝ) (-2) (↑(n + 1) : ℝ) *
                  HSub.hSub (α := ℝ) (if i₂ = i₁ then 1 else 0) (if True then 1 else 0) *
                (dist s.circumcenter (s.points i₂) * dist s.circumcenter (s.points i₂)) +
            HDiv.hDiv (α := ℝ) (-2) (↑(n + 1) : ℝ) * HSub.hSub (α := ℝ) 0 0 *
              (dist s.circumcenter s.circumcenter * dist s.circumcenter s.circumcenter))) /
      2 =
    0
⊢ -(∑ x : Fin (n + 2 + 1),
                (if True ∨ i₁ = i₂ then (↑(n + 1) : ℝ)⁻¹ else 0) *
                    HSub.hSub (α := ℝ) (if x = i₁ then 1 else 0) (if x = i₂ then 1 else 0) *
                  (dist (s.points i₁) (s.points x) * dist (s.points i₁) (s.points x)) +
              (if True ∨ i₁ = i₂ then (↑(n + 1) : ℝ)⁻¹ else 0) * HSub.hSub (α := ℝ) 0 0 *
                (dist (s.points i₁) s.circumcenter * dist (s.points i₁) s.circumcenter) +
            (∑ x : Fin (n + 2 + 1),
                (if i₂ = i₁ ∨ True then (↑(n + 1) : ℝ)⁻¹ else 0) *
                    HSub.hSub (α := ℝ) (if x = i₁ then 1 else 0) (if x = i₂ then 1 else 0) *
                  (dist (s.points i₂) (s.points x) * dist (s.points i₂) (s.points x)) +
              (if i₂ = i₁ ∨ True then (↑(n + 1) : ℝ)⁻¹ else 0) * HSub.hSub (α := ℝ) 0 0 *
                (dist (s.points i₂) s.circumcenter * dist (s.points i₂) s.circumcenter)) +
          (HDiv.hDiv (α := ℝ) (-2) (↑(n + 1) : ℝ) *
                  HSub.hSub (α := ℝ) (if True then 1 else 0) (if i₁ = i₂ then 1 else 0) *
                (dist s.circumcenter (s.points i₁) * dist s.circumcenter (s.points i₁)) +
              HDiv.hDiv (α := ℝ) (-2) (↑(n + 1) : ℝ) *
                  HSub.hSub (α := ℝ) (if i₂ = i₁ then 1 else 0) (if True then 1 else 0) *
                (dist s.circumcenter (s.points i₂) * dist s.circumcenter (s.points i₂)) +
            HDiv.hDiv (α := ℝ) (-2) (↑(n + 1) : ℝ) * HSub.hSub (α := ℝ) 0 0 *
              (dist s.circumcenter s.circumcenter * dist s.circumcenter s.circumcenter))) /
      2 =
    0
have rw : ∀ (x : Fin (n + 3)),
  Membership.mem (γ := Finset (Fin (n + 3))) univ x →
    x ∉ fs →
      (if True ∨ i₁ = i₂ then (↑(n + 1) : ℝ)⁻¹ else 0) *
            HSub.hSub (α := ℝ) (if x = i₁ then 1 else 0) (if x = i₂ then 1 else 0) *
          (dist (s.points i₁) (s.points x) * dist (s.points i₁) (s.points x)) =
        0
Tactic: rw [← sum_subset fs.subset_univ _]