Module: Mathlib.Geometry.Euclidean.MongePoint

Goal state before:
pp: case neg
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P (n + 2)
i₁ i₂ : Fin (n + 3)
h : ¬i₁ = i₂
hs : ∑ i, (pointWeightsWithCircumcenter i₁ - pointWeightsWithCircumcenter i₂) i = 0
fs : Finset (Fin (n + 3)) := {i₁, i₂}
hfs : ∀ i ∉ fs, i ≠ i₁ ∧ i ≠ i₂
⊢ -(∑ x ∈ fs,
            (∑ i,
                (if x = i₁ ∨ x = i₂ then (↑(n + 1))⁻¹ else 0) *
                    (pointWeightsWithCircumcenter i₁ - pointWeightsWithCircumcenter i₂) (pointIndex i) *
                  (dist (s.points x) (s.pointsWithCircumcenter (pointIndex i)) *
                    dist (s.points x) (s.pointsWithCircumcenter (pointIndex i))) +
              (if x = i₁ ∨ x = i₂ then (↑(n + 1))⁻¹ else 0) *
                  (pointWeightsWithCircumcenter i₁ - pointWeightsWithCircumcenter i₂) circumcenterIndex *
                (dist (s.points x) (s.pointsWithCircumcenter circumcenterIndex) *
                  dist (s.points x) (s.pointsWithCircumcenter circumcenterIndex))) +
          (∑ i,
              -2 / ↑(n + 1) * (pointWeightsWithCircumcenter i₁ - pointWeightsWithCircumcenter i₂) (pointIndex i) *
                (dist s.circumcenter (s.pointsWithCircumcenter (pointIndex i)) *
                  dist s.circumcenter (s.pointsWithCircumcenter (pointIndex i))) +
            -2 / ↑(n + 1) * (pointWeightsWithCircumcenter i₁ - pointWeightsWithCircumcenter i₂) circumcenterIndex *
              (dist s.circumcenter (s.pointsWithCircumcenter circumcenterIndex) *
                dist s.circumcenter (s.pointsWithCircumcenter circumcenterIndex)))) /
      2 =
    0

Tactic:
pointsWithCircumcenter_eq_circumcenter,

Goal state after:
case neg
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P (n + 2)
i₁ i₂ : Fin (n + 3)
h : ¬i₁ = i₂
hs : ∑ i, (pointWeightsWithCircumcenter i₁ - pointWeightsWithCircumcenter i₂) i = 0
fs : Finset (Fin (n + 3)) := {i₁, i₂}
hfs : ∀ i ∉ fs, i ≠ i₁ ∧ i ≠ i₂
⊢ -(∑ x ∈ fs,
            (∑ i,
                (if x = i₁ ∨ x = i₂ then (↑(n + 1))⁻¹ else 0) *
                    (pointWeightsWithCircumcenter i₁ - pointWeightsWithCircumcenter i₂) (pointIndex i) *
                  (dist (s.points x) (s.pointsWithCircumcenter (pointIndex i)) *
                    dist (s.points x) (s.pointsWithCircumcenter (pointIndex i))) +
              (if x = i₁ ∨ x = i₂ then (↑(n + 1))⁻¹ else 0) *
                  (pointWeightsWithCircumcenter i₁ - pointWeightsWithCircumcenter i₂) circumcenterIndex *
                (dist (s.points x) s.circumcenter * dist (s.points x) s.circumcenter)) +
          (∑ i,
              -2 / ↑(n + 1) * (pointWeightsWithCircumcenter i₁ - pointWeightsWithCircumcenter i₂) (pointIndex i) *
                (dist s.circumcenter (s.pointsWithCircumcenter (pointIndex i)) *
                  dist s.circumcenter (s.pointsWithCircumcenter (pointIndex i))) +
            -2 / ↑(n + 1) * (pointWeightsWithCircumcenter i₁ - pointWeightsWithCircumcenter i₂) circumcenterIndex *
              (dist s.circumcenter s.circumcenter * dist s.circumcenter s.circumcenter))) /
      2 =
    0