-- Mathlib/Geometry/Euclidean/Circumcenter.lean
theorem existsUnique_dist_eq_of_insert {s : AffineSubspace ℝ P}
    [HasOrthogonalProjection s.direction] {ps : Set P} (hnps : ps.Nonempty) {p : P} (hps : ps ⊆ s)
    (hp : p ∉ s) (hu : ∃! cs : Sphere P, cs.center ∈ s ∧ ps ⊆ (cs : Set P)) :
    ∃! cs₂ : Sphere P,
      cs₂.center ∈ affineSpan ℝ (insert p (s : Set P)) ∧ insert p ps ⊆ (cs₂ : Set P)

Proof state:
case 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
inst✝ : HasOrthogonalProjection s.direction
ps : Set P
p : P
hps : ps ⊆ ↑s
hp : p ∉ s
this : Nonempty ↥s
cc : P
cr : ℝ
hcccru : ∀ (y : Sphere P), y.center ∈ s ∧ ps ⊆ Metric.sphere y.center y.radius → y = { center := cc, radius := cr }
hcc : cc ∈ s
hcr : ps ⊆ Metric.sphere cc cr
x : ℝ := dist cc ↑((orthogonalProjection s) p)
y : ℝ := dist p ↑((orthogonalProjection s) p)
hy0 : y ≠ 0
ycc₂ : ℝ := (x * x + y * y - cr * cr) / (2 * y)
cc₂ : P := (ycc₂ / y) • (p -ᵥ ↑((orthogonalProjection s) p)) +ᵥ cc
cr₂ : ℝ := √(cr * cr + ycc₂ * ycc₂)
hpo : p = 1 • (p -ᵥ ↑((orthogonalProjection s) p)) +ᵥ ↑((orthogonalProjection s) p)
cc₃ : P
cr₃ : ℝ
hcc₃ : cc₃ ∈ affineSpan ℝ (insert p ↑s)
hcr₃ : insert p ps ⊆ Metric.sphere cc₃ cr₃
t₃ : ℝ
hcc₃' : cc ∈ s
hcc₃'' : cc₃ = t₃ • (p -ᵥ ↑((orthogonalProjection s) p)) +ᵥ cc
hcr₃' : ∀ p₁ ∈ ps, dist p₁ ↑⟨cc, hcc₃'⟩ = cr
p0 : P
hp0 : p0 ∈ ps
⊢ cr₃ = √(cr * cr + t₃ * y * (t₃ * y))

Tactic:
have h' : ↑(⟨cc, hcc₃'⟩ : s) = cc := rfl

Result:
case 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
inst✝ : HasOrthogonalProjection s.direction
ps : Set P
p : P
hps : ps ⊆ ↑s
hp : p ∉ s
this : Nonempty ↥s
cc : P
cr : ℝ
hcccru : ∀ (y : Sphere P), y.center ∈ s ∧ ps ⊆ Metric.sphere y.center y.radius → y = { center := cc, radius := cr }
hcc : cc ∈ s
hcr : ps ⊆ Metric.sphere cc cr
x : ℝ := dist cc ↑((orthogonalProjection s) p)
y : ℝ := dist p ↑((orthogonalProjection s) p)
hy0 : y ≠ 0
ycc₂ : ℝ := (x * x + y * y - cr * cr) / (2 * y)
cc₂ : P := (ycc₂ / y) • (p -ᵥ ↑((orthogonalProjection s) p)) +ᵥ cc
cr₂ : ℝ := √(cr * cr + ycc₂ * ycc₂)
hpo : p = 1 • (p -ᵥ ↑((orthogonalProjection s) p)) +ᵥ ↑((orthogonalProjection s) p)
cc₃ : P
cr₃ : ℝ
hcc₃ : cc₃ ∈ affineSpan ℝ (insert p ↑s)
hcr₃ : insert p ps ⊆ Metric.sphere cc₃ cr₃
t₃ : ℝ
hcc₃' : cc ∈ s
hcc₃'' : cc₃ = t₃ • (p -ᵥ ↑((orthogonalProjection s) p)) +ᵥ cc
hcr₃' : ∀ p₁ ∈ ps, dist p₁ ↑⟨cc, hcc₃'⟩ = cr
p0 : P
hp0 : p0 ∈ ps
h' : ↑⟨cc, hcc₃'⟩ = cc
⊢ cr₃ = √(cr * cr + t₃ * y * (t₃ * y))

