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₂
⊢ -(∑ x,
            (∑ x_1,
                (mongePointWeightsWithCircumcenter 0 (PointsWithCircumcenterIndex.pointIndex x) -
                      reflectionCircumcenterWeightsWithCircumcenter i₁ i₂ (PointsWithCircumcenterIndex.pointIndex x)) *
                    (mongePointWeightsWithCircumcenter 0 (PointsWithCircumcenterIndex.pointIndex x_1) -
                      reflectionCircumcenterWeightsWithCircumcenter i₁ i₂
                        (PointsWithCircumcenterIndex.pointIndex x_1)) *
                  (dist (pointsWithCircumcenter t (PointsWithCircumcenterIndex.pointIndex x))
                      (pointsWithCircumcenter t (PointsWithCircumcenterIndex.pointIndex x_1)) *
                    dist (pointsWithCircumcenter t (PointsWithCircumcenterIndex.pointIndex x))
                      (pointsWithCircumcenter t (PointsWithCircumcenterIndex.pointIndex x_1))) +
              (mongePointWeightsWithCircumcenter 0 (PointsWithCircumcenterIndex.pointIndex x) -
                    reflectionCircumcenterWeightsWithCircumcenter i₁ i₂ (PointsWithCircumcenterIndex.pointIndex x)) *
                  (mongePointWeightsWithCircumcenter 0 PointsWithCircumcenterIndex.circumcenterIndex -
                    reflectionCircumcenterWeightsWithCircumcenter i₁ i₂ PointsWithCircumcenterIndex.circumcenterIndex) *
                (dist (pointsWithCircumcenter t (PointsWithCircumcenterIndex.pointIndex x))
                    (pointsWithCircumcenter t PointsWithCircumcenterIndex.circumcenterIndex) *
                  dist (pointsWithCircumcenter t (PointsWithCircumcenterIndex.pointIndex x))
                    (pointsWithCircumcenter t PointsWithCircumcenterIndex.circumcenterIndex))) +
          (∑ x,
              (mongePointWeightsWithCircumcenter 0 PointsWithCircumcenterIndex.circumcenterIndex -
                    reflectionCircumcenterWeightsWithCircumcenter i₁ i₂ PointsWithCircumcenterIndex.circumcenterIndex) *
                  (mongePointWeightsWithCircumcenter 0 (PointsWithCircumcenterIndex.pointIndex x) -
                    reflectionCircumcenterWeightsWithCircumcenter i₁ i₂ (PointsWithCircumcenterIndex.pointIndex x)) *
                (dist (pointsWithCircumcenter t PointsWithCircumcenterIndex.circumcenterIndex)
                    (pointsWithCircumcenter t (PointsWithCircumcenterIndex.pointIndex x)) *
                  dist (pointsWithCircumcenter t PointsWithCircumcenterIndex.circumcenterIndex)
                    (pointsWithCircumcenter t (PointsWithCircumcenterIndex.pointIndex x))) +
            (mongePointWeightsWithCircumcenter 0 PointsWithCircumcenterIndex.circumcenterIndex -
                  reflectionCircumcenterWeightsWithCircumcenter i₁ i₂ PointsWithCircumcenterIndex.circumcenterIndex) *
                (mongePointWeightsWithCircumcenter 0 PointsWithCircumcenterIndex.circumcenterIndex -
                  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

Tactic:
mongePointWeightsWithCircumcenter,

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₂
⊢ -(∑ x,
            (∑ x_1,
                ((↑(0 + 1))⁻¹ -
                      reflectionCircumcenterWeightsWithCircumcenter i₁ i₂ (PointsWithCircumcenterIndex.pointIndex x)) *
                    ((↑(0 + 1))⁻¹ -
                      reflectionCircumcenterWeightsWithCircumcenter i₁ i₂
                        (PointsWithCircumcenterIndex.pointIndex x_1)) *
                  (dist (pointsWithCircumcenter t (PointsWithCircumcenterIndex.pointIndex x))
                      (pointsWithCircumcenter t (PointsWithCircumcenterIndex.pointIndex x_1)) *
                    dist (pointsWithCircumcenter t (PointsWithCircumcenterIndex.pointIndex x))
                      (pointsWithCircumcenter t (PointsWithCircumcenterIndex.pointIndex x_1))) +
              ((↑(0 + 1))⁻¹ -
                    reflectionCircumcenterWeightsWithCircumcenter i₁ i₂ (PointsWithCircumcenterIndex.pointIndex x)) *
                  (-2 / ↑(0 + 1) -
                    reflectionCircumcenterWeightsWithCircumcenter i₁ i₂ PointsWithCircumcenterIndex.circumcenterIndex) *
                (dist (pointsWithCircumcenter t (PointsWithCircumcenterIndex.pointIndex x))
                    (pointsWithCircumcenter t PointsWithCircumcenterIndex.circumcenterIndex) *
                  dist (pointsWithCircumcenter t (PointsWithCircumcenterIndex.pointIndex x))
                    (pointsWithCircumcenter t PointsWithCircumcenterIndex.circumcenterIndex))) +
          (∑ x,
              (-2 / ↑(0 + 1) -
                    reflectionCircumcenterWeightsWithCircumcenter i₁ i₂ PointsWithCircumcenterIndex.circumcenterIndex) *
                  ((↑(0 + 1))⁻¹ -
                    reflectionCircumcenterWeightsWithCircumcenter i₁ i₂ (PointsWithCircumcenterIndex.pointIndex x)) *
                (dist (pointsWithCircumcenter t PointsWithCircumcenterIndex.circumcenterIndex)
                    (pointsWithCircumcenter t (PointsWithCircumcenterIndex.pointIndex x)) *
                  dist (pointsWithCircumcenter t PointsWithCircumcenterIndex.circumcenterIndex)
                    (pointsWithCircumcenter t (PointsWithCircumcenterIndex.pointIndex x))) +
            (-2 / ↑(0 + 1) -
                  reflectionCircumcenterWeightsWithCircumcenter i₁ i₂ PointsWithCircumcenterIndex.circumcenterIndex) *
                (-2 / ↑(0 + 1) -
                  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