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
inst_4 : s.direction.HasOrthogonalProjection
ps : Set P
hnps : ps.Nonempty
p : P
hps : ps ⊆ (↑s : Set P)
hp : p ∉ s
this : Nonempty.{u_2 + 1} ↥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 : (a : P) → ↥s) p) : P)
y : ℝ := dist p (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)
hy0 : y ≠ 0
ycc₂ : ℝ := (x * x + y * y - cr * cr) / (2 * y)
cc₂ : P := (ycc₂ / y) • (p -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)) +ᵥ cc
cr₂ : ℝ := √(cr * cr + ycc₂ * ycc₂)
hpo :
  p =
    HVAdd.hVAdd (β := P) (HSMul.hSMul (α := ℝ) 1 (p -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)))
      (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)
h :
  Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (insert p (↑s : Set P)))
      (Sphere.center { center := cc₂, radius := cr₂ : Sphere P }) ∧
    insert p ps ⊆
      Metric.sphere (Sphere.center { center := cc₂, radius := cr₂ }) (Sphere.radius { center := cc₂, radius := cr₂ })
h₁ :
  ∀ (y : Sphere P),
    Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (insert p (↑s : Set P))) y.center ∧
        insert p ps ⊆ Metric.sphere y.center y.radius →
      y = { center := cc₂, radius := cr₂ }
⊢ (Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (insert p (↑s : Set P)))
        (Sphere.center { center := cc₂, radius := cr₂ : Sphere P }) ∧
      insert p ps ⊆
        Metric.sphere (Sphere.center { center := cc₂, radius := cr₂ })
          (Sphere.radius { center := cc₂, radius := cr₂ })) ∧
    ∀ (y : Sphere P),
      Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (insert p (↑s : Set P))) y.center ∧
          insert p ps ⊆ Metric.sphere y.center y.radius →
        y = { center := cc₂, radius := cr₂ }

Tactic:
constructor
-- 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
inst_4 : s.direction.HasOrthogonalProjection
ps : Set P
hnps : ps.Nonempty
p : P
hps : ps ⊆ (↑s : Set P)
hp : p ∉ s
this : Nonempty.{u_2 + 1} ↥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 : (a : P) → ↥s) p) : P)
y : ℝ := dist p (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)
hy0 : y ≠ 0
ycc₂ : ℝ := (x * x + y * y - cr * cr) / (2 * y)
cc₂ : P := (ycc₂ / y) • (p -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)) +ᵥ cc
cr₂ : ℝ := √(cr * cr + ycc₂ * ycc₂)
hpo :
  p =
    HVAdd.hVAdd (β := P) (HSMul.hSMul (α := ℝ) 1 (p -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)))
      (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)
h :
  Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (insert p (↑s : Set P)))
    (Sphere.center { center := cc₂, radius := cr₂ : Sphere P })
h₁ :
  insert p ps ⊆
    Metric.sphere (Sphere.center { center := cc₂, radius := cr₂ }) (Sphere.radius { center := cc₂, radius := cr₂ })
⊢ Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (insert p (↑s : Set P)))
      (Sphere.center { center := cc₂, radius := cr₂ : Sphere P }) ∧
    insert p ps ⊆
      Metric.sphere (Sphere.center { center := cc₂, radius := cr₂ }) (Sphere.radius { center := cc₂, radius := cr₂ })

Tactic:
constructor
-- 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
inst_4 : s.direction.HasOrthogonalProjection
ps : Set P
hnps : ps.Nonempty
p : P
hps : ps ⊆ (↑s : Set P)
hp : p ∉ s
this : Nonempty.{u_2 + 1} ↥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 : (a : P) → ↥s) p) : P)
y : ℝ := dist p (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)
hy0 : y ≠ 0
ycc₂ : ℝ := (x * x + y * y - cr * cr) / (2 * y)
cc₂ : P := (ycc₂ / y) • (p -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)) +ᵥ cc
cr₂ : ℝ := √(cr * cr + ycc₂ * ycc₂)
hpo :
  p =
    HVAdd.hVAdd (β := P) (HSMul.hSMul (α := ℝ) 1 (p -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)))
      (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)
⊢ Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (insert p (↑s : Set P)))
    (Sphere.center { center := cc₂, radius := cr₂ : Sphere P })

Tactic:
vadd_mem_of_mem_direction ?_ (mem_affineSpan ℝ (Set.mem_insert_of_mem _ hcc))