Proof state:
case h.left.left
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝ : HasOrthogonalProjection s.direction
ps : Set P
hnps : ps.Nonempty
p : P
hps : ps ⊆ ↑s
hp : p ∉ s
this : Nonempty ↥s
cc : P
cr : ℝ
hcccru : ∀ (y : Sphere P), y.center ∈ s ∧ ps ⊆ Metric.sphere y.center y.radius → y = { center := cc, radius := cr }
hcc : cc ∈ s
hcr : ps ⊆ Metric.sphere cc cr
x : ℝ := dist cc ↑((orthogonalProjection s) p)
y : ℝ := dist p ↑((orthogonalProjection s) p)
hy0 : y ≠ 0
ycc₂ : ℝ := (x * x + y * y - cr * cr) / (2 * y)
cc₂ : P := (ycc₂ / y) • (p -ᵥ ↑((orthogonalProjection s) p)) +ᵥ cc
cr₂ : ℝ := √(cr * cr + ycc₂ * ycc₂)
hpo : p = 1 • (p -ᵥ ↑((orthogonalProjection s) p)) +ᵥ ↑((orthogonalProjection s) p)
⊢ (ycc₂ / y) • (p -ᵥ ↑((orthogonalProjection s) p)) ∈ (affineSpan ℝ (insert p ↑s)).direction

Tactic:
rw [direction_affineSpan]

Result:
case h.left.left
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝ : HasOrthogonalProjection s.direction
ps : Set P
hnps : ps.Nonempty
p : P
hps : ps ⊆ ↑s
hp : p ∉ s
this : Nonempty ↥s
cc : P
cr : ℝ
hcccru : ∀ (y : Sphere P), y.center ∈ s ∧ ps ⊆ Metric.sphere y.center y.radius → y = { center := cc, radius := cr }
hcc : cc ∈ s
hcr : ps ⊆ Metric.sphere cc cr
x : ℝ := dist cc ↑((orthogonalProjection s) p)
y : ℝ := dist p ↑((orthogonalProjection s) p)
hy0 : y ≠ 0
ycc₂ : ℝ := (x * x + y * y - cr * cr) / (2 * y)
cc₂ : P := (ycc₂ / y) • (p -ᵥ ↑((orthogonalProjection s) p)) +ᵥ cc
cr₂ : ℝ := √(cr * cr + ycc₂ * ycc₂)
hpo : p = 1 • (p -ᵥ ↑((orthogonalProjection s) p)) +ᵥ ↑((orthogonalProjection s) p)
⊢ (ycc₂ / y) • (p -ᵥ ↑((orthogonalProjection s) p)) ∈ vectorSpan ℝ (insert p ↑s)

