-- Lean 4 proof step from Mathlib.Geometry.Euclidean.MongePoint (goal)
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₂
⊢ HDiv.hDiv (α := ℝ)
      (-∑ i₁_1 : PointsWithCircumcenterIndex 2,
          ∑ i₂_1 : PointsWithCircumcenterIndex 2,
            HSub.hSub (α := PointsWithCircumcenterIndex 2 → ℝ) (mongePointWeightsWithCircumcenter 0)
                  (reflectionCircumcenterWeightsWithCircumcenter i₁ i₂) i₁_1 *
                HSub.hSub (α := PointsWithCircumcenterIndex 2 → ℝ) (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
have simp_rw : -(∑ 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_pointsWithCircumcenter, Pi.sub_apply, mongePointWeightsWithCircumcenter,
    reflectionCircumcenterWeightsWithCircumcenter]