Premises used: Real, Set.Mem, Set.mem_insert_of_mem, mem_affineSpan, AffineSubspace.vadd_mem_of_mem_direction
-- 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
inst_4 : s.direction.HasOrthogonalProjection
ps : Set P
hnps : ps.Nonempty
p : P
hps : ps ⊆ (↑s : Set P)
hp : p ∉ s
this : Nonempty.{u_2 + 1} ↥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 : (a : P) → ↥s) p) : P)
y : ℝ := dist p (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)
hy0 : y ≠ 0
ycc₂ : ℝ := (x * x + y * y - cr * cr) / (2 * y)
cc₂ : P := (ycc₂ / y) • (p -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)) +ᵥ cc
cr₂ : ℝ := √(cr * cr + ycc₂ * ycc₂)
hpo :
  p =
    HVAdd.hVAdd (β := P) (HSMul.hSMul (α := ℝ) 1 (p -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)))
      (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)
h :
  Membership.mem (γ := Submodule ℝ V) (direction (affineSpan ℝ (insert p (↑s : Set P))))
    ((ycc₂ / y) • (p -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)))
⊢ Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (insert p (↑s : Set P)))
    (Sphere.center { center := cc₂, radius := cr₂ : Sphere P })

Tactic:
refine vadd_mem_of_mem_direction ?_ (mem_affineSpan ℝ (Set.mem_insert_of_mem _ hcc))

Premises used: Real, Set.mem_insert_of_mem, mem_affineSpan, AffineSubspace.vadd_mem_of_mem_direction
-- 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
inst_4 : s.direction.HasOrthogonalProjection
ps : Set P
hnps : ps.Nonempty
p : P
hps : ps ⊆ (↑s : Set P)
hp : p ∉ s
this : Nonempty.{u_2 + 1} ↥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 : (a : P) → ↥s) p) : P)
y : ℝ := dist p (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)
hy0 : y ≠ 0
ycc₂ : ℝ := (x * x + y * y - cr * cr) / (2 * y)
cc₂ : P := (ycc₂ / y) • (p -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)) +ᵥ cc
cr₂ : ℝ := √(cr * cr + ycc₂ * ycc₂)
hpo :
  p =
    HVAdd.hVAdd (β := P) (HSMul.hSMul (α := ℝ) 1 (p -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)))
      (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)
h :
  Membership.mem (γ := Submodule ℝ V) (vectorSpan ℝ (insert p (↑s : Set P)))
    ((ycc₂ / y) • (p -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)))
⊢ Membership.mem (γ := Submodule ℝ V) (direction (affineSpan ℝ (insert p (↑s : Set P))))
    ((ycc₂ / y) • (p -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)))

Tactic:
rw [direction_affineSpan]

Premises used: direction_affineSpan
-- 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
inst_4 : s.direction.HasOrthogonalProjection
ps : Set P
hnps : ps.Nonempty
p : P
hps : ps ⊆ (↑s : Set P)
hp : p ∉ s
this : Nonempty.{u_2 + 1} ↥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 : (a : P) → ↥s) p) : P)
y : ℝ := dist p (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)
hy0 : y ≠ 0
ycc₂ : ℝ := (x * x + y * y - cr * cr) / (2 * y)
cc₂ : P := (ycc₂ / y) • (p -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)) +ᵥ cc
cr₂ : ℝ := √(cr * cr + ycc₂ * ycc₂)
hpo :
  p =
    HVAdd.hVAdd (β := P) (HSMul.hSMul (α := ℝ) 1 (p -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)))
      (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)
⊢ Membership.mem (γ := Submodule ℝ V) (vectorSpan ℝ (insert p (↑s : Set P)))
    ((ycc₂ / y) • (p -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)))

Tactic:
Submodule.smul_mem _ _
          (vsub_mem_vectorSpan ℝ (Set.mem_insert _ _)
            (Set.mem_insert_of_mem _ (orthogonalProjection_mem _)))

