-- Mathlib/Geometry/Euclidean/MongePoint.lean
theorem inner_mongePoint_vsub_face_centroid_vsub {n : ℕ} (s : Simplex ℝ P (n + 2))
    {i₁ i₂ : Fin (n + 3)} :
    ⟪s.mongePoint -ᵥ ({i₁, i₂}ᶜ : Finset (Fin (n + 3))).centroid ℝ s.points,
        s.points i₁ -ᵥ s.points i₂⟫ =
      0

Proof state:
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)
⊢ inner (s.mongePoint -ᵥ centroid ℝ {i₁, i₂}ᶜ s.points) (s.points i₁ -ᵥ s.points i₂) = 0

Tactic:
by_cases h : i₁ = i₂

Result:
case pos
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₂
⊢ inner (s.mongePoint -ᵥ centroid ℝ {i₁, i₂}ᶜ s.points) (s.points i₁ -ᵥ s.points i₂) = 0

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₂
⊢ inner (s.mongePoint -ᵥ centroid ℝ {i₁, i₂}ᶜ s.points) (s.points i₁ -ᵥ s.points i₂) = 0

Proof state:
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 : PointsWithCircumcenterIndex (n + 2), (pointWeightsWithCircumcenter i₁ - pointWeightsWithCircumcenter i₂) i = 0
⊢ -(∑ x : Fin (n + 2 + 1),
            ∑ x_1 : PointsWithCircumcenterIndex (n + 2),
              (if x = i₁ ∨ x = i₂ then (↑(n + 1))⁻¹ else 0) *
                  (pointWeightsWithCircumcenter i₁ - pointWeightsWithCircumcenter i₂) x_1 *
                (dist (s.points x) (s.pointsWithCircumcenter x_1) * dist (s.points x) (s.pointsWithCircumcenter x_1)) +
          ∑ x : PointsWithCircumcenterIndex (n + 2),
            -2 / ↑(n + 1) * (pointWeightsWithCircumcenter i₁ - pointWeightsWithCircumcenter i₂) x *
              (dist s.circumcenter (s.pointsWithCircumcenter x) * dist s.circumcenter (s.pointsWithCircumcenter x))) /
      2 =
    0

Tactic:
let fs : Finset (Fin (n + 3)) := {i₁, i₂}

Result:
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 : PointsWithCircumcenterIndex (n + 2), (pointWeightsWithCircumcenter i₁ - pointWeightsWithCircumcenter i₂) i = 0
fs : Finset (Fin (n + 3)) := {i₁, i₂}
⊢ -(∑ x : Fin (n + 2 + 1),
            ∑ x_1 : PointsWithCircumcenterIndex (n + 2),
              (if x = i₁ ∨ x = i₂ then (↑(n + 1))⁻¹ else 0) *
                  (pointWeightsWithCircumcenter i₁ - pointWeightsWithCircumcenter i₂) x_1 *
                (dist (s.points x) (s.pointsWithCircumcenter x_1) * dist (s.points x) (s.pointsWithCircumcenter x_1)) +
          ∑ x : PointsWithCircumcenterIndex (n + 2),
            -2 / ↑(n + 1) * (pointWeightsWithCircumcenter i₁ - pointWeightsWithCircumcenter i₂) x *
              (dist s.circumcenter (s.pointsWithCircumcenter x) * dist s.circumcenter (s.pointsWithCircumcenter x))) /
      2 =
    0

Proof state:
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 : PointsWithCircumcenterIndex (n + 2), (pointWeightsWithCircumcenter i₁ - pointWeightsWithCircumcenter i₂) i = 0
fs : Finset (Fin (n + 3)) := {i₁, i₂}
hfs : ∀ i ∉ fs, i ≠ i₁ ∧ i ≠ i₂
i : Fin (n + 3)
a✝ : i ∈ univ
hi : i ∉ fs
⊢ (if True ∨ i₁ = i₂ then (↑(n + 1))⁻¹ else 0) * ((if i = i₁ then 1 else 0) - if i = i₂ then 1 else 0) *
      (dist (s.points i₁) (s.points i) * dist (s.points i₁) (s.points i)) =
    0

Tactic:
simp [hfs i hi]

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
n : ℕ
s : Simplex ℝ P (n + 2)
i₁ i₂ : Fin (n + 3)
h : ¬i₁ = i₂
⊢ ∑ i : PointsWithCircumcenterIndex (n + 2), (pointWeightsWithCircumcenter i₁ - pointWeightsWithCircumcenter i₂) i = 0

Tactic:
simp

Result:
no goals

Proof state:
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 : PointsWithCircumcenterIndex (n + 2), (pointWeightsWithCircumcenter i₁ - pointWeightsWithCircumcenter i₂) i = 0
fs : Finset (Fin (n + 3)) := {i₁, i₂}
hfs : ∀ i ∉ fs, i ≠ i₁ ∧ i ≠ i₂
⊢ -(∑ x ∈ fs,
            ∑ x_1 : PointsWithCircumcenterIndex (n + 2),
              (if x = i₁ ∨ x = i₂ then (↑(n + 1))⁻¹ else 0) *
                  (pointWeightsWithCircumcenter i₁ - pointWeightsWithCircumcenter i₂) x_1 *
                (dist (s.points x) (s.pointsWithCircumcenter x_1) * dist (s.points x) (s.pointsWithCircumcenter x_1)) +
          ∑ x : PointsWithCircumcenterIndex (n + 2),
            -2 / ↑(n + 1) * (pointWeightsWithCircumcenter i₁ - pointWeightsWithCircumcenter i₂) x *
              (dist s.circumcenter (s.pointsWithCircumcenter x) * dist s.circumcenter (s.pointsWithCircumcenter x))) /
      2 =
    0

Tactic:
simp_rw [sum_pointsWithCircumcenter, pointsWithCircumcenter_eq_circumcenter,
  pointsWithCircumcenter_point, Pi.sub_apply, pointWeightsWithCircumcenter]

Result:
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 : PointsWithCircumcenterIndex (n + 2), (pointWeightsWithCircumcenter i₁ - pointWeightsWithCircumcenter i₂) i = 0
fs : Finset (Fin (n + 3)) := {i₁, i₂}
hfs : ∀ i ∉ fs, i ≠ i₁ ∧ i ≠ i₂
⊢ -(∑ x ∈ fs,
            (∑ x_1 : Fin (n + 2 + 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 : Fin (n + 2 + 1),
              -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

Proof state:
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 : PointsWithCircumcenterIndex (n + 2), (pointWeightsWithCircumcenter i₁ - pointWeightsWithCircumcenter i₂) i = 0
fs : Finset (Fin (n + 3)) := {i₁, i₂}
hfs : ∀ i ∉ fs, i ≠ i₁ ∧ i ≠ i₂
i : Fin (n + 3)
a✝ : i ∈ univ
hi : i ∉ fs
⊢ ∑ x : PointsWithCircumcenterIndex (n + 2),
      (if i = i₁ ∨ i = i₂ then (↑(n + 1))⁻¹ else 0) *
          (pointWeightsWithCircumcenter i₁ - pointWeightsWithCircumcenter i₂) x *
        (dist (s.points i) (s.pointsWithCircumcenter x) * dist (s.points i) (s.pointsWithCircumcenter x)) =
    0

Tactic:
simp [hfs i hi]

Result:
no goals