awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : AffineSubspace ℝ P
ps : Set P
h : ps ⊆ (↑s : Set P)
inst_4 : Nonempty.{u_2 + 1} ↥s
n : ℕ
inst_5 : FiniteDimensional.{0, u_1} ℝ ↥s.direction
hd : finrank.{0, u_1} ℝ ↥s.direction = n
c : P
hc_1 : c ∈ s
r : ℝ
hcr : ∀ p ∈ ps, dist p c = r
sx : Simplex ℝ P n
hsxps : Set.range sx.points ⊆ ps
hsx : affineSpan ℝ (Set.range sx.points) = s
hc : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range sx.points)) c
⊢ sx.circumradius = r

Tactic:
(sx.eq_circumradius_of_dist_eq hc fun i =>
        hcr (sx.points i) (hsxps (Set.mem_range_self i))).symm

Premises used: Set.mem_range_self, Affine.Simplex.points, Affine.Simplex.eq_circumradius_of_dist_eq, Eq.symm
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : AffineSubspace ℝ P
ps : Set P
h : ps ⊆ (↑s : Set P)
inst_4 : Nonempty.{u_2 + 1} ↥s
n : ℕ
inst_5 : FiniteDimensional.{0, u_1} ℝ ↥s.direction
hd : finrank.{0, u_1} ℝ ↥s.direction = n
c : P
hc_1 : c ∈ s
r : ℝ
hcr : ∀ p ∈ ps, dist p c = r
sx : Simplex ℝ P n
hsxps : Set.range sx.points ⊆ ps
hsx : affineSpan ℝ (Set.range sx.points) = s
hc : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range sx.points)) c
⊢ sx.circumradius = r

Tactic:
exact
    (sx.eq_circumradius_of_dist_eq hc fun i =>
        hcr (sx.points i) (hsxps (Set.mem_range_self i))).symm

Premises used: Set.mem_range_self, Affine.Simplex.points, Affine.Simplex.eq_circumradius_of_dist_eq, Eq.symm
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : AffineSubspace ℝ P
ps : Set P
h : ps ⊆ (↑s : Set P)
inst_4 : Nonempty.{u_2 + 1} ↥s
n : ℕ
inst_5 : FiniteDimensional.{0, u_1} ℝ ↥s.direction
hd : finrank.{0, u_1} ℝ ↥s.direction = n
hc : Cospherical ps
sx₁ sx₂ : Simplex ℝ P n
hsx₁ : Set.range sx₁.points ⊆ ps
hsx₂ : Set.range sx₂.points ⊆ ps
rcases :
  ∀ (r : ℝ) (hr : ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumradius = r),
    sx₁.circumradius = sx₂.circumradius
⊢ sx₁.circumradius = sx₂.circumradius

Tactic:
rcases exists_circumradius_eq_of_cospherical_subset h hd hc with ⟨r, hr⟩

Premises used: EuclideanGeometry.exists_circumradius_eq_of_cospherical_subset
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : AffineSubspace ℝ P
ps : Set P
h : ps ⊆ (↑s : Set P)
inst_4 : Nonempty.{u_2 + 1} ↥s
n : ℕ
inst_5 : FiniteDimensional.{0, u_1} ℝ ↥s.direction
hd : finrank.{0, u_1} ℝ ↥s.direction = n
hc : Cospherical ps
sx₁ sx₂ : Simplex ℝ P n
hsx₁ : Set.range sx₁.points ⊆ ps
hsx₂ : Set.range sx₂.points ⊆ ps
r : ℝ
hr : ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumradius = r
rw : r = sx₂.circumradius
rw₁ rw₂ : r = r
⊢ sx₁.circumradius = sx₂.circumradius

Tactic:
rw [hr sx₁ hsx₁, hr sx₂ hsx₂]
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
ps : Set P
n : ℕ
inst_4 : FiniteDimensional ℝ V
hd : finrank ℝ V = n
hc : Cospherical ps
⊢ finrank.{0, u_1} ℝ ↥(direction.{0, u_1, u_2} (P := P) ⊤) = n

