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,
            (∑ x_1,
                (if x = i₁ ∨ x = i₂ then (↑(n + 1))⁻¹ else 0) *
                    ((if x_1 = i₁ then 1 else 0) - if x_1 = i₂ then 1 else 0) *
                  (dist (s.points x) (s.points x_1) * dist (s.points x) (s.points x_1)) +
              (if x = i₁ ∨ x = i₂ then (↑(n + 1))⁻¹ else 0) * (0 - 0) *
                (dist (s.points x) s.circumcenter * dist (s.points x) s.circumcenter)) +
          (∑ x ∈ fs,
              -2 / ↑(n + 1) * ((if x = i₁ then 1 else 0) - if x = i₂ then 1 else 0) *
                (dist s.circumcenter (s.points x) * dist s.circumcenter (s.points x)) +
            -2 / ↑(n + 1) * (0 - 0) * (dist s.circumcenter s.circumcenter * dist s.circumcenter s.circumcenter))) /
      2 =
    0

pp: 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 ∈ univ,
    x ∉ fs →
      -2 / ↑(n + 1) * ((if x = i₁ then 1 else 0) - if x = i₂ then 1 else 0) *
          (dist s.circumcenter (s.points x) * dist s.circumcenter (s.points x)) =
        0

Tactic:
]

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,
            (∑ x_1,
                (if x = i₁ ∨ x = i₂ then (↑(n + 1))⁻¹ else 0) *
                    ((if x_1 = i₁ then 1 else 0) - if x_1 = i₂ then 1 else 0) *
                  (dist (s.points x) (s.points x_1) * dist (s.points x) (s.points x_1)) +
              (if x = i₁ ∨ x = i₂ then (↑(n + 1))⁻¹ else 0) * (0 - 0) *
                (dist (s.points x) s.circumcenter * dist (s.points x) s.circumcenter)) +
          (∑ x ∈ fs,
              -2 / ↑(n + 1) * ((if x = i₁ then 1 else 0) - if x = i₂ then 1 else 0) *
                (dist s.circumcenter (s.points x) * dist s.circumcenter (s.points x)) +
            -2 / ↑(n + 1) * (0 - 0) * (dist s.circumcenter s.circumcenter * dist s.circumcenter s.circumcenter))) /
      2 =
    0

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 ∈ univ,
    x ∉ fs →
      -2 / ↑(n + 1) * ((if x = i₁ then 1 else 0) - if x = i₂ then 1 else 0) *
          (dist s.circumcenter (s.points x) * dist s.circumcenter (s.points x)) =
        0