diff --git a/src/geometry/euclidean/basic.lean b/src/geometry/euclidean/basic.lean
index d7a4d6bbc8e23..bbc3264657584 100644
--- a/src/geometry/euclidean/basic.lean
+++ b/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
diff --git a/src/geometry/euclidean/circumcenter.lean b/src/geometry/euclidean/circumcenter.lean
index 69ada84e2f8bf..9d1f9f40241c2 100644
--- a/src/geometry/euclidean/circumcenter.lean
+++ b/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
 
diff --git a/src/geometry/euclidean/inversion.lean b/src/geometry/euclidean/inversion.lean
index 0ad5c99bb4357..e9dd02b11c4b0 100644
--- a/src/geometry/euclidean/inversion.lean
+++ b/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