Tactic:
rw [← finrank_top, ← direction_top ℝ V P] at hd

Premises used: Real, AffineSubspace.direction_top, finrank_top
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
ps : Set P
n : ℕ
inst_4 : FiniteDimensional ℝ V
hd : finrank ℝ V = n
hc : Cospherical ps
hd₁ : finrank.{0, u_1} ℝ ↥(direction.{0, u_1, u_2} (P := P) ⊤) = n
⊢ Cospherical ps

Tactic:
rw [← finrank_top, ← direction_top ℝ V P] at hd

Premises used: Real, AffineSubspace.direction_top, finrank_top
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
ps : Set P
n : ℕ
inst_4 : FiniteDimensional ℝ V
hd : finrank.{0, u_1} ℝ ↥(direction.{0, u_1, u_2} (P := P) ⊤) = n
hc : Cospherical ps
⊢ ∃ (r : ℝ), ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumradius = r

Tactic:
exists_circumradius_eq_of_cospherical_subset ?_ hd hc

Premises used: EuclideanGeometry.exists_circumradius_eq_of_cospherical_subset
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
ps : Set P
n : ℕ
inst_4 : FiniteDimensional ℝ V
hd : finrank.{0, u_1} ℝ ↥(direction.{0, u_1, u_2} (P := P) ⊤) = n
hc : Cospherical ps
refine : ps ⊆ (↑⊤ : Set P)
⊢ ∃ (r : ℝ), ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumradius = r

Tactic:
refine exists_circumradius_eq_of_cospherical_subset ?_ hd hc

Premises used: EuclideanGeometry.exists_circumradius_eq_of_cospherical_subset
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
ps : Set P
n : ℕ
inst_4 : FiniteDimensional ℝ V
hd : finrank.{0, u_1} ℝ ↥(direction.{0, u_1, u_2} (P := P) ⊤) = n
hc : Cospherical ps
⊢ ps ⊆ (↑⊤ : Set P)

Tactic:
Set.subset_univ _

Premises used: Set.subset_univ, Set.univ, setOf
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
ps : Set P
n : ℕ
inst_4 : FiniteDimensional ℝ V
hd : finrank.{0, u_1} ℝ ↥(direction.{0, u_1, u_2} (P := P) ⊤) = n
hc : Cospherical ps
⊢ ps ⊆ (↑⊤ : Set P)

Tactic:
exact Set.subset_univ _

Premises used: Set.subset_univ
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
ps : Set P
n : ℕ
inst_4 : FiniteDimensional ℝ V
hd : finrank ℝ V = n
hc : Cospherical ps
sx₁ sx₂ : Simplex ℝ P n
hsx₁ : Set.range sx₁.points ⊆ ps
hsx₂ : Set.range sx₂.points ⊆ ps
rcases :
  ∀ (r : ℝ) (hr : ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumradius = r),
    sx₁.circumradius = sx₂.circumradius
⊢ sx₁.circumradius = sx₂.circumradius

Tactic:
rcases exists_circumradius_eq_of_cospherical hd hc with ⟨r, hr⟩

Premises used: EuclideanGeometry.exists_circumradius_eq_of_cospherical
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
ps : Set P
n : ℕ
inst_4 : FiniteDimensional ℝ V
hd : finrank ℝ V = n
hc : Cospherical ps
sx₁ sx₂ : Simplex ℝ P n
hsx₁ : Set.range sx₁.points ⊆ ps
hsx₂ : Set.range sx₂.points ⊆ ps
r : ℝ
hr : ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumradius = r
rw : r = sx₂.circumradius
rw₁ rw₂ : r = r
⊢ sx₁.circumradius = sx₂.circumradius

