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,
            (∑ 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

Tactic:
Pi.sub_apply,

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,
                (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