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₂)
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
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₂
⊢ 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₁ (↑(Subtype.mk (p := fun (x : P) ↦ x ∈ s) cc hcc) : P) *
      dist p₁ (↑(Subtype.mk (p := fun (x : P) ↦ x ∈ s) cc hcc) : P) +
    dist (Sphere.center { center := cc₂, radius := cr₂ : Sphere P })
        (↑(Subtype.mk (p := fun (x : P) ↦ x ∈ s) cc hcc) : P) *
      dist (Sphere.center { center := cc₂, radius := cr₂ : Sphere P })
        (↑(Subtype.mk (p := fun (x : P) ↦ x ∈ s) cc hcc) : 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]
-- 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
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₂
h₁ :
  dist p₁ (↑(Subtype.mk (p := fun (x : P) ↦ x ∈ s) cc hcc) : P) *
        dist p₁ (↑(Subtype.mk (p := fun (x : P) ↦ x ∈ s) cc hcc) : P) +
      dist (Sphere.center { center := cc₂, radius := cr₂ : Sphere P })
          (↑(Subtype.mk (p := fun (x : P) ↦ x ∈ s) cc hcc) : P) *
        dist (Sphere.center { center := cc₂, radius := cr₂ : Sphere P })
          (↑(Subtype.mk (p := fun (x : P) ↦ x ∈ s) cc hcc) : 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₂ : dist p₁ cc * dist p₁ cc +
    dist (Sphere.center { center := cc₂, radius := cr₂ : Sphere P }) cc *
      dist (Sphere.center { center := cc₂, radius := cr₂ : Sphere P }) cc =
  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]
-- 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)
cc₃ : P
cr₃ : ℝ
hcc₃ : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (insert p (↑s : Set P))) cc₃
hcr₃ : insert p ps ⊆ Metric.sphere cc₃ cr₃
⊢ ∃ (r : ℝ), ∃ p0 ∈ s, cc₃ = r • (p -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)) +ᵥ p0
have 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
Tactic: rwa [mem_affineSpan_insert_iff (orthogonalProjection_mem p)] at hcc₃
Cleared hypotheses: hcc₃, hcr₃
-- 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)
cc₃ : P
cr₃ : ℝ
hcc₃ : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (insert p (↑s : Set P))) cc₃
hcr₃ : insert p ps ⊆ Metric.sphere cc₃ cr₃
⊢ Eq (α := Sphere P) { center := cc₃, radius := cr₃ } { center := cc₂, radius := cr₂ }
have 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₂ }
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₃
-- 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₂)
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₃
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₂ }
have hcr₃' : ∃ (r : ℝ), ∀ p₁ ∈ ps, dist p₁ cc₃ = r
Tactic: have hcr₃' : ∃ r, ∀ p₁ ∈ ps, dist p₁ cc₃ = r :=
      ⟨cr₃, fun p₁ hp₁ => dist_of_mem_subset_mk_sphere (Set.mem_insert_of_mem _ hp₁) hcr₃⟩
-- 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₂)
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₃
t₃ : ℝ
cc₃' : P
hcc₃' : cc₃' ∈ s
hcc₃'' : cc₃ = t₃ • (p -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)) +ᵥ cc₃'
hcr₃' : ∃ (r : ℝ), ∀ p₁ ∈ ps, dist p₁ cc₃ = r
⊢ Eq (α := Sphere P) { center := cc₃, radius := cr₃ } { center := cc₂, radius := cr₂ }
have hcr₃'₁ : ∃ (r : ℝ), ∀ p₁ ∈ ps, dist p₁ (↑(Subtype.mk (p := fun (x : P) ↦ x ∈ s) cc₃' hcc₃') : P) = r
Tactic: rw [exists_dist_eq_iff_exists_dist_orthogonalProjection_eq hps cc₃, hcc₃'',
      orthogonalProjection_vadd_smul_vsub_orthogonalProjection _ _ hcc₃'] at hcr₃'
Cleared hypotheses: hcr₃'
-- 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)
cc₃ : P
cr₃ : ℝ
hcc₃ : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (insert p (↑s : Set P))) cc₃
hcr₃ : insert p ps ⊆ Metric.sphere cc₃ cr₃
t₃ : ℝ
cc₃' : P
hcc₃' : cc₃' ∈ s
hcc₃'' : cc₃ = t₃ • (p -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)) +ᵥ cc₃'
hcr₃' : ∃ (r : ℝ), ∀ p₁ ∈ ps, dist p₁ (↑(Subtype.mk (p := fun (x : P) ↦ x ∈ s) cc₃' hcc₃') : P) = r
⊢ Eq (α := Sphere P) { center := cc₃, radius := cr₃ } { center := cc₂, radius := cr₂ }
have h : ∀ (cr₃' : ℝ) (hcr₃' : ∀ p₁ ∈ ps, dist p₁ (↑(Subtype.mk (p := fun (x : P) ↦ x ∈ s) cc₃' hcc₃') : P) = cr₃'),
  Eq (α := Sphere P) { center := cc₃, radius := cr₃ } { center := cc₂, radius := cr₂ }
Tactic: obtain ⟨cr₃', hcr₃'⟩ := hcr₃'
Cleared hypotheses: hcr₃'
-- 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₂)
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₃
t₃ : ℝ
cc₃' : P
hcc₃' : cc₃' ∈ s
hcc₃'' : cc₃ = t₃ • (p -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)) +ᵥ cc₃'
cr₃' : ℝ
hcr₃' : ∀ p₁ ∈ ps, dist p₁ (↑(Subtype.mk (p := fun (x : P) ↦ x ∈ s) cc₃' hcc₃') : P) = cr₃'
⊢ Eq (α := Sphere P) { center := cc₃, radius := cr₃ } { center := cc₂, radius := cr₂ }
have hu : Sphere.center { center := cc₃', radius := cr₃' : Sphere P } ∈ s ∧
    ps ⊆
      Metric.sphere (Sphere.center { center := cc₃', radius := cr₃' })
        (Sphere.radius { center := cc₃', radius := cr₃' }) →
  Eq (α := Sphere P) { center := cc₃', radius := cr₃' } { center := cc, radius := cr }