Tactic:
rw [hr sx₁ hsx₁, hr sx₂ hsx₂]
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : AffineSubspace ℝ P
ps : Set P
h : ps ⊆ (↑s : Set P)
inst_4 : Nonempty.{u_2 + 1} ↥s
n : ℕ
inst_5 : FiniteDimensional.{0, u_1} ℝ ↥s.direction
hd : finrank.{0, u_1} ℝ ↥s.direction = n
hc : ∃ center ∈ s, ∃ (radius : ℝ), ∀ p ∈ ps, dist p center = radius
rcases :
  ∀ (c : P) (hc : c ∈ s) (r : ℝ) (hcr : ∀ p ∈ ps, dist p c = r),
    ∃ (c : P), ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumcenter = c
⊢ ∃ (c : P), ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumcenter = c

Tactic:
rcases hc with ⟨c, hc, r, hcr⟩
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : AffineSubspace ℝ P
ps : Set P
h : ps ⊆ (↑s : Set P)
inst_4 : Nonempty.{u_2 + 1} ↥s
n : ℕ
inst_5 : FiniteDimensional.{0, u_1} ℝ ↥s.direction
hd : finrank.{0, u_1} ℝ ↥s.direction = n
c : P
hc : c ∈ s
r : ℝ
hcr : ∀ p ∈ ps, dist p c = r
h₁ : ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumcenter = c
⊢ ∃ (c : P), ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumcenter = c

Tactic:
use c
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : AffineSubspace ℝ P
ps : Set P
h : ps ⊆ (↑s : Set P)
inst_4 : Nonempty.{u_2 + 1} ↥s
n : ℕ
inst_5 : FiniteDimensional.{0, u_1} ℝ ↥s.direction
hd : finrank.{0, u_1} ℝ ↥s.direction = n
c : P
hc_1 : c ∈ s
r : ℝ
hcr : ∀ p ∈ ps, dist p c = r
sx : Simplex ℝ P n
hsxps : Set.range sx.points ⊆ ps
hsx : affineSpan ℝ (Set.range sx.points) = s
hc : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range sx.points)) c
⊢ sx.circumcenter = c

Tactic:
(sx.eq_circumcenter_of_dist_eq hc fun i =>
        hcr (sx.points i) (hsxps (Set.mem_range_self i))).symm

Premises used: Set.mem_range_self, Affine.Simplex.points, Eq.symm, Affine.Simplex.eq_circumcenter_of_dist_eq
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : AffineSubspace ℝ P
ps : Set P
h : ps ⊆ (↑s : Set P)
inst_4 : Nonempty.{u_2 + 1} ↥s
n : ℕ
inst_5 : FiniteDimensional.{0, u_1} ℝ ↥s.direction
hd : finrank.{0, u_1} ℝ ↥s.direction = n
c : P
hc_1 : c ∈ s
r : ℝ
hcr : ∀ p ∈ ps, dist p c = r
sx : Simplex ℝ P n
hsxps : Set.range sx.points ⊆ ps
hsx : affineSpan ℝ (Set.range sx.points) = s
hc : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range sx.points)) c
⊢ sx.circumcenter = c

Tactic:
exact
    (sx.eq_circumcenter_of_dist_eq hc fun i =>
        hcr (sx.points i) (hsxps (Set.mem_range_self i))).symm

Premises used: Set.mem_range_self, Affine.Simplex.points, Eq.symm, Affine.Simplex.eq_circumcenter_of_dist_eq
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : AffineSubspace ℝ P
ps : Set P
h : ps ⊆ (↑s : Set P)
inst_4 : Nonempty.{u_2 + 1} ↥s
n : ℕ
inst_5 : FiniteDimensional.{0, u_1} ℝ ↥s.direction
hd : finrank.{0, u_1} ℝ ↥s.direction = n
hc : Cospherical ps
sx₁ sx₂ : Simplex ℝ P n
hsx₁ : Set.range sx₁.points ⊆ ps
hsx₂ : Set.range sx₂.points ⊆ ps
rcases :
  ∀ (r : P) (hr : ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumcenter = r),
    sx₁.circumcenter = sx₂.circumcenter
⊢ sx₁.circumcenter = sx₂.circumcenter

Tactic:
rcases exists_circumcenter_eq_of_cospherical_subset h hd hc with ⟨r, hr⟩

