feat(geometry/euclidean/basic): bundled spheres (#16184)

Define a bundled `sphere` structure, for various uses in Euclidean
geometry where it's convenient to pass around `center` and `radius`
together.

Some basic API is set up for this structure, including `sphere`
versions of a few existing lemmas that could naturally be expressed in
that way.  The construction of `circumcenter` and `circumradius` is
also changed to pass around a `sphere` instead of using `P × ℝ`.  It
is likely that other existing lemmas can usefully have bundled sphere
versions added in followups.  Certainly there are plenty of other
definitions and results about spheres that can usefully be built up on
top of this basic API.

Notes:

* As with `cospherical`, the definition and some of the most basic
  lemmas don't actually need anything more than the metric space
  structure.  `sphere` is defined alongside `cospherical`, but it
  would also be reasonable to define both in some metric space file.
  In that case, the name of `sphere` would need to change to avoid
  conflicts with the existing `metric.sphere` (which is part of a
  family of unbundled definitions with `metric.ball` and
  `metric.closed_ball`, so should probably remain as-is).

* The definition doesn't include any non-degeneracy conditions, so
  avoiding the need for users to prove such conditions when
  constructing a `sphere` for a lemma that doesn't need them.  Note
  that the base case for the induction constructing the circumsphere
  uses a radius of zero.

* I haven't forgotten the discussion in #4088 of simplifying the proof
  of `eq_of_dist_eq_of_dist_eq_of_mem_of_finrank_eq_two` using bundled
  spheres, a definition of the radical subspace and a proof that a
  one-dimensional sphere has at most two points (so ending up proving
  the unbundled lemma using the bundled one rather than vice versa),
  but I think quite a lot more API about power of a point and radical
  subspaces would still need adding before that could be done.

src/geometry/euclidean/basic.lean

@@ -1315,6 +1315,69 @@ reflection_orthogonal_vadd hp₁
 
 omit V
 
+variables (P)
+
+/-- A `sphere P` bundles a `center` and `radius`. This definition does not require the radius to
+be positive; that should be given as a hypothesis to lemmas that require it. -/
+@[ext] structure sphere :=
+(center : P)
+(radius : ℝ)
+
+variables {P}
+
+instance [nonempty P] : nonempty (sphere P) := ⟨⟨classical.arbitrary P, 0⟩⟩
+
+instance : has_coe (sphere P) (set P) := ⟨λ s, metric.sphere s.center s.radius⟩
+instance : has_mem P (sphere P) := ⟨λ p s, p ∈ (s : set P)⟩
+
+lemma sphere.mk_center (c : P) (r : ℝ) : (⟨c, r⟩ : sphere P).center = c := rfl
+
+lemma sphere.mk_radius (c : P) (r : ℝ) : (⟨c, r⟩ : sphere P).radius = r := rfl
+
+@[simp] lemma sphere.mk_center_radius (s : sphere P) : (⟨s.center, s.radius⟩ : sphere P) = s :=
+by ext; refl
+
+lemma sphere.coe_def (s : sphere P) : (s : set P) = metric.sphere s.center s.radius := rfl
+
+@[simp] lemma sphere.coe_mk (c : P) (r : ℝ) : ↑(⟨c, r⟩ : sphere P) = metric.sphere c r := rfl
+
+@[simp] lemma sphere.mem_coe {p : P} {s : sphere P} : p ∈ (s : set P) ↔ p ∈ s := iff.rfl
+
+lemma mem_sphere {p : P} {s : sphere P} : p ∈ s ↔ dist p s.center = s.radius := iff.rfl
+
+lemma mem_sphere' {p : P} {s : sphere P} : p ∈ s ↔ dist s.center p = s.radius :=
+metric.mem_sphere'
+
+lemma subset_sphere {ps : set P} {s : sphere P} : ps ⊆ s ↔ ∀ p ∈ ps, p ∈ s := iff.rfl
+
+lemma dist_of_mem_subset_sphere {p : P} {ps : set P} {s : sphere P} (hp : p ∈ ps)
+  (hps : ps ⊆ (s : set P)) : dist p s.center = s.radius :=
+mem_sphere.1 (sphere.mem_coe.1 (set.mem_of_mem_of_subset hp hps))
+
+lemma dist_of_mem_subset_mk_sphere {p c : P} {ps : set P} {r : ℝ} (hp : p ∈ ps)
+  (hps : ps ⊆ ↑(⟨c, r⟩ : sphere P)) : dist p c = r :=
+dist_of_mem_subset_sphere hp hps
+
+lemma sphere.ne_iff {s₁ s₂ : sphere P} :
+  s₁ ≠ s₂ ↔ s₁.center ≠ s₂.center ∨ s₁.radius ≠ s₂.radius :=
+by rw [←not_and_distrib, ←sphere.ext_iff]
+
+lemma sphere.center_eq_iff_eq_of_mem {s₁ s₂ : sphere P} {p : P} (hs₁ : p ∈ s₁) (hs₂ : p ∈ s₂) :
+  s₁.center = s₂.center ↔ s₁ = s₂ :=
+begin
+  refine ⟨λ h, sphere.ext _ _ h _, λ h, h ▸ rfl⟩,
+  rw mem_sphere at hs₁ hs₂,
+  rw [←hs₁, ←hs₂, h]
+end
+
+lemma sphere.center_ne_iff_ne_of_mem {s₁ s₂ : sphere P} {p : P} (hs₁ : p ∈ s₁) (hs₂ : p ∈ s₂) :
+  s₁.center ≠ s₂.center ↔ s₁ ≠ s₂ :=
+(sphere.center_eq_iff_eq_of_mem hs₁ hs₂).not
+
+lemma dist_center_eq_dist_center_of_mem_sphere {p₁ p₂ : P} {s : sphere P} (hp₁ : p₁ ∈ s)
+  (hp₂ : p₂ ∈ s) : dist p₁ s.center = dist p₂ s.center :=
+by rw [mem_sphere.1 hp₁, mem_sphere.1 hp₂]
+
 /-- A set of points is cospherical if they are equidistant from some
 point.  In two dimensions, this is the same thing as being
 concyclic. -/
@@ -1326,6 +1389,21 @@ lemma cospherical_def (ps : set P) :
   cospherical ps ↔ ∃ (center : P) (radius : ℝ), ∀ p ∈ ps, dist p center = radius :=
 iff.rfl
 
+/-- A set of points is cospherical if and only if they lie in some sphere. -/
+lemma cospherical_iff_exists_sphere {ps : set P} :
+  cospherical ps ↔ ∃ s : sphere P, ps ⊆ (s : set P) :=
+begin
+  refine ⟨λ h, _, λ h, _⟩,
+  { rcases h with ⟨c, r, h⟩,
+    exact ⟨⟨c, r⟩, h⟩ },
+  { rcases h with ⟨s, h⟩,
+    exact ⟨s.center, s.radius, h⟩ }
+end
+
+/-- The set of points in a sphere is cospherical. -/
+lemma sphere.cospherical (s : sphere P) : cospherical (s : set P) :=
+cospherical_iff_exists_sphere.2 ⟨s, set.subset.rfl⟩
+
 /-- A subset of a cospherical set is cospherical. -/
 lemma cospherical_subset {ps₁ ps₂ : set P} (hs : ps₁ ⊆ ps₂) (hc : cospherical ps₂) :
   cospherical ps₁ :=
@@ -1410,4 +1488,34 @@ begin
   exact (dec_trivial : (1 : fin 3) ≠ 2) (hfi hf12)
 end
 
+/-- Suppose that `p₁` and `p₂` lie in spheres `s₁` and `s₂`.  Then the vector between the centers
+of those spheres is orthogonal to that between `p₁` and `p₂`; this is a version of
+`inner_vsub_vsub_of_dist_eq_of_dist_eq` for bundled spheres.  (In two dimensions, this says that
+the diagonals of a kite are orthogonal.) -/
+lemma inner_vsub_vsub_of_mem_sphere_of_mem_sphere {p₁ p₂ : P} {s₁ s₂ : sphere P}
+  (hp₁s₁ : p₁ ∈ s₁) (hp₂s₁ : p₂ ∈ s₁) (hp₁s₂ : p₁ ∈ s₂) (hp₂s₂ : p₂ ∈ s₂) :
+  ⟪s₂.center -ᵥ s₁.center, p₂ -ᵥ p₁⟫ = 0 :=
+inner_vsub_vsub_of_dist_eq_of_dist_eq (dist_center_eq_dist_center_of_mem_sphere hp₁s₁ hp₂s₁)
+                                      (dist_center_eq_dist_center_of_mem_sphere hp₁s₂ hp₂s₂)
+
+/-- Two spheres intersect in at most two points in a two-dimensional subspace containing their
+centers; this is a version of `eq_of_dist_eq_of_dist_eq_of_mem_of_finrank_eq_two` for bundled
+spheres. -/
+lemma eq_of_mem_sphere_of_mem_sphere_of_mem_of_finrank_eq_two {s : affine_subspace ℝ P}
+  [finite_dimensional ℝ s.direction] (hd : finrank ℝ s.direction = 2) {s₁ s₂ : sphere P}
+  {p₁ p₂ p : P} (hs₁ : s₁.center ∈ s) (hs₂ : s₂.center ∈ s) (hp₁s : p₁ ∈ s) (hp₂s : p₂ ∈ s)
+  (hps : p ∈ s) (hs : s₁ ≠ s₂) (hp : p₁ ≠ p₂) (hp₁s₁ : p₁ ∈ s₁) (hp₂s₁ : p₂ ∈ s₁) (hps₁ : p ∈ s₁)
+  (hp₁s₂ : p₁ ∈ s₂) (hp₂s₂ : p₂ ∈ s₂) (hps₂ : p ∈ s₂) : p = p₁ ∨ p = p₂ :=
+eq_of_dist_eq_of_dist_eq_of_mem_of_finrank_eq_two hd hs₁ hs₂ hp₁s hp₂s hps
+  ((sphere.center_ne_iff_ne_of_mem hps₁ hps₂).2 hs) hp hp₁s₁ hp₂s₁ hps₁ hp₁s₂ hp₂s₂ hps₂
+
+/-- Two spheres intersect in at most two points in two-dimensional space; this is a version of
+`eq_of_dist_eq_of_dist_eq_of_finrank_eq_two` for bundled spheres. -/
+lemma eq_of_mem_sphere_of_mem_sphere_of_finrank_eq_two [finite_dimensional ℝ V]
+  (hd : finrank ℝ V = 2) {s₁ s₂ : sphere P} {p₁ p₂ p : P} (hs : s₁ ≠ s₂) (hp : p₁ ≠ p₂)
+  (hp₁s₁ : p₁ ∈ s₁) (hp₂s₁ : p₂ ∈ s₁) (hps₁ : p ∈ s₁) (hp₁s₂ : p₁ ∈ s₂) (hp₂s₂ : p₂ ∈ s₂)
+  (hps₂ : p ∈ s₂) : p = p₁ ∨ p = p₂ :=
+eq_of_dist_eq_of_dist_eq_of_finrank_eq_two hd ((sphere.center_ne_iff_ne_of_mem hps₁ hps₂).2 hs)
+  hp hp₁s₁ hp₂s₁ hps₁ hp₁s₂ hp₂s₂ hps₂
+
 end euclidean_geometry

src/geometry/euclidean/circumcenter.lean

@@ -95,21 +95,21 @@ subspace with `p` added. -/
 lemma exists_unique_dist_eq_of_insert {s : affine_subspace ℝ P}
   [complete_space s.direction] {ps : set P} (hnps : ps.nonempty) {p : P}
   (hps : ps ⊆ s) (hp : p ∉ s)
-  (hu : ∃! cccr : (P × ℝ), cccr.fst ∈ s ∧ ∀ p1 ∈ ps, dist p1 cccr.fst = cccr.snd) :
-  ∃! cccr₂ : (P × ℝ), cccr₂.fst ∈ affine_span ℝ (insert p (s : set P)) ∧
-    ∀ p1 ∈ insert p ps, dist p1 cccr₂.fst = cccr₂.snd :=
+  (hu : ∃! cs : sphere P, cs.center ∈ s ∧ ps ⊆ (cs : set P)) :
+  ∃! cs₂ : sphere P, cs₂.center ∈ affine_span ℝ (insert p (s : set P)) ∧
+    (insert p ps) ⊆ (cs₂ : set P) :=
 begin
   haveI : nonempty s := set.nonempty.to_subtype (hnps.mono hps),
   rcases hu with ⟨⟨cc, cr⟩, ⟨hcc, hcr⟩, hcccru⟩,
-  simp only [prod.fst, prod.snd] at hcc hcr hcccru,
+  simp only at hcc hcr hcccru,
   let x := dist cc (orthogonal_projection s p),
   let y := dist p (orthogonal_projection s p),
   have hy0 : y ≠ 0 := dist_orthogonal_projection_ne_zero_of_not_mem hp,
   let ycc₂ := (x * x + y * y - cr * cr) / (2 * y),
   let cc₂ := (ycc₂ / y) • (p -ᵥ orthogonal_projection s p : V) +ᵥ cc,
   let cr₂ := real.sqrt (cr * cr + ycc₂ * ycc₂),
-  use (cc₂, cr₂),
-  simp only [prod.fst, prod.snd],
+  use ⟨cc₂, cr₂⟩,
+  simp only,
   have hpo : p = (1 : ℝ) • (p -ᵥ orthogonal_projection s p : V) +ᵥ orthogonal_projection s p,
   { simp },
   split,
@@ -120,7 +120,7 @@ begin
         (vsub_mem_vector_span ℝ (set.mem_insert _ _)
                                 (set.mem_insert_of_mem _ (orthogonal_projection_mem _))) },
     { intros p1 hp1,
-      rw [←mul_self_inj_of_nonneg dist_nonneg (real.sqrt_nonneg _),
+      rw [sphere.mem_coe, mem_sphere, ←mul_self_inj_of_nonneg dist_nonneg (real.sqrt_nonneg _),
           real.mul_self_sqrt (add_nonneg (mul_self_nonneg _) (mul_self_nonneg _))],
       cases hp1,
       { rw hp1,
@@ -134,39 +134,39 @@ begin
       { rw [dist_sq_eq_dist_orthogonal_projection_sq_add_dist_orthogonal_projection_sq
                _ (hps hp1),
             orthogonal_projection_vadd_smul_vsub_orthogonal_projection _ _ hcc, subtype.coe_mk,
-            hcr _ hp1, dist_eq_norm_vsub V cc₂ cc, vadd_vsub, norm_smul, ←dist_eq_norm_vsub V,
+            dist_of_mem_subset_mk_sphere hp1 hcr,
+            dist_eq_norm_vsub V cc₂ cc, vadd_vsub, norm_smul, ←dist_eq_norm_vsub V,
             real.norm_eq_abs, abs_div, abs_of_nonneg dist_nonneg, div_mul_cancel _ hy0,
             abs_mul_abs_self] } } },
   { rintros ⟨cc₃, cr₃⟩ ⟨hcc₃, hcr₃⟩,
-    simp only [prod.fst, prod.snd] at hcc₃ hcr₃,
+    simp only at hcc₃ hcr₃,
     obtain ⟨t₃, cc₃', hcc₃', hcc₃''⟩ :
       ∃ (r : ℝ) (p0 : P) (hp0 : p0 ∈ s), cc₃ = r • (p -ᵥ ↑((orthogonal_projection s) p)) +ᵥ p0,
     { rwa mem_affine_span_insert_iff (orthogonal_projection_mem p) at hcc₃ },
     have hcr₃' : ∃ r, ∀ p1 ∈ ps, dist p1 cc₃ = r :=
-      ⟨cr₃, λ p1 hp1, hcr₃ p1 (set.mem_insert_of_mem _ hp1)⟩,
+      ⟨cr₃, λ p1 hp1, dist_of_mem_subset_mk_sphere (set.mem_insert_of_mem _ hp1) hcr₃⟩,
     rw [exists_dist_eq_iff_exists_dist_orthogonal_projection_eq hps cc₃, hcc₃'',
       orthogonal_projection_vadd_smul_vsub_orthogonal_projection _ _ hcc₃'] at hcr₃',
     cases hcr₃' with cr₃' hcr₃',
-    have hu := hcccru (cc₃', cr₃'),
-    simp only [prod.fst, prod.snd] at hu,
+    have hu := hcccru ⟨cc₃', cr₃'⟩,
+    simp only at hu,
     replace hu := hu ⟨hcc₃', hcr₃'⟩,
-    rw prod.ext_iff at hu,
-    simp only [prod.fst, prod.snd] at hu,
     cases hu with hucc hucr,
     substs hucc hucr,
     have hcr₃val : cr₃ = real.sqrt (cr₃' * cr₃' + (t₃ * y) * (t₃ * y)),
     { cases hnps with p0 hp0,
       have h' : ↑(⟨cc₃', hcc₃'⟩ : s) = cc₃' := rfl,
-      rw [←hcr₃ p0 (set.mem_insert_of_mem _ hp0), hcc₃'',
+      rw [←dist_of_mem_subset_mk_sphere (set.mem_insert_of_mem _ hp0) hcr₃, hcc₃'',
           ←mul_self_inj_of_nonneg dist_nonneg (real.sqrt_nonneg _),
           real.mul_self_sqrt (add_nonneg (mul_self_nonneg _) (mul_self_nonneg _)),
           dist_sq_eq_dist_orthogonal_projection_sq_add_dist_orthogonal_projection_sq
             _ (hps hp0),
-          orthogonal_projection_vadd_smul_vsub_orthogonal_projection _ _ hcc₃', h', hcr p0 hp0,
+          orthogonal_projection_vadd_smul_vsub_orthogonal_projection _ _ hcc₃', h',
+          dist_of_mem_subset_mk_sphere hp0 hcr,
           dist_eq_norm_vsub V _ cc₃', vadd_vsub, norm_smul, ←dist_eq_norm_vsub V p,
           real.norm_eq_abs, ←mul_assoc, mul_comm _ (|t₃|), ←mul_assoc, abs_mul_abs_self],
       ring },
-    replace hcr₃ := hcr₃ p (set.mem_insert _ _),
+    replace hcr₃ := dist_of_mem_subset_mk_sphere (set.mem_insert _ _) hcr₃,
     rw [hpo, hcc₃'', hcr₃val, ←mul_self_inj_of_nonneg dist_nonneg (real.sqrt_nonneg _),
         dist_sq_smul_orthogonal_vadd_smul_orthogonal_vadd
           (orthogonal_projection_mem p) hcc₃' _ _
@@ -193,8 +193,7 @@ there is a unique (circumcenter, circumradius) pair for those points
 in the affine subspace they span. -/
 lemma _root_.affine_independent.exists_unique_dist_eq {ι : Type*} [hne : nonempty ι] [fintype ι]
     {p : ι → P} (ha : affine_independent ℝ p) :
-  ∃! cccr : (P × ℝ), cccr.fst ∈ affine_span ℝ (set.range p) ∧
-    ∀ i, dist (p i) cccr.fst = cccr.snd :=
+  ∃! cs : sphere P, cs.center ∈ affine_span ℝ (set.range p) ∧ set.range p ⊆ (cs : set P) :=
 begin
   unfreezingI { induction hn : fintype.card ι with m hm generalizing ι },
   { exfalso,
@@ -205,21 +204,17 @@ begin
     { rw fintype.card_eq_one_iff at hn,
       cases hn with i hi,
       haveI : unique ι := ⟨⟨i⟩, hi⟩,
-      use (p i, 0),
-      simp only [prod.fst, prod.snd, set.range_unique, affine_subspace.mem_affine_span_singleton],
+      use ⟨p i, 0⟩,
+      simp only [set.range_unique, affine_subspace.mem_affine_span_singleton],
       split,
-      { simp_rw [hi default],
-        use rfl,
-        intro i1,
-        rw hi i1,
-        exact dist_self _ },
+      { simp_rw [hi default, set.singleton_subset_iff, sphere.mem_coe, mem_sphere, dist_self],
+        exact ⟨rfl, rfl⟩ },
       { rintros ⟨cc, cr⟩,
-        simp only [prod.fst, prod.snd],
+        simp only,
         rintros ⟨rfl, hdist⟩,
-        rw hi default,
-        congr',
-        rw ←hdist default,
-        exact dist_self _ } },
+        simp_rw [set.singleton_subset_iff, sphere.mem_coe, mem_sphere, dist_self] at hdist,
+        rw [hi default, hdist],
+        exact ⟨rfl, rfl⟩ } },
     { have i := hne.some,
       let ι2 := {x // x ≠ i},
       have hc : fintype.card ι2 = m + 1,
@@ -239,13 +234,7 @@ begin
         rw [←set.image_eq_range, ←set.image_univ, ←set.image_insert_eq],
         congr' with j,
         simp [classical.em] },
-      change ∃! (cccr : P × ℝ), (_ ∧ ∀ i2, (λ q, dist q cccr.fst = cccr.snd) (p i2)),
-      conv { congr, funext, conv { congr, skip, rw ←set.forall_range_iff } },
-      dsimp only,
-      rw hr,
-      change ∃! (cccr : P × ℝ), (_ ∧ ∀ (i2 : ι2), (λ q, dist q cccr.fst = cccr.snd) (p i2)) at hm,
-      conv at hm { congr, funext, conv { congr, skip, rw ←set.forall_range_iff } },
-      rw ←affine_span_insert_affine_span,
+      rw [hr, ←affine_span_insert_affine_span],
       refine exists_unique_dist_eq_of_insert
         (set.range_nonempty _)
         (subset_span_points ℝ _)
@@ -269,36 +258,46 @@ variables {V : Type*} {P : Type*} [inner_product_space ℝ V] [metric_space P]
     [normed_add_torsor V P]
 include V
 
-/-- The pair (circumcenter, circumradius) of a simplex. -/
-def circumcenter_circumradius {n : ℕ} (s : simplex ℝ P n) : (P × ℝ) :=
+/-- The circumsphere of a simplex. -/
+def circumsphere {n : ℕ} (s : simplex ℝ P n) : sphere P :=
 s.independent.exists_unique_dist_eq.some
 
-/-- The property satisfied by the (circumcenter, circumradius) pair. -/
-lemma circumcenter_circumradius_unique_dist_eq {n : ℕ} (s : simplex ℝ P n) :
-  (s.circumcenter_circumradius.fst ∈ affine_span ℝ (set.range s.points) ∧
-    ∀ i, dist (s.points i) s.circumcenter_circumradius.fst = s.circumcenter_circumradius.snd) ∧
-  (∀ cccr : (P × ℝ), (cccr.fst ∈ affine_span ℝ (set.range s.points) ∧
-    ∀ i, dist (s.points i) cccr.fst = cccr.snd) → cccr = s.circumcenter_circumradius) :=
+/-- The property satisfied by the circumsphere. -/
+lemma circumsphere_unique_dist_eq {n : ℕ} (s : simplex ℝ P n) :
+  (s.circumsphere.center ∈ affine_span ℝ (set.range s.points) ∧
+    set.range s.points ⊆ s.circumsphere) ∧
+  (∀ cs : sphere P, (cs.center ∈ affine_span ℝ (set.range s.points) ∧
+    set.range s.points ⊆ cs → cs = s.circumsphere)) :=
 s.independent.exists_unique_dist_eq.some_spec
 
 /-- The circumcenter of a simplex. -/
 def circumcenter {n : ℕ} (s : simplex ℝ P n) : P :=
-s.circumcenter_circumradius.fst
+s.circumsphere.center
 
 /-- The circumradius of a simplex. -/
 def circumradius {n : ℕ} (s : simplex ℝ P n) : ℝ :=
-s.circumcenter_circumradius.snd
+s.circumsphere.radius
+
+/-- The center of the circumsphere is the circumcenter. -/
+@[simp] lemma circumsphere_center {n : ℕ} (s : simplex ℝ P n) :
+  s.circumsphere.center = s.circumcenter :=
+rfl
+
+/-- The radius of the circumsphere is the circumradius. -/
+@[simp] lemma circumsphere_radius {n : ℕ} (s : simplex ℝ P n) :
+  s.circumsphere.radius = s.circumradius :=
+rfl
 
 /-- The circumcenter lies in the affine span. -/
 lemma circumcenter_mem_affine_span {n : ℕ} (s : simplex ℝ P n) :
   s.circumcenter ∈ affine_span ℝ (set.range s.points) :=
-s.circumcenter_circumradius_unique_dist_eq.1.1
+s.circumsphere_unique_dist_eq.1.1
 
 /-- All points have distance from the circumcenter equal to the
 circumradius. -/
-@[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
+@[simp] lemma dist_circumcenter_eq_circumradius {n : ℕ} (s : simplex ℝ P n) (i : fin (n + 1)) :
+  dist (s.points i) s.circumcenter = s.circumradius :=
+dist_of_mem_subset_sphere (set.mem_range_self _) s.circumsphere_unique_dist_eq.1.2
 
 /-- All points have distance to the circumcenter equal to the
 circumradius. -/
@@ -316,8 +315,9 @@ lemma eq_circumcenter_of_dist_eq {n : ℕ} (s : simplex ℝ P n) {p : P}
     (hp : p ∈ affine_span ℝ (set.range s.points)) {r : ℝ} (hr : ∀ i, dist (s.points i) p = r) :
   p = s.circumcenter :=
 begin
-  have h := s.circumcenter_circumradius_unique_dist_eq.2 (p, r),
-  simp only [hp, hr, forall_const, eq_self_iff_true, and_self, prod.ext_iff] at h,
+  have h := s.circumsphere_unique_dist_eq.2 ⟨p, r⟩,
+  simp only [hp, hr, forall_const, eq_self_iff_true, subset_sphere, sphere.ext_iff,
+             set.forall_range_iff, mem_sphere, true_and] at h,
   exact h.1
 end
 
@@ -327,8 +327,9 @@ lemma eq_circumradius_of_dist_eq {n : ℕ} (s : simplex ℝ P n) {p : P}
     (hp : p ∈ affine_span ℝ (set.range s.points)) {r : ℝ} (hr : ∀ i, dist (s.points i) p = r) :
   r = s.circumradius :=
 begin
-  have h := s.circumcenter_circumradius_unique_dist_eq.2 (p, r),
-  simp only [hp, hr, forall_const, eq_self_iff_true, and_self, prod.ext_iff] at h,
+  have h := s.circumsphere_unique_dist_eq.2 ⟨p, r⟩,
+  simp only [hp, hr, forall_const, eq_self_iff_true, subset_sphere, sphere.ext_iff,
+             set.forall_range_iff, mem_sphere, true_and] at h,
   exact h.2
 end
 

src/geometry/euclidean/inversion.lean

@@ -49,7 +49,7 @@ begin
     rwa [dist_ne_zero] }
 end
 
-lemma inversion_of_mem_sphere (h : x ∈ sphere c R) : inversion c R x = x :=
+lemma inversion_of_mem_sphere (h : x ∈ metric.sphere c R) : inversion c R x = x :=
 h.out ▸ inversion_dist_center c x
 
 /-- Distance from the image of a point under inversion to the center. This formula accidentally