<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>t : Triangle ℝ P<VAR>i₁ i₂ : Fin 3<VAR>h : i₁ ≠ i₂<VAR>hu : {i₁, i₂} ⊆ univ<VAR>i₃ : Fin 3<VAR>hi₃ : univ \ {i₁, i₂} = {i₃}<VAR>hi₃₁ : i₃ ≠ i₁<VAR>hi₃₂ : i₃ ≠ i₂<GOAL>-(∑ x ∈ {i₃}, ((↑(0 + 1))⁻¹ - if i₃ = i₁ ∨ i₃ = i₂ then 1 else 0) * ((↑(0 + 1))⁻¹ - if x = i₁ ∨ x = i₂ then 1 else 0) * (dist (pointsWithCircumcenter t (PointsWithCircumcenterIndex.pointIndex i₃)) (pointsWithCircumcenter t (PointsWithCircumcenterIndex.pointIndex x)) * dist (pointsWithCircumcenter t (PointsWithCircumcenterIndex.pointIndex i₃)) (pointsWithCircumcenter t (PointsWithCircumcenterIndex.pointIndex x))) + ∑ x ∈ {i₁, i₂}, ((↑(0 + 1))⁻¹ - if i₃ = i₁ ∨ i₃ = i₂ then 1 else 0) * ((↑(0 + 1))⁻¹ - if x = i₁ ∨ x = i₂ then 1 else 0) * (dist (pointsWithCircumcenter t (PointsWithCircumcenterIndex.pointIndex i₃)) (pointsWithCircumcenter t (PointsWithCircumcenterIndex.pointIndex x)) * dist (pointsWithCircumcenter t (PointsWithCircumcenterIndex.pointIndex i₃)) (pointsWithCircumcenter t (PointsWithCircumcenterIndex.pointIndex x))) + ((↑(0 + 1))⁻¹ - if i₃ = i₁ ∨ i₃ = i₂ then 1 else 0) * (-2 / ↑(0 + 1) - -1) * (dist (pointsWithCircumcenter t (PointsWithCircumcenterIndex.pointIndex i₃)) (pointsWithCircumcenter t PointsWithCircumcenterIndex.circumcenterIndex) * dist (pointsWithCircumcenter t (PointsWithCircumcenterIndex.pointIndex i₃)) (pointsWithCircumcenter t PointsWithCircumcenterIndex.circumcenterIndex)) + ∑ x ∈ {i₁, i₂}, (∑ x_1 : Fin (0 + 2 + 1), ((↑(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