Premises used: EuclideanGeometry.exists_circumcenter_eq_of_cospherical_subset
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : AffineSubspace ℝ P
ps : Set P
h : ps ⊆ (↑s : Set P)
inst_4 : Nonempty.{u_2 + 1} ↥s
n : ℕ
inst_5 : FiniteDimensional.{0, u_1} ℝ ↥s.direction
hd : finrank.{0, u_1} ℝ ↥s.direction = n
hc : Cospherical ps
sx₁ sx₂ : Simplex ℝ P n
hsx₁ : Set.range sx₁.points ⊆ ps
hsx₂ : Set.range sx₂.points ⊆ ps
r : P
hr : ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumcenter = r
rw : r = sx₂.circumcenter
rw₁ rw₂ : r = r
⊢ sx₁.circumcenter = sx₂.circumcenter

Tactic:
rw [hr sx₁ hsx₁, hr sx₂ hsx₂]
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
ps : Set P
n : ℕ
inst_4 : FiniteDimensional ℝ V
hd : finrank.{0, u_1} ℝ ↥(direction.{0, u_1, u_2} (P := P) ⊤) = n
hc : Cospherical ps
⊢ ∃ (c : P), ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumcenter = c

Tactic:
exists_circumcenter_eq_of_cospherical_subset ?_ hd hc

Premises used: EuclideanGeometry.exists_circumcenter_eq_of_cospherical_subset
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
ps : Set P
n : ℕ
inst_4 : FiniteDimensional ℝ V
hd : finrank.{0, u_1} ℝ ↥(direction.{0, u_1, u_2} (P := P) ⊤) = n
hc : Cospherical ps
refine : ps ⊆ (↑⊤ : Set P)
⊢ ∃ (c : P), ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumcenter = c

Tactic:
refine exists_circumcenter_eq_of_cospherical_subset ?_ hd hc

Premises used: EuclideanGeometry.exists_circumcenter_eq_of_cospherical_subset
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
ps : Set P
n : ℕ
inst_4 : FiniteDimensional ℝ V
hd : finrank ℝ V = n
hc : Cospherical ps
sx₁ sx₂ : Simplex ℝ P n
hsx₁ : Set.range sx₁.points ⊆ ps
hsx₂ : Set.range sx₂.points ⊆ ps
rcases :
  ∀ (r : P) (hr : ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumcenter = r),
    sx₁.circumcenter = sx₂.circumcenter
⊢ sx₁.circumcenter = sx₂.circumcenter

Tactic:
rcases exists_circumcenter_eq_of_cospherical hd hc with ⟨r, hr⟩

Premises used: EuclideanGeometry.exists_circumcenter_eq_of_cospherical
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
ps : Set P
n : ℕ
inst_4 : FiniteDimensional ℝ V
hd : finrank ℝ V = n
hc : Cospherical ps
sx₁ sx₂ : Simplex ℝ P n
hsx₁ : Set.range sx₁.points ⊆ ps
hsx₂ : Set.range sx₂.points ⊆ ps
r : P
hr : ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumcenter = r
rw : r = sx₂.circumcenter
rw₁ rw₂ : r = r
⊢ sx₁.circumcenter = sx₂.circumcenter

Tactic:
rw [hr sx₁ hsx₁, hr sx₂ hsx₂]
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : AffineSubspace ℝ P
ps : Set P
h : ps ⊆ (↑s : Set P)
inst_4 : Nonempty.{u_2 + 1} ↥s
n : ℕ
inst_5 : FiniteDimensional.{0, u_1} ℝ ↥s.direction
hd : finrank.{0, u_1} ℝ ↥s.direction = n
hc : Cospherical ps
obtain :
  ∀ (r : ℝ) (hr : ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumradius = r),
    ∃ (c : Sphere P), ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumsphere = c
⊢ ∃ (c : Sphere P), ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumsphere = c

Tactic:
obtain ⟨r, hr⟩ := exists_circumradius_eq_of_cospherical_subset h hd hc

