-- Mathlib/Geometry/Euclidean/Circumcenter.lean
theorem cospherical_iff_exists_mem_of_complete {s : AffineSubspace ℝ P} {ps : Set P} (h : ps ⊆ s)
    [Nonempty s] [HasOrthogonalProjection s.direction] :
    Cospherical ps ↔ ∃ center ∈ s, ∃ radius : ℝ, ∀ p ∈ ps, dist p center = radius

Proof state:
case mp
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
ps : Set P
h : ps ⊆ ↑s
inst✝¹ : Nonempty ↥s
inst✝ : HasOrthogonalProjection s.direction
⊢ Cospherical ps → ∃ center ∈ s, ∃ radius, ∀ p ∈ ps, dist p center = radius

Tactic:
rintro ⟨c, hcr⟩

Result:
case mp.intro
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
ps : Set P
h : ps ⊆ ↑s
inst✝¹ : Nonempty ↥s
inst✝ : HasOrthogonalProjection s.direction
c : P
hcr : ∃ radius, ∀ p ∈ ps, dist p c = radius
⊢ ∃ center ∈ s, ∃ radius, ∀ p ∈ ps, dist p center = radius

Proof state:
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
ps : Set P
h : ps ⊆ ↑s
inst✝¹ : Nonempty ↥s
inst✝ : HasOrthogonalProjection s.direction
⊢ Cospherical ps ↔ ∃ center ∈ s, ∃ radius, ∀ p ∈ ps, dist p center = radius

Tactic:
constructor

Result:
case mp
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
ps : Set P
h : ps ⊆ ↑s
inst✝¹ : Nonempty ↥s
inst✝ : HasOrthogonalProjection s.direction
⊢ Cospherical ps → ∃ center ∈ s, ∃ radius, ∀ p ∈ ps, dist p center = radius

case mpr
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
ps : Set P
h : ps ⊆ ↑s
inst✝¹ : Nonempty ↥s
inst✝ : HasOrthogonalProjection s.direction
⊢ (∃ center ∈ s, ∃ radius, ∀ p ∈ ps, dist p center = radius) → Cospherical ps

Proof state:
case mp.intro
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
ps : Set P
h : ps ⊆ ↑s
inst✝¹ : Nonempty ↥s
inst✝ : HasOrthogonalProjection s.direction
c : P
hcr : ∃ r, ∀ p₁ ∈ ps, dist p₁ ↑((orthogonalProjection s) c) = r
⊢ ∃ center ∈ s, ∃ radius, ∀ p ∈ ps, dist p center = radius

Tactic:
exact ⟨orthogonalProjection s c, orthogonalProjection_mem _, hcr⟩

Result:
no goals

Proof state:
case mp.intro
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
ps : Set P
h : ps ⊆ ↑s
inst✝¹ : Nonempty ↥s
inst✝ : HasOrthogonalProjection s.direction
c : P
hcr : ∃ radius, ∀ p ∈ ps, dist p c = radius
⊢ ∃ center ∈ s, ∃ radius, ∀ p ∈ ps, dist p center = radius

Tactic:
rw [exists_dist_eq_iff_exists_dist_orthogonalProjection_eq h c] at hcr

Result:
case mp.intro
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
ps : Set P
h : ps ⊆ ↑s
inst✝¹ : Nonempty ↥s
inst✝ : HasOrthogonalProjection s.direction
c : P
hcr : ∃ r, ∀ p₁ ∈ ps, dist p₁ ↑((orthogonalProjection s) c) = r
⊢ ∃ center ∈ s, ∃ radius, ∀ p ∈ ps, dist p center = radius

Proof state:
case mpr
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
ps : Set P
h : ps ⊆ ↑s
inst✝¹ : Nonempty ↥s
inst✝ : HasOrthogonalProjection s.direction
⊢ (∃ center ∈ s, ∃ radius, ∀ p ∈ ps, dist p center = radius) → Cospherical ps

Tactic:
exact fun ⟨c, _, hd⟩ => ⟨c, hd⟩

Result:
no goals