case refine'_1
V : Type ?u.6464
P : Type u_1
inst✝ : MetricSpace P
ps : Set P
h : Cospherical ps
⊢ ∃ s, ps ⊆ Metric.sphere s.center s.radius

case refine'_2
V : Type ?u.6464
P : Type u_1
inst✝ : MetricSpace P
ps : Set P
h : ∃ s, ps ⊆ Metric.sphere s.center s.radius
⊢ Cospherical ps
V : Type ?u.6464
P : Type u_1
inst✝ : MetricSpace P
ps : Set P
⊢ Cospherical ps ↔ ∃ s, ps ⊆ Metric.sphere s.center s.radius
refine' ⟨fun h => _, fun h => _⟩
case refine'_1.intro.intro
V : Type ?u.6464
P : Type u_1
inst✝ : MetricSpace P
ps : Set P
c : P
r : ℝ
h : ∀ (p : P), p ∈ ps → dist p c = r
⊢ ∃ s, ps ⊆ Metric.sphere s.center s.radius
case refine'_1
V : Type ?u.6464
P : Type u_1
inst✝ : MetricSpace P
ps : Set P
h : Cospherical ps
⊢ ∃ s, ps ⊆ Metric.sphere s.center s.radius
rcases h with ⟨c, r, h⟩
no goals
case refine'_1.intro.intro
V : Type ?u.6464
P : Type u_1
inst✝ : MetricSpace P
ps : Set P
c : P
r : ℝ
h : ∀ (p : P), p ∈ ps → dist p c = r
⊢ ∃ s, ps ⊆ Metric.sphere s.center s.radius
exact ⟨⟨c, r⟩, h⟩
case refine'_2.intro
V : Type ?u.6464
P : Type u_1
inst✝ : MetricSpace P
ps : Set P
s : Sphere P
h : ps ⊆ Metric.sphere s.center s.radius
⊢ Cospherical ps
case refine'_2
V : Type ?u.6464
P : Type u_1
inst✝ : MetricSpace P
ps : Set P
h : ∃ s, ps ⊆ Metric.sphere s.center s.radius
⊢ Cospherical ps
rcases h with ⟨s, h⟩
no goals
case refine'_2.intro
V : Type ?u.6464
P : Type u_1
inst✝ : MetricSpace P
ps : Set P
s : Sphere P
h : ps ⊆ Metric.sphere s.center s.radius
⊢ Cospherical ps
exact ⟨s.center, s.radius, h⟩