Premises used: EuclideanGeometry.exists_circumradius_eq_of_cospherical_subset
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : AffineSubspace ℝ P
ps : Set P
h : ps ⊆ (↑s : Set P)
inst_4 : Nonempty.{u_2 + 1} ↥s
n : ℕ
inst_5 : FiniteDimensional.{0, u_1} ℝ ↥s.direction
hd : finrank.{0, u_1} ℝ ↥s.direction = n
hc : Cospherical ps
r : ℝ
hr : ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumradius = r
obtain :
  ∀ (c : P) (hc : ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumcenter = c),
    ∃ (c : Sphere P), ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumsphere = c
⊢ ∃ (c : Sphere P), ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumsphere = c

Tactic:
obtain ⟨c, hc⟩ := exists_circumcenter_eq_of_cospherical_subset h hd hc

Premises used: EuclideanGeometry.exists_circumcenter_eq_of_cospherical_subset
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : AffineSubspace ℝ P
ps : Set P
h : ps ⊆ (↑s : Set P)
inst_4 : Nonempty.{u_2 + 1} ↥s
n : ℕ
inst_5 : FiniteDimensional.{0, u_1} ℝ ↥s.direction
hd : finrank.{0, u_1} ℝ ↥s.direction = n
hc_1 : Cospherical ps
r : ℝ
hr : ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumradius = r
c : P
hc : ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumcenter = c
⊢ ∃ (c : Sphere P), ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumsphere = c

Tactic:
⟨⟨c, r⟩, fun sx hsx => Sphere.ext (hc sx hsx) (hr sx hsx)⟩

Premises used: EuclideanGeometry.Sphere.ext, EuclideanGeometry.Sphere.mk, Exists.intro
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : AffineSubspace ℝ P
ps : Set P
h : ps ⊆ (↑s : Set P)
inst_4 : Nonempty.{u_2 + 1} ↥s
n : ℕ
inst_5 : FiniteDimensional.{0, u_1} ℝ ↥s.direction
hd : finrank.{0, u_1} ℝ ↥s.direction = n
hc_1 : Cospherical ps
r : ℝ
hr : ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumradius = r
c : P
hc : ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumcenter = c
⊢ ∃ (c : Sphere P), ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumsphere = c

Tactic:
exact ⟨⟨c, r⟩, fun sx hsx => Sphere.ext (hc sx hsx) (hr sx hsx)⟩
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : AffineSubspace ℝ P
ps : Set P
h : ps ⊆ (↑s : Set P)
inst_4 : Nonempty.{u_2 + 1} ↥s
n : ℕ
inst_5 : FiniteDimensional.{0, u_1} ℝ ↥s.direction
hd : finrank.{0, u_1} ℝ ↥s.direction = n
hc : Cospherical ps
sx₁ sx₂ : Simplex ℝ P n
hsx₁ : Set.range sx₁.points ⊆ ps
hsx₂ : Set.range sx₂.points ⊆ ps
rcases :
  ∀ (r : Sphere P) (hr : ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumsphere = r),
    sx₁.circumsphere = sx₂.circumsphere
⊢ sx₁.circumsphere = sx₂.circumsphere

Tactic:
rcases exists_circumsphere_eq_of_cospherical_subset h hd hc with ⟨r, hr⟩

Premises used: EuclideanGeometry.exists_circumsphere_eq_of_cospherical_subset
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : AffineSubspace ℝ P
ps : Set P
h : ps ⊆ (↑s : Set P)
inst_4 : Nonempty.{u_2 + 1} ↥s
n : ℕ
inst_5 : FiniteDimensional.{0, u_1} ℝ ↥s.direction
hd : finrank.{0, u_1} ℝ ↥s.direction = n
hc : Cospherical ps
sx₁ sx₂ : Simplex ℝ P n
hsx₁ : Set.range sx₁.points ⊆ ps
hsx₂ : Set.range sx₂.points ⊆ ps
r : Sphere P
hr : ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumsphere = r
rw : r = sx₂.circumsphere
rw₁ rw₂ : r = r
⊢ sx₁.circumsphere = sx₂.circumsphere