Premises used: vsub_mem_vectorSpan, Real, Set.Mem, Set.mem_insert_of_mem, EuclideanGeometry.orthogonalProjection_mem, Set.mem_insert, Submodule.smul_mem
-- 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
inst_4 : s.direction.HasOrthogonalProjection
ps : Set P
hnps : ps.Nonempty
p : P
hps : ps ⊆ (↑s : Set P)
hp : p ∉ s
this : Nonempty.{u_2 + 1} ↥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 : (a : P) → ↥s) p) : P)
y : ℝ := dist p (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)
hy0 : y ≠ 0
ycc₂ : ℝ := (x * x + y * y - cr * cr) / (2 * y)
cc₂ : P := (ycc₂ / y) • (p -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)) +ᵥ cc
cr₂ : ℝ := √(cr * cr + ycc₂ * ycc₂)
hpo :
  p =
    HVAdd.hVAdd (β := P) (HSMul.hSMul (α := ℝ) 1 (p -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)))
      (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)
⊢ Membership.mem (γ := Submodule ℝ V) (vectorSpan ℝ (insert p (↑s : Set P)))
    ((ycc₂ / y) • (p -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)))

Tactic:
exact
        Submodule.smul_mem _ _
          (vsub_mem_vectorSpan ℝ (Set.mem_insert _ _)
            (Set.mem_insert_of_mem _ (orthogonalProjection_mem _)))

Premises used: vsub_mem_vectorSpan, Real, Set.mem_insert_of_mem, EuclideanGeometry.orthogonalProjection_mem, Set.mem_insert, Submodule.smul_mem
-- 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
inst_4 : s.direction.HasOrthogonalProjection
ps : Set P
hnps : ps.Nonempty
p : P
hps : ps ⊆ (↑s : Set P)
hp : p ∉ s
this : Nonempty.{u_2 + 1} ↥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 : (a : P) → ↥s) p) : P)
y : ℝ := dist p (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)
hy0 : y ≠ 0
ycc₂ : ℝ := (x * x + y * y - cr * cr) / (2 * y)
cc₂ : P := (ycc₂ / y) • (p -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)) +ᵥ cc
cr₂ : ℝ := √(cr * cr + ycc₂ * ycc₂)
hpo :
  p =
    HVAdd.hVAdd (β := P) (HSMul.hSMul (α := ℝ) 1 (p -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)))
      (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)
p₁ : P
hp₁ : p₁ ∈ insert p ps
h :
  dist p₁ (Sphere.center { center := cc₂, radius := cr₂ : Sphere P }) *
      dist p₁ (Sphere.center { center := cc₂, radius := cr₂ : Sphere P }) =
    cr * cr + ycc₂ * ycc₂
⊢ p₁ ∈
    Metric.sphere (Sphere.center { center := cc₂, radius := cr₂ : Sphere P })
      (Sphere.radius { center := cc₂, radius := cr₂ : Sphere P })

Tactic:
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 _))]

Premises used: mul_self_nonneg, mul_self_inj_of_nonneg, dist_nonneg, Real.mul_self_sqrt, add_nonneg, EuclideanGeometry.mem_sphere, EuclideanGeometry.Sphere.mem_coe, Real.sqrt_nonneg
-- 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
inst_4 : s.direction.HasOrthogonalProjection
ps : Set P
hnps : ps.Nonempty
p : P
hps : ps ⊆ (↑s : Set P)
hp : p ∉ s
this : Nonempty.{u_2 + 1} ↥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 : (a : P) → ↥s) p) : P)
y : ℝ := dist p (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)
hy0 : y ≠ 0
ycc₂ : ℝ := (x * x + y * y - cr * cr) / (2 * y)
cc₂ : P := (ycc₂ / y) • (p -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)) +ᵥ cc
cr₂ : ℝ := √(cr * cr + ycc₂ * ycc₂)
hpo :
  p =
    HVAdd.hVAdd (β := P) (HSMul.hSMul (α := ℝ) 1 (p -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)))
      (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)
p₁ : P
hp₁ : p₁ ∈ insert p ps
h :
  ∀ (hp₁ : p₁ = p),
    dist p₁ (Sphere.center { center := cc₂, radius := cr₂ : Sphere P }) *
        dist p₁ (Sphere.center { center := cc₂, radius := cr₂ : Sphere P }) =
      cr * cr + ycc₂ * ycc₂
h₁ :
  ∀ (hp₁ : p₁ ∈ ps),
    dist p₁ (Sphere.center { center := cc₂, radius := cr₂ : Sphere P }) *
        dist p₁ (Sphere.center { center := cc₂, radius := cr₂ : Sphere P }) =
      cr * cr + ycc₂ * ycc₂
⊢ dist p₁ (Sphere.center { center := cc₂, radius := cr₂ : Sphere P }) *
      dist p₁ (Sphere.center { center := cc₂, radius := cr₂ : Sphere P }) =
    cr * cr + ycc₂ * ycc₂

