Module: Mathlib.Geometry.Euclidean.MongePoint

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
t : Triangle ℝ P
i₁ i₂ : Fin 3
h : i₁ ≠ i₂
⊢ (-∑ i₁_1,
          ∑ i₂_1,
            (mongePointWeightsWithCircumcenter 0 - reflectionCircumcenterWeightsWithCircumcenter i₁ i₂) i₁_1 *
                (mongePointWeightsWithCircumcenter 0 - reflectionCircumcenterWeightsWithCircumcenter i₁ i₂) i₂_1 *
              (dist (pointsWithCircumcenter t i₁_1) (pointsWithCircumcenter t i₂_1) *
                dist (pointsWithCircumcenter t i₁_1) (pointsWithCircumcenter t i₂_1))) /
      2 =
    circumradius t * circumradius t

Tactic:
sum_pointsWithCircumcenter,

Goal state after:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
t : Triangle ℝ P
i₁ i₂ : Fin 3
h : i₁ ≠ i₂
⊢ -(∑ i,
            (∑ i_1,
                (mongePointWeightsWithCircumcenter 0 - reflectionCircumcenterWeightsWithCircumcenter i₁ i₂)
                      (PointsWithCircumcenterIndex.pointIndex i) *
                    (mongePointWeightsWithCircumcenter 0 - reflectionCircumcenterWeightsWithCircumcenter i₁ i₂)
                      (PointsWithCircumcenterIndex.pointIndex i_1) *
                  (dist (pointsWithCircumcenter t (PointsWithCircumcenterIndex.pointIndex i))
                      (pointsWithCircumcenter t (PointsWithCircumcenterIndex.pointIndex i_1)) *
                    dist (pointsWithCircumcenter t (PointsWithCircumcenterIndex.pointIndex i))
                      (pointsWithCircumcenter t (PointsWithCircumcenterIndex.pointIndex i_1))) +
              (mongePointWeightsWithCircumcenter 0 - reflectionCircumcenterWeightsWithCircumcenter i₁ i₂)
                    (PointsWithCircumcenterIndex.pointIndex i) *
                  (mongePointWeightsWithCircumcenter 0 - reflectionCircumcenterWeightsWithCircumcenter i₁ i₂)
                    PointsWithCircumcenterIndex.circumcenterIndex *
                (dist (pointsWithCircumcenter t (PointsWithCircumcenterIndex.pointIndex i))
                    (pointsWithCircumcenter t PointsWithCircumcenterIndex.circumcenterIndex) *
                  dist (pointsWithCircumcenter t (PointsWithCircumcenterIndex.pointIndex i))
                    (pointsWithCircumcenter t PointsWithCircumcenterIndex.circumcenterIndex))) +
          (∑ i,
              (mongePointWeightsWithCircumcenter 0 - reflectionCircumcenterWeightsWithCircumcenter i₁ i₂)
                    PointsWithCircumcenterIndex.circumcenterIndex *
                  (mongePointWeightsWithCircumcenter 0 - reflectionCircumcenterWeightsWithCircumcenter i₁ i₂)
                    (PointsWithCircumcenterIndex.pointIndex i) *
                (dist (pointsWithCircumcenter t PointsWithCircumcenterIndex.circumcenterIndex)
                    (pointsWithCircumcenter t (PointsWithCircumcenterIndex.pointIndex i)) *
                  dist (pointsWithCircumcenter t PointsWithCircumcenterIndex.circumcenterIndex)
                    (pointsWithCircumcenter t (PointsWithCircumcenterIndex.pointIndex i))) +
            (mongePointWeightsWithCircumcenter 0 - reflectionCircumcenterWeightsWithCircumcenter i₁ i₂)
                  PointsWithCircumcenterIndex.circumcenterIndex *
                (mongePointWeightsWithCircumcenter 0 - reflectionCircumcenterWeightsWithCircumcenter i₁ i₂)
                  PointsWithCircumcenterIndex.circumcenterIndex *
              (dist (pointsWithCircumcenter t PointsWithCircumcenterIndex.circumcenterIndex)
                  (pointsWithCircumcenter t PointsWithCircumcenterIndex.circumcenterIndex) *
                dist (pointsWithCircumcenter t PointsWithCircumcenterIndex.circumcenterIndex)
                  (pointsWithCircumcenter t PointsWithCircumcenterIndex.circumcenterIndex)))) /
      2 =
    circumradius t * circumradius t