Tactic: have hu := hcccru ⟨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₂)
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₃
t₃ : ℝ
cc₃' : P
hcc₃' : cc₃' ∈ s
hcc₃'' : cc₃ = t₃ • (p -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)) +ᵥ cc₃'
cr₃' : ℝ
hcr₃' : ∀ p₁ ∈ ps, dist p₁ (↑(Subtype.mk (p := fun (x : P) ↦ x ∈ s) cc₃' hcc₃') : P) = cr₃'
hu :
  cc₃' ∈ s ∧ ps ⊆ Metric.sphere cc₃' cr₃' →
    Eq (α := Sphere P) { center := cc₃', radius := cr₃' } { center := cc, radius := cr }
⊢ Eq (α := Sphere P) { center := cc₃, radius := cr₃ } { center := cc₂, radius := cr₂ }
have hu₁ : Eq (α := Sphere P) { center := cc₃', radius := cr₃' } { center := cc, radius := cr }
Tactic: replace hu := hu ⟨hcc₃', hcr₃'⟩
Cleared hypotheses: hu
-- 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₂)
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₃
t₃ : ℝ
cc₃' : P
hcc₃' : cc₃' ∈ s
hcc₃'' : cc₃ = t₃ • (p -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)) +ᵥ cc₃'
cr₃' : ℝ
hcr₃' : ∀ p₁ ∈ ps, dist p₁ (↑(Subtype.mk (p := fun (x : P) ↦ x ∈ s) cc₃' hcc₃') : P) = cr₃'
hu : Eq (α := Sphere P) { center := cc₃', radius := cr₃' } { center := cc, radius := cr }
hcc₃'₁ : cc ∈ s
⊢ Eq (α := Sphere P) { center := cc₃, radius := cr₃ } { center := cc₂, radius := cr₂ }
have hcc₃''₁ : cc₃ = t₃ • (p -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)) +ᵥ cc
Tactic: cases hu
Cleared hypotheses: cc₃', hcc₃', hcc₃'', cr₃', hcr₃', hu
-- 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₂)
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₃
t₃ : ℝ
cc₃' : P
hcc₃' : cc₃' ∈ s
hcc₃'' : cc₃ = t₃ • (p -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)) +ᵥ cc₃'
cr₃' : ℝ
hcr₃' : ∀ p₁ ∈ ps, dist p₁ (↑(Subtype.mk (p := fun (x : P) ↦ x ∈ s) cc₃' hcc₃') : P) = cr₃'
hu : Eq (α := Sphere P) { center := cc₃', radius := cr₃' } { center := cc, radius := cr }
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₂ }
have hcr₃'₁ : ∀ p₁ ∈ ps, dist p₁ (↑(Subtype.mk (p := fun (x : P) ↦ x ∈ s) cc hcc₃'₁) : P) = cr
Tactic: cases hu
Cleared hypotheses: cc₃', hcc₃', hcc₃'', cr₃', hcr₃', hu
-- 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)
cc₃ : P
cr₃ : ℝ
hcc₃ : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (insert p (↑s : Set P))) cc₃
hcr₃ : insert p ps ⊆ Metric.sphere cc₃ cr₃
t₃ : ℝ
hcc₃' : cc ∈ s
hcc₃'' : cc₃ = t₃ • (p -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)) +ᵥ cc
hcr₃' : ∀ p₁ ∈ ps, dist p₁ (↑(Subtype.mk (p := fun (x : P) ↦ x ∈ s) cc hcc₃') : P) = cr
⊢ cr₃ = √(cr * cr + t₃ * y * (t₃ * y))
have obtain : ∀ (p0 : P) (hp0 : p0 ∈ ps), cr₃ = √(cr * cr + t₃ * y * (t₃ * y))
Tactic: obtain ⟨p0, hp0⟩ := hnps
Cleared hypotheses: hnps