feat(geometry/euclidean): circumradius simp lemmas (#3834)

Mark `dist_circumcenter_eq_circumradius` as a `simp` lemma.  Also add
a variant of that lemma where the distance is the other way round so
`simp` can work with both forms.

Author: jsm28

src/geometry/euclidean.lean

@@ -1185,10 +1185,20 @@ s.circumcenter_circumradius_unique_dist_eq.1.1
 
 /-- All points have distance from the circumcenter equal to the
 circumradius. -/
-lemma dist_circumcenter_eq_circumradius {n : ℕ} (s : simplex ℝ P n) :
+@[simp] lemma dist_circumcenter_eq_circumradius {n : ℕ} (s : simplex ℝ P n) :
   ∀ i, dist (s.points i) s.circumcenter = s.circumradius :=
 s.circumcenter_circumradius_unique_dist_eq.1.2
 
+/-- All points have distance to the circumcenter equal to the
+circumradius. -/
+@[simp] lemma dist_circumcenter_eq_circumradius' {n : ℕ} (s : simplex ℝ P n) :
+  ∀ i, dist s.circumcenter (s.points i) = s.circumradius :=
+begin
+  intro i,
+  rw dist_comm,
+  exact dist_circumcenter_eq_circumradius _ _
+end
+
 /-- Given a point in the affine span from which all the points are
 equidistant, that point is the circumcenter. -/
 lemma eq_circumcenter_of_dist_eq {n : ℕ} (s : simplex ℝ P n) {p : P}