Tactic:
rw [hr sx₁ hsx₁, hr sx₂ hsx₂]
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
ps : Set P
n : ℕ
inst_4 : FiniteDimensional ℝ V
hd : finrank.{0, u_1} ℝ ↥(direction.{0, u_1, u_2} (P := P) ⊤) = n
hc : Cospherical ps
⊢ ∃ (c : Sphere P), ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumsphere = c

Tactic:
exists_circumsphere_eq_of_cospherical_subset ?_ hd hc

Premises used: EuclideanGeometry.exists_circumsphere_eq_of_cospherical_subset
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
ps : Set P
n : ℕ
inst_4 : FiniteDimensional ℝ V
hd : finrank.{0, u_1} ℝ ↥(direction.{0, u_1, u_2} (P := P) ⊤) = n
hc : Cospherical ps
refine : ps ⊆ (↑⊤ : Set P)
⊢ ∃ (c : Sphere P), ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumsphere = c

Tactic:
refine exists_circumsphere_eq_of_cospherical_subset ?_ hd hc

Premises used: EuclideanGeometry.exists_circumsphere_eq_of_cospherical_subset
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
ps : Set P
n : ℕ
inst_4 : FiniteDimensional ℝ V
hd : finrank ℝ V = n
hc : Cospherical ps
sx₁ sx₂ : Simplex ℝ P n
hsx₁ : Set.range sx₁.points ⊆ ps
hsx₂ : Set.range sx₂.points ⊆ ps
rcases :
  ∀ (r : Sphere P) (hr : ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumsphere = r),
    sx₁.circumsphere = sx₂.circumsphere
⊢ sx₁.circumsphere = sx₂.circumsphere

Tactic:
rcases exists_circumsphere_eq_of_cospherical hd hc with ⟨r, hr⟩

Premises used: EuclideanGeometry.exists_circumsphere_eq_of_cospherical
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
ps : Set P
n : ℕ
inst_4 : FiniteDimensional ℝ V
hd : finrank ℝ V = n
hc : Cospherical ps
sx₁ sx₂ : Simplex ℝ P n
hsx₁ : Set.range sx₁.points ⊆ ps
hsx₂ : Set.range sx₂.points ⊆ ps
r : Sphere P
hr : ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumsphere = r
rw : r = sx₂.circumsphere
rw₁ rw₂ : r = r
⊢ sx₁.circumsphere = sx₂.circumsphere

Tactic:
rw [hr sx₁ hsx₁, hr sx₂ hsx₂]
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P n
p p₁ p₂ : P
r : ℝ
hp₁ : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (insert p (Set.range s.points))) p₁
hp₂ : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (insert p (Set.range s.points))) p₂
h₁ : ∀ (i : Fin (n + 1)), dist (s.points i) p₁ = r
h₂ : ∀ (i : Fin (n + 1)), dist (s.points i) p₂ = r
span_s : AffineSubspace ℝ P := affineSpan ℝ (Set.range s.points)
⊢ (↑((s.orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range s.points))) p₁) : P) = s.circumcenter

Tactic:
have h₁' := s.orthogonalProjection_eq_circumcenter_of_dist_eq h₁
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P n
p p₁ p₂ : P
r : ℝ
hp₁ : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (insert p (Set.range s.points))) p₁
hp₂ : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (insert p (Set.range s.points))) p₂
h₁ : ∀ (i : Fin (n + 1)), dist (s.points i) p₁ = r
h₂ : ∀ (i : Fin (n + 1)), dist (s.points i) p₂ = r
span_s : AffineSubspace ℝ P := affineSpan ℝ (Set.range s.points)
h₁' : (↑((s.orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range s.points))) p₁) : P) = s.circumcenter
⊢ (↑((s.orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range s.points))) p₂) : P) = s.circumcenter

Tactic:
have h₂' := s.orthogonalProjection_eq_circumcenter_of_dist_eq h₂