awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Circumcenter (goal)
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₂)
⊢ ∃! cs₂ : Sphere P,
    Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (insert p (↑s : Set P))) cs₂.center ∧
      insert p ps ⊆ Metric.sphere cs₂.center cs₂.radius
have h : (fun (cs₂ : Sphere P) ↦
      Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (insert p (↑s : Set P))) cs₂.center ∧
        insert p ps ⊆ Metric.sphere cs₂.center cs₂.radius)
    { center := cc₂, radius := cr₂ } ∧
  ∀ (y : Sphere P),
    (fun (cs₂ : Sphere P) ↦
          Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (insert p (↑s : Set P))) cs₂.center ∧
            insert p ps ⊆ Metric.sphere cs₂.center cs₂.radius)
        y →
      y = { center := cc₂, radius := cr₂ }
Tactic: use ⟨cc₂, cr₂⟩
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Circumcenter (hypothesis)
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₂)
⊢ (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₂ }
have hpo : p =
  HVAdd.hVAdd (β := P) (HSMul.hSMul (α := ℝ) 1 (p -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)))
    (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)
Tactic: have hpo : p = (1 : ℝ) • (p -ᵥ orthogonalProjection s p : V) +ᵥ (orthogonalProjection s p : P) :=
    by simp
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Circumcenter (goal)
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 }) ∧
      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₂ }
have 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₂ })
Tactic: constructor
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Circumcenter (goal)
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₂ })
⊢ (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₂ }
have 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₂ }
Tactic: constructor
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Circumcenter (goal)
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 }) ∧
    insert p ps ⊆
      Metric.sphere (Sphere.center { center := cc₂, radius := cr₂ }) (Sphere.radius { center := cc₂, radius := cr₂ })
have h : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (insert p (↑s : Set P)))
  (Sphere.center { center := cc₂, radius := cr₂ : Sphere P })
Tactic: constructor
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Circumcenter (goal)
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 })
⊢ 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₂ })
have h₁ : insert p ps ⊆
  Metric.sphere (Sphere.center { center := cc₂, radius := cr₂ }) (Sphere.radius { center := cc₂, radius := cr₂ })
Tactic: constructor
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Circumcenter (goal)
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 })
have h : Membership.mem (γ := Submodule ℝ V) (direction (affineSpan ℝ (insert p (↑s : Set P))))
  ((ycc₂ / y) • (p -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)))
Tactic: refine vadd_mem_of_mem_direction ?_ (mem_affineSpan ℝ (Set.mem_insert_of_mem _ hcc))
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Circumcenter (goal)
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) (direction (affineSpan ℝ (insert p (↑s : Set P))))
    ((ycc₂ / y) • (p -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)))
have h : Membership.mem (γ := Submodule ℝ V) (vectorSpan ℝ (insert p (↑s : Set P)))
  ((ycc₂ / y) • (p -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)))
Tactic: rw [direction_affineSpan]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Circumcenter (goal)
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
⊢ p₁ ∈
    Metric.sphere (Sphere.center { center := cc₂, radius := cr₂ : Sphere P })
      (Sphere.radius { center := cc₂, radius := cr₂ : Sphere P })
have 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₂
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 _))]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Circumcenter (goal)
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
⊢ dist p₁ (Sphere.center { center := cc₂, radius := cr₂ : Sphere P }) *
      dist p₁ (Sphere.center { center := cc₂, radius := cr₂ : Sphere P }) =
    cr * cr + ycc₂ * ycc₂
have 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₂
Tactic: rcases hp₁ with hp₁ | hp₁
Cleared hypotheses: hp₁
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Circumcenter (goal)
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₂
⊢ dist p₁ (Sphere.center { center := cc₂, radius := cr₂ : Sphere P }) *
      dist p₁ (Sphere.center { center := cc₂, radius := cr₂ : Sphere P }) =
    cr * cr + ycc₂ * ycc₂
have 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₂
Tactic: rcases hp₁ with hp₁ | hp₁
Cleared hypotheses: hp₁
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Circumcenter (goal)
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 p₁ (Sphere.center { center := cc₂, radius := cr₂ : Sphere P }) *
      dist p₁ (Sphere.center { center := cc₂, radius := cr₂ : Sphere P }) =
    cr * cr + ycc₂ * ycc₂
have 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₂
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]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Circumcenter (goal)
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₁ ∈ 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₂
have h : dist p₁ (↑((orthogonalProjection s : (a : P) → ↥s) (Sphere.center { center := cc₂, radius := cr₂ : Sphere P })) : P) *
      dist p₁
        (↑((orthogonalProjection s : (a : P) → ↥s) (Sphere.center { center := cc₂, radius := cr₂ : Sphere P })) : P) +
    dist (Sphere.center { center := cc₂, radius := cr₂ : Sphere P })
        (↑((orthogonalProjection s : (a : P) → ↥s) (Sphere.center { center := cc₂, radius := cr₂ : Sphere P })) : P) *
      dist (Sphere.center { center := cc₂, radius := cr₂ : Sphere P })
        (↑((orthogonalProjection s : (a : P) → ↥s) (Sphere.center { center := cc₂, radius := cr₂ : Sphere P })) : P) =
  cr * cr + ycc₂ * ycc₂
Tactic: rw [dist_sq_eq_dist_orthogonalProjection_sq_add_dist_orthogonalProjection_sq _ (hps hp₁),
          orthogonalProjection_vadd_smul_vsub_orthogonalProjection _ _ hcc, Subtype.coe_mk,
          dist_of_mem_subset_mk_sphere hp₁ hcr, dist_eq_norm_vsub V cc₂ cc, vadd_vsub, norm_smul, ←
          dist_eq_norm_vsub V, Real.norm_eq_abs, abs_div, abs_of_nonneg dist_nonneg,
          div_mul_cancel₀ _ hy0, abs_mul_abs_self]