-- Module: Mathlib.Geometry.Euclidean.MongePoint
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
t : Triangle ℝ P
i₁ i₂ : Fin 3
h : i₁ ≠ i₂
hu : Subset (α := Finset (Fin 3)) {i₁, i₂} univ
i₃ : Fin 3
hi₃ : Eq (α := Finset (Fin 3)) (univ \ {i₁, i₂}) {i₃}
hi₃₁ : i₃ ≠ i₁
hi₃₂ : i₃ ≠ i₂
simp_rw :
  -(HAdd.hAdd (α := ℝ)
            (∑ x ∈ {i₃},
              (HAdd.hAdd (α := ℝ)
                  (∑ x_1 ∈ {i₃},
                    HSub.hSub (α := ℝ) (↑(HAdd.hAdd (α := ℕ) 0 1) : ℝ)⁻¹ (if x = i₁ ∨ x = i₂ then 1 else 0) *
                        HSub.hSub (α := ℝ) (↑(HAdd.hAdd (α := ℕ) 0 1) : ℝ)⁻¹ (if x_1 = i₁ ∨ x_1 = i₂ then 1 else 0) *
                      (dist (pointsWithCircumcenter t (PointsWithCircumcenterIndex.pointIndex x))
                          (pointsWithCircumcenter t (PointsWithCircumcenterIndex.pointIndex x_1)) *
                        dist (pointsWithCircumcenter t (PointsWithCircumcenterIndex.pointIndex x))
                          (pointsWithCircumcenter t (PointsWithCircumcenterIndex.pointIndex x_1))))
                  (∑ x_1 ∈ {i₁, i₂},
                    HSub.hSub (α := ℝ) (↑(HAdd.hAdd (α := ℕ) 0 1) : ℝ)⁻¹ (if x = i₁ ∨ x = i₂ then 1 else 0) *
                        HSub.hSub (α := ℝ) (↑(HAdd.hAdd (α := ℕ) 0 1) : ℝ)⁻¹ (if x_1 = i₁ ∨ x_1 = i₂ then 1 else 0) *
                      (dist (pointsWithCircumcenter t (PointsWithCircumcenterIndex.pointIndex x))
                          (pointsWithCircumcenter t (PointsWithCircumcenterIndex.pointIndex x_1)) *
                        dist (pointsWithCircumcenter t (PointsWithCircumcenterIndex.pointIndex x))
                          (pointsWithCircumcenter t (PointsWithCircumcenterIndex.pointIndex x_1)))) +
                HSub.hSub (α := ℝ) (↑(HAdd.hAdd (α := ℕ) 0 1) : ℝ)⁻¹ (if x = i₁ ∨ x = i₂ then 1 else 0) *
                    (HDiv.hDiv (α := ℝ) (-2) (↑(HAdd.hAdd (α := ℕ) 0 1) : ℝ) - -1) *
                  (dist (pointsWithCircumcenter t (PointsWithCircumcenterIndex.pointIndex x))
                      (pointsWithCircumcenter t PointsWithCircumcenterIndex.circumcenterIndex) *
                    dist (pointsWithCircumcenter t (PointsWithCircumcenterIndex.pointIndex x))
                      (pointsWithCircumcenter t PointsWithCircumcenterIndex.circumcenterIndex))))
            (∑ x ∈ {i₁, i₂},
              (HAdd.hAdd (α := ℝ)
                  (∑ x_1 ∈ {i₃},
                    HSub.hSub (α := ℝ) (↑(HAdd.hAdd (α := ℕ) 0 1) : ℝ)⁻¹ (if x = i₁ ∨ x = i₂ then 1 else 0) *
                        HSub.hSub (α := ℝ) (↑(HAdd.hAdd (α := ℕ) 0 1) : ℝ)⁻¹ (if x_1 = i₁ ∨ x_1 = i₂ then 1 else 0) *
                      (dist (pointsWithCircumcenter t (PointsWithCircumcenterIndex.pointIndex x))
                          (pointsWithCircumcenter t (PointsWithCircumcenterIndex.pointIndex x_1)) *
                        dist (pointsWithCircumcenter t (PointsWithCircumcenterIndex.pointIndex x))
                          (pointsWithCircumcenter t (PointsWithCircumcenterIndex.pointIndex x_1))))
                  (∑ x_1 ∈ {i₁, i₂},
                    HSub.hSub (α := ℝ) (↑(HAdd.hAdd (α := ℕ) 0 1) : ℝ)⁻¹ (if x = i₁ ∨ x = i₂ then 1 else 0) *
                        HSub.hSub (α := ℝ) (↑(HAdd.hAdd (α := ℕ) 0 1) : ℝ)⁻¹ (if x_1 = i₁ ∨ x_1 = i₂ then 1 else 0) *
                      (dist (pointsWithCircumcenter t (PointsWithCircumcenterIndex.pointIndex x))
                          (pointsWithCircumcenter t (PointsWithCircumcenterIndex.pointIndex x_1)) *
                        dist (pointsWithCircumcenter t (PointsWithCircumcenterIndex.pointIndex x))
                          (pointsWithCircumcenter t (PointsWithCircumcenterIndex.pointIndex x_1)))) +
                HSub.hSub (α := ℝ) (↑(HAdd.hAdd (α := ℕ) 0 1) : ℝ)⁻¹ (if x = i₁ ∨ x = i₂ then 1 else 0) *
                    (HDiv.hDiv (α := ℝ) (-2) (↑(HAdd.hAdd (α := ℕ) 0 1) : ℝ) - -1) *
                  (dist (pointsWithCircumcenter t (PointsWithCircumcenterIndex.pointIndex x))
                      (pointsWithCircumcenter t PointsWithCircumcenterIndex.circumcenterIndex) *
                    dist (pointsWithCircumcenter t (PointsWithCircumcenterIndex.pointIndex x))
                      (pointsWithCircumcenter t PointsWithCircumcenterIndex.circumcenterIndex)))) +
          (HAdd.hAdd (α := ℝ)
              (∑ x ∈ {i₃},
                (HDiv.hDiv (α := ℝ) (-2) (↑(HAdd.hAdd (α := ℕ) 0 1) : ℝ) - -1) *
                    HSub.hSub (α := ℝ) (↑(HAdd.hAdd (α := ℕ) 0 1) : ℝ)⁻¹ (if x = i₁ ∨ x = i₂ then 1 else 0) *
                  (dist (pointsWithCircumcenter t PointsWithCircumcenterIndex.circumcenterIndex)
                      (pointsWithCircumcenter t (PointsWithCircumcenterIndex.pointIndex x)) *
                    dist (pointsWithCircumcenter t PointsWithCircumcenterIndex.circumcenterIndex)
                      (pointsWithCircumcenter t (PointsWithCircumcenterIndex.pointIndex x))))
              (∑ x ∈ {i₁, i₂},
                (HDiv.hDiv (α := ℝ) (-2) (↑(HAdd.hAdd (α := ℕ) 0 1) : ℝ) - -1) *
                    HSub.hSub (α := ℝ) (↑(HAdd.hAdd (α := ℕ) 0 1) : ℝ)⁻¹ (if x = i₁ ∨ x = i₂ then 1 else 0) *
                  (dist (pointsWithCircumcenter t PointsWithCircumcenterIndex.circumcenterIndex)
                      (pointsWithCircumcenter t (PointsWithCircumcenterIndex.pointIndex x)) *
                    dist (pointsWithCircumcenter t PointsWithCircumcenterIndex.circumcenterIndex)
                      (pointsWithCircumcenter t (PointsWithCircumcenterIndex.pointIndex x)))) +
            (HDiv.hDiv (α := ℝ) (-2) (↑(HAdd.hAdd (α := ℕ) 0 1) : ℝ) - -1) *
                (HDiv.hDiv (α := ℝ) (-2) (↑(HAdd.hAdd (α := ℕ) 0 1) : ℝ) - -1) *
              (dist (pointsWithCircumcenter t PointsWithCircumcenterIndex.circumcenterIndex)
                  (pointsWithCircumcenter t PointsWithCircumcenterIndex.circumcenterIndex) *
                dist (pointsWithCircumcenter t PointsWithCircumcenterIndex.circumcenterIndex)
                  (pointsWithCircumcenter t PointsWithCircumcenterIndex.circumcenterIndex)))) /
      2 =
    circumradius t * circumradius t