Proof state:
case h.right.mk.intro.intro.intro.intro.intro.refl
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝ : HasOrthogonalProjection s.direction
ps : Set P
hnps : ps.Nonempty
p : P
hps : ps ⊆ ↑s
hp : p ∉ s
this : Nonempty ↥s
cc : P
cr : ℝ
hcccru : ∀ (y : Sphere P), y.center ∈ s ∧ ps ⊆ Metric.sphere y.center y.radius → y = { center := cc, radius := cr }
hcc : cc ∈ s
hcr : ps ⊆ Metric.sphere cc cr
x : ℝ := dist cc ↑((orthogonalProjection s) p)
y : ℝ := dist p ↑((orthogonalProjection s) p)
hy0 : y ≠ 0
ycc₂ : ℝ := (x * x + y * y - cr * cr) / (2 * y)
cc₂ : P := (ycc₂ / y) • (p -ᵥ ↑((orthogonalProjection s) p)) +ᵥ cc
cr₂ : ℝ := √(cr * cr + ycc₂ * ycc₂)
hpo : p = 1 • (p -ᵥ ↑((orthogonalProjection s) p)) +ᵥ ↑((orthogonalProjection s) p)
cc₃ : P
cr₃ : ℝ
hcc₃ : cc₃ ∈ affineSpan ℝ (insert p ↑s)
t₃ : ℝ
hcc₃' : cc ∈ s
hcc₃'' : cc₃ = t₃ • (p -ᵥ ↑((orthogonalProjection s) p)) +ᵥ cc
hcr₃' : ∀ p₁ ∈ ps, dist p₁ ↑⟨cc, hcc₃'⟩ = cr
hcr₃val : cr₃ = √(cr * cr + t₃ * y * (t₃ * y))
hcr₃ : dist p cc₃ = cr₃
⊢ { center := cc₃, radius := cr₃ } = { center := cc₂, radius := cr₂ }

Tactic:
rw [hpo, hcc₃'', hcr₃val, ← mul_self_inj_of_nonneg dist_nonneg (Real.sqrt_nonneg _),
  dist_sq_smul_orthogonal_vadd_smul_orthogonal_vadd (orthogonalProjection_mem p) hcc₃' _ _
    (vsub_orthogonalProjection_mem_direction_orthogonal s p),
  dist_comm, ← dist_eq_norm_vsub V p,
  Real.mul_self_sqrt (add_nonneg (mul_self_nonneg _) (mul_self_nonneg _))] at hcr₃

Result:
case h.right.mk.intro.intro.intro.intro.intro.refl
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝ : HasOrthogonalProjection s.direction
ps : Set P
hnps : ps.Nonempty
p : P
hps : ps ⊆ ↑s
hp : p ∉ s
this : Nonempty ↥s
cc : P
cr : ℝ
hcccru : ∀ (y : Sphere P), y.center ∈ s ∧ ps ⊆ Metric.sphere y.center y.radius → y = { center := cc, radius := cr }
hcc : cc ∈ s
hcr : ps ⊆ Metric.sphere cc cr
x : ℝ := dist cc ↑((orthogonalProjection s) p)
y : ℝ := dist p ↑((orthogonalProjection s) p)
hy0 : y ≠ 0
ycc₂ : ℝ := (x * x + y * y - cr * cr) / (2 * y)
cc₂ : P := (ycc₂ / y) • (p -ᵥ ↑((orthogonalProjection s) p)) +ᵥ cc
cr₂ : ℝ := √(cr * cr + ycc₂ * ycc₂)
hpo : p = 1 • (p -ᵥ ↑((orthogonalProjection s) p)) +ᵥ ↑((orthogonalProjection s) p)
cc₃ : P
cr₃ : ℝ
hcc₃ : cc₃ ∈ affineSpan ℝ (insert p ↑s)
t₃ : ℝ
hcc₃' : cc ∈ s
hcc₃'' : cc₃ = t₃ • (p -ᵥ ↑((orthogonalProjection s) p)) +ᵥ cc
hcr₃' : ∀ p₁ ∈ ps, dist p₁ ↑⟨cc, hcc₃'⟩ = cr
hcr₃val : cr₃ = √(cr * cr + t₃ * y * (t₃ * y))
hcr₃ :
  dist cc ↑((orthogonalProjection s) p) * dist cc ↑((orthogonalProjection s) p) +
      (1 - t₃) * (1 - t₃) * (dist p ↑((orthogonalProjection s) p) * dist p ↑((orthogonalProjection s) p)) =
    cr * cr + t₃ * y * (t₃ * y)
⊢ { center := cc₃, radius := cr₃ } = { center := cc₂, radius := cr₂ }