-- Mathlib/Geometry/Euclidean/MongePoint.lean
theorem dist_orthocenter_reflection_circumcenter (t : Triangle ℝ P) {i₁ i₂ : Fin 3} (h : i₁ ≠ i₂) :
    dist t.orthocenter (reflection (affineSpan ℝ (t.points '' {i₁, i₂})) t.circumcenter) =
      t.circumradius

Proof state:
case intro.intro.intro
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₂
hu : {i₁, i₂} ⊆ univ
i₃ : Fin 3
hi₃ : univ \ {i₁, i₂} = {i₃}
hi₃₁ : i₃ ≠ i₁
hi₃₂ : i₃ ≠ i₂
⊢ -(∑ x ∈ {i₃},
              (∑ x_1 ∈ {i₃},
                    ((↑(0 + 1))⁻¹ - if x = i₁ ∨ x = i₂ then 1 else 0) *
                        ((↑(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₂},
                    ((↑(0 + 1))⁻¹ - if x = i₁ ∨ x = i₂ then 1 else 0) *
                        ((↑(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))) +
                ((↑(0 + 1))⁻¹ - if x = i₁ ∨ x = i₂ then 1 else 0) * (-2 / ↑(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₂},
              (∑ x_1 ∈ {i₃},
                    ((↑(0 + 1))⁻¹ - if x = i₁ ∨ x = i₂ then 1 else 0) *
                        ((↑(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₂},
                    ((↑(0 + 1))⁻¹ - if x = i₁ ∨ x = i₂ then 1 else 0) *
                        ((↑(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))) +
                ((↑(0 + 1))⁻¹ - if x = i₁ ∨ x = i₂ then 1 else 0) * (-2 / ↑(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₃},
                (-2 / ↑(0 + 1) - -1) * ((↑(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₂},
                (-2 / ↑(0 + 1) - -1) * ((↑(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))) +
            (-2 / ↑(0 + 1) - -1) * (-2 / ↑(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:
norm_num [hi₃₁, hi₃₂]

Result:
no goals

Proof state:
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₂
hu : {i₁, i₂} ⊆ univ
⊢ ∃ i₃, univ \ {i₁, i₂} = {i₃} ∧ i₃ ≠ i₁ ∧ i₃ ≠ i₂

Tactic:
decide +revert

Result:
no goals