Tactic:
rcases hp₁ with hp₁ | hp₁
-- 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
inst_4 : s.direction.HasOrthogonalProjection
ps : Set P
hnps : ps.Nonempty
p : P
hps : ps ⊆ (↑s : Set P)
hp : p ∉ s
this : Nonempty.{u_2 + 1} ↥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 : (a : P) → ↥s) p) : P)
y : ℝ := dist p (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)
hy0 : y ≠ 0
ycc₂ : ℝ := (x * x + y * y - cr * cr) / (2 * y)
cc₂ : P := (ycc₂ / y) • (p -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)) +ᵥ cc
cr₂ : ℝ := √(cr * cr + ycc₂ * ycc₂)
hpo :
  p =
    HVAdd.hVAdd (β := P) (HSMul.hSMul (α := ℝ) 1 (p -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)))
      (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)
p₁ : P
hp₁ : p₁ = p
h :
  dist cc (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) *
        dist cc (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) +
      (1 - ycc₂ / y) * (1 - ycc₂ / y) *
        (dist p (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) *
          dist p (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)) =
    cr * cr + ycc₂ * ycc₂
⊢ dist p₁ (Sphere.center { center := cc₂, radius := cr₂ : Sphere P }) *
      dist p₁ (Sphere.center { center := cc₂, radius := cr₂ : Sphere P }) =
    cr * cr + ycc₂ * ycc₂

Tactic:
rw [hp₁, hpo,
          dist_sq_smul_orthogonal_vadd_smul_orthogonal_vadd (orthogonalProjection_mem p) hcc _ _
            (vsub_orthogonalProjection_mem_direction_orthogonal s p),
          Real.norm_eq_abs, abs_mul_abs_self, ← dist_eq_norm_vsub V p, dist_comm _ cc]

Premises used: EuclideanGeometry.vsub_orthogonalProjection_mem_direction_orthogonal, dist_comm, EuclideanGeometry.orthogonalProjection_mem, EuclideanGeometry.dist_sq_smul_orthogonal_vadd_smul_orthogonal_vadd, abs_mul_abs_self, dist_eq_norm_vsub, Real.norm_eq_abs
-- 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
inst_4 : s.direction.HasOrthogonalProjection
ps : Set P
hnps : ps.Nonempty
p : P
hps : ps ⊆ (↑s : Set P)
hp : p ∉ s
this : Nonempty.{u_2 + 1} ↥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 : (a : P) → ↥s) p) : P)
y : ℝ := dist p (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)
hy0 : y ≠ 0
ycc₂ : ℝ := (x * x + y * y - cr * cr) / (2 * y)
cc₂ : P := (ycc₂ / y) • (p -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)) +ᵥ cc
cr₂ : ℝ := √(cr * cr + ycc₂ * ycc₂)
hpo :
  p =
    HVAdd.hVAdd (β := P) (HSMul.hSMul (α := ℝ) 1 (p -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)))
      (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)
p₁ : P
hp₁ : p₁ = p
h :
  dist cc (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) *
        dist cc (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) +
      (1 - (x * x + y * y - cr * cr) / (2 * y) / y) * (1 - (x * x + y * y - cr * cr) / (2 * y) / y) *
        (dist p (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) *
          dist p (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)) =
    cr * cr + (x * x + y * y - cr * cr) / (2 * y) * ((x * x + y * y - cr * cr) / (2 * y))
⊢ dist cc (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) *
        dist cc (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) +
      (1 - ycc₂ / y) * (1 - ycc₂ / y) *
        (dist p (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) *
          dist p (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)) =
    cr * cr + ycc₂ * ycc₂

Tactic:
simp only [ycc₂]
-- 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
inst_4 : s.direction.HasOrthogonalProjection
ps : Set P
hnps : ps.Nonempty
p : P
hps : ps ⊆ (↑s : Set P)
hp : p ∉ s
this : Nonempty.{u_2 + 1} ↥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 : (a : P) → ↥s) p) : P)
y : ℝ := dist p (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)
hy0 : y ≠ 0
ycc₂ : ℝ := (x * x + y * y - cr * cr) / (2 * y)
cc₂ : P := (ycc₂ / y) • (p -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)) +ᵥ cc
cr₂ : ℝ := √(cr * cr + ycc₂ * ycc₂)
hpo :
  p =
    HVAdd.hVAdd (β := P) (HSMul.hSMul (α := ℝ) 1 (p -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)))
      (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)