⊢ -(∑ x : Fin (0 + 2 + 1),
            (∑ x_1 : Fin (0 + 2 + 1),
                HSub.hSub (α := ℝ) (↑(HAdd.hAdd (α := ℕ) 0 1) : ℝ)⁻¹ (if x = i₁ ∨ x = i₂ then 1 else 0) *
                    HSub.hSub (α := ℝ) (↑(HAdd.hAdd (α := ℕ) 0 1) : ℝ)⁻¹ (if x_1 = i₁ ∨ x_1 = i₂ then 1 else 0) *
                  (dist (pointsWithCircumcenter t (PointsWithCircumcenterIndex.pointIndex x))
                      (pointsWithCircumcenter t (PointsWithCircumcenterIndex.pointIndex x_1)) *
                    dist (pointsWithCircumcenter t (PointsWithCircumcenterIndex.pointIndex x))
                      (pointsWithCircumcenter t (PointsWithCircumcenterIndex.pointIndex x_1))) +
              HSub.hSub (α := ℝ) (↑(HAdd.hAdd (α := ℕ) 0 1) : ℝ)⁻¹ (if x = i₁ ∨ x = i₂ then 1 else 0) *
                  (HDiv.hDiv (α := ℝ) (-2) (↑(HAdd.hAdd (α := ℕ) 0 1) : ℝ) - -1) *
                (dist (pointsWithCircumcenter t (PointsWithCircumcenterIndex.pointIndex x))
                    (pointsWithCircumcenter t PointsWithCircumcenterIndex.circumcenterIndex) *
                  dist (pointsWithCircumcenter t (PointsWithCircumcenterIndex.pointIndex x))
                    (pointsWithCircumcenter t PointsWithCircumcenterIndex.circumcenterIndex))) +
          (∑ x : Fin (0 + 2 + 1),
              (HDiv.hDiv (α := ℝ) (-2) (↑(HAdd.hAdd (α := ℕ) 0 1) : ℝ) - -1) *
                  HSub.hSub (α := ℝ) (↑(HAdd.hAdd (α := ℕ) 0 1) : ℝ)⁻¹ (if x = i₁ ∨ x = i₂ then 1 else 0) *
                (dist (pointsWithCircumcenter t PointsWithCircumcenterIndex.circumcenterIndex)
                    (pointsWithCircumcenter t (PointsWithCircumcenterIndex.pointIndex x)) *
                  dist (pointsWithCircumcenter t PointsWithCircumcenterIndex.circumcenterIndex)
                    (pointsWithCircumcenter t (PointsWithCircumcenterIndex.pointIndex x))) +
            (HDiv.hDiv (α := ℝ) (-2) (↑(HAdd.hAdd (α := ℕ) 0 1) : ℝ) - -1) *
                (HDiv.hDiv (α := ℝ) (-2) (↑(HAdd.hAdd (α := ℕ) 0 1) : ℝ) - -1) *
              (dist (pointsWithCircumcenter t PointsWithCircumcenterIndex.circumcenterIndex)
                  (pointsWithCircumcenter t PointsWithCircumcenterIndex.circumcenterIndex) *
                dist (pointsWithCircumcenter t PointsWithCircumcenterIndex.circumcenterIndex)
                  (pointsWithCircumcenter t PointsWithCircumcenterIndex.circumcenterIndex)))) /
      2 =
    circumradius t * circumradius t

Tactic:
simp_rw [← sum_sdiff hu, hi₃]

Premises used: Finset.sum_sdiff