p₁ : P
hp₁ : p₁ = p
⊢ dist cc (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) *
        dist cc (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) +
      (1 - (x * x + y * y - cr * cr) / (2 * y) / y) * (1 - (x * x + y * y - cr * cr) / (2 * y) / y) *
        (dist p (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) *
          dist p (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)) =
    cr * cr + (x * x + y * y - cr * cr) / (2 * y) * ((x * x + y * y - cr * cr) / (2 * y))

Tactic:
field
-- 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
inst_4 : s.direction.HasOrthogonalProjection
ps : Set P
hnps : ps.Nonempty
p : P
hps : ps ⊆ (↑s : Set P)
hp : p ∉ s
this : Nonempty.{u_2 + 1} ↥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 : (a : P) → ↥s) p) : P)
y : ℝ := dist p (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)
hy0 : y ≠ 0
ycc₂ : ℝ := (x * x + y * y - cr * cr) / (2 * y)
cc₂ : P := (ycc₂ / y) • (p -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)) +ᵥ cc
cr₂ : ℝ := √(cr * cr + ycc₂ * ycc₂)
hpo :
  p =
    HVAdd.hVAdd (β := P) (HSMul.hSMul (α := ℝ) 1 (p -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)))
      (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)
cc₃ : P
cr₃ : ℝ
hcc₃ : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (insert p (↑s : Set P))) cc₃
hcr₃ : insert p ps ⊆ Metric.sphere cc₃ cr₃
rwa rwa₁ rwa₂ rwa₃ :
  ∀ (hcc₃ : ∃ (r : ℝ), ∃ p0 ∈ s, cc₃ = r • (p -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)) +ᵥ p0)
    (hcr₃ : insert p ps ⊆ Metric.sphere cc₃ cr₃),
    ∃ (r : ℝ), ∃ p0 ∈ s, cc₃ = r • (p -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)) +ᵥ p0
⊢ ∃ (r : ℝ), ∃ p0 ∈ s, cc₃ = r • (p -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)) +ᵥ p0

Tactic:
rwa [mem_affineSpan_insert_iff (orthogonalProjection_mem p)] at hcc₃

Premises used: AffineSubspace.mem_affineSpan_insert_iff, EuclideanGeometry.orthogonalProjection_mem
-- 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
inst_4 : s.direction.HasOrthogonalProjection
ps : Set P
hnps : ps.Nonempty
p : P
hps : ps ⊆ (↑s : Set P)
hp : p ∉ s
this : Nonempty.{u_2 + 1} ↥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 : (a : P) → ↥s) p) : P)
y : ℝ := dist p (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)
hy0 : y ≠ 0
ycc₂ : ℝ := (x * x + y * y - cr * cr) / (2 * y)
cc₂ : P := (ycc₂ / y) • (p -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)) +ᵥ cc
cr₂ : ℝ := √(cr * cr + ycc₂ * ycc₂)
hpo :
  p =
    HVAdd.hVAdd (β := P) (HSMul.hSMul (α := ℝ) 1 (p -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)))
      (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)
cc₃ : P
cr₃ : ℝ
hcc₃ : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (insert p (↑s : Set P))) cc₃
hcr₃ : insert p ps ⊆ Metric.sphere cc₃ cr₃
h :
  ∀ (t₃ : ℝ) (cc₃' : P) (hcc₃' : cc₃' ∈ s)
    (hcc₃'' : cc₃ = t₃ • (p -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)) +ᵥ cc₃'),
    Eq (α := Sphere P) { center := cc₃, radius := cr₃ } { center := cc₂, radius := cr₂ }
⊢ Eq (α := Sphere P) { center := cc₃, radius := cr₃ } { center := cc₂, radius := cr₂ }

Tactic:
obtain ⟨t₃, cc₃', hcc₃', hcc₃''⟩ :
      ∃ r : ℝ, ∃ p0 ∈ s, cc₃ = r • (p -ᵥ ↑((orthogonalProjection s) p)) +ᵥ p0 := by
      rwa [mem_affineSpan_insert_iff (orthogonalProjection_mem p)] at hcc₃

Premises used: VSub.vsub, EuclideanGeometry.orthogonalProjection, Subtype.val, DFunLike.coe