awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
ps : Set P
h : ps ⊆ (↑s : Set P)
inst_4 : Nonempty.{u_2 + 1} ↥s
n : ℕ
inst_5 : FiniteDimensional.{0, u_1} ℝ ↥s.direction
hd : finrank.{0, u_1} ℝ ↥s.direction = n
hc : Cospherical ps
⊢ ∃ (r : ℝ), ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumradius = r
have hc₁ : ∃ center ∈ s, ∃ (radius : ℝ), ∀ p ∈ ps, dist p center = radius
Tactic: rw [cospherical_iff_exists_mem_of_finiteDimensional h] at hc
Cleared hypotheses: hc
-- 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
ps : Set P
h : ps ⊆ (↑s : Set P)
inst_4 : Nonempty.{u_2 + 1} ↥s
n : ℕ
inst_5 : FiniteDimensional.{0, u_1} ℝ ↥s.direction
hd : finrank.{0, u_1} ℝ ↥s.direction = n
hc : ∃ center ∈ s, ∃ (radius : ℝ), ∀ p ∈ ps, dist p center = radius
⊢ ∃ (r : ℝ), ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumradius = r
have rcases : ∀ (c : P) (hc : c ∈ s) (r : ℝ) (hcr : ∀ p ∈ ps, dist p c = r),
  ∃ (r : ℝ), ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumradius = r
Tactic: rcases hc with ⟨c, hc, r, hcr⟩
Cleared hypotheses: hc
-- 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
ps : Set P
h : ps ⊆ (↑s : Set P)
inst_4 : Nonempty.{u_2 + 1} ↥s
n : ℕ
inst_5 : FiniteDimensional.{0, u_1} ℝ ↥s.direction
hd : finrank.{0, u_1} ℝ ↥s.direction = n
c : P
hc : c ∈ s
r : ℝ
hcr : ∀ p ∈ ps, dist p c = r
⊢ ∃ (r : ℝ), ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumradius = r
have h₁ : ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumradius = r
Tactic: use r
-- 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
ps : Set P
h : ps ⊆ (↑s : Set P)
inst_4 : Nonempty.{u_2 + 1} ↥s
n : ℕ
inst_5 : FiniteDimensional.{0, u_1} ℝ ↥s.direction
hd : finrank.{0, u_1} ℝ ↥s.direction = n
c : P
hc : c ∈ s
r : ℝ
hcr : ∀ p ∈ ps, dist p c = r
sx : Simplex ℝ P n
hsxps : Set.range sx.points ⊆ ps
⊢ affineSpan ℝ (Set.range sx.points) = s
have this : Fintype.card (Fin (n + 1)) = finrank.{0, u_1} ℝ ↥s.direction + 1
Tactic: refine
      sx.independent.affineSpan_eq_of_le_of_card_eq_finrank_add_one
        (affineSpan_le_of_subset_coe (hsxps.trans h)) ?_
-- 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
ps : Set P
h : ps ⊆ (↑s : Set P)
inst_4 : Nonempty.{u_2 + 1} ↥s
n : ℕ
inst_5 : FiniteDimensional.{0, u_1} ℝ ↥s.direction
hd : finrank.{0, u_1} ℝ ↥s.direction = n
c : P
hc : c ∈ s
r : ℝ
hcr : ∀ p ∈ ps, dist p c = r
sx : Simplex ℝ P n
hsxps : Set.range sx.points ⊆ ps
⊢ sx.circumradius = r
have hsx : affineSpan ℝ (Set.range sx.points) = s
Tactic: have hsx : affineSpan ℝ (Set.range sx.points) = s := by
    refine
      sx.independent.affineSpan_eq_of_le_of_card_eq_finrank_add_one
        (affineSpan_le_of_subset_coe (hsxps.trans h)) ?_
    simp [hd]
-- 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
ps : Set P
h : ps ⊆ (↑s : Set P)
inst_4 : Nonempty.{u_2 + 1} ↥s
n : ℕ
inst_5 : FiniteDimensional.{0, u_1} ℝ ↥s.direction
hd : finrank.{0, u_1} ℝ ↥s.direction = n
c : P
hc : c ∈ s
r : ℝ
hcr : ∀ p ∈ ps, dist p c = r
sx : Simplex ℝ P n
hsxps : Set.range sx.points ⊆ ps
hsx : affineSpan ℝ (Set.range sx.points) = s
⊢ sx.circumradius = r
have hc₁ : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range sx.points)) c
Tactic: have hc : c ∈ affineSpan ℝ (Set.range sx.points) := hsx.symm ▸ hc
-- 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
ps : Set P
h : ps ⊆ (↑s : Set P)
inst_4 : Nonempty.{u_2 + 1} ↥s
n : ℕ
inst_5 : FiniteDimensional.{0, u_1} ℝ ↥s.direction
hd : finrank.{0, u_1} ℝ ↥s.direction = n
hc : Cospherical ps
sx₁ sx₂ : Simplex ℝ P n
hsx₁ : Set.range sx₁.points ⊆ ps
hsx₂ : Set.range sx₂.points ⊆ ps
⊢ sx₁.circumradius = sx₂.circumradius
have rcases : ∀ (r : ℝ) (hr : ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumradius = r),
  sx₁.circumradius = sx₂.circumradius
Tactic: rcases exists_circumradius_eq_of_cospherical_subset h hd hc with ⟨r, hr⟩
-- 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
ps : Set P
h : ps ⊆ (↑s : Set P)
inst_4 : Nonempty.{u_2 + 1} ↥s
n : ℕ
inst_5 : FiniteDimensional.{0, u_1} ℝ ↥s.direction
hd : finrank.{0, u_1} ℝ ↥s.direction = n
hc : Cospherical ps
sx₁ sx₂ : Simplex ℝ P n
hsx₁ : Set.range sx₁.points ⊆ ps
hsx₂ : Set.range sx₂.points ⊆ ps
r : ℝ
hr : ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumradius = r
⊢ sx₁.circumradius = sx₂.circumradius
have rw : r = sx₂.circumradius
Tactic: rw [hr sx₁ hsx₁, hr sx₂ hsx₂]
-- 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
ps : Set P
h : ps ⊆ (↑s : Set P)
inst_4 : Nonempty.{u_2 + 1} ↥s
n : ℕ
inst_5 : FiniteDimensional.{0, u_1} ℝ ↥s.direction
hd : finrank.{0, u_1} ℝ ↥s.direction = n
hc : Cospherical ps
sx₁ sx₂ : Simplex ℝ P n
hsx₁ : Set.range sx₁.points ⊆ ps
hsx₂ : Set.range sx₂.points ⊆ ps
r : ℝ
hr : ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumradius = r
rw : r = sx₂.circumradius
⊢ sx₁.circumradius = sx₂.circumradius
have rw₁ : r = r
Tactic: rw [hr sx₁ hsx₁, hr sx₂ hsx₂]
-- 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
ps : Set P
n : ℕ
inst_4 : FiniteDimensional ℝ V
hd : finrank ℝ V = n
hc : Cospherical ps
⊢ ∃ (r : ℝ), ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumradius = r
have hd₁ : finrank.{0, u_1} ℝ ↥(direction.{0, u_1, u_2} (P := P) ⊤) = n
Tactic: rw [← finrank_top, ← direction_top ℝ V P] at hd
Cleared hypotheses: hd, hc
-- 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
ps : Set P
n : ℕ
inst_4 : FiniteDimensional ℝ V
hd : finrank.{0, u_1} ℝ ↥(direction.{0, u_1, u_2} (P := P) ⊤) = n
hc : Cospherical ps
⊢ ∃ (r : ℝ), ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumradius = r
have refine : ps ⊆ (↑⊤ : Set P)
Tactic: refine exists_circumradius_eq_of_cospherical_subset ?_ hd hc
-- 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
ps : Set P
n : ℕ
inst_4 : FiniteDimensional ℝ V
hd : finrank ℝ V = n
hc : Cospherical ps
sx₁ sx₂ : Simplex ℝ P n
hsx₁ : Set.range sx₁.points ⊆ ps
hsx₂ : Set.range sx₂.points ⊆ ps
⊢ sx₁.circumradius = sx₂.circumradius
have rcases : ∀ (r : ℝ) (hr : ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumradius = r),
  sx₁.circumradius = sx₂.circumradius
Tactic: rcases exists_circumradius_eq_of_cospherical hd hc with ⟨r, hr⟩
-- 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
ps : Set P
n : ℕ
inst_4 : FiniteDimensional ℝ V
hd : finrank ℝ V = n
hc : Cospherical ps
sx₁ sx₂ : Simplex ℝ P n
hsx₁ : Set.range sx₁.points ⊆ ps
hsx₂ : Set.range sx₂.points ⊆ ps
r : ℝ
hr : ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumradius = r
⊢ sx₁.circumradius = sx₂.circumradius
have rw : r = sx₂.circumradius
Tactic: rw [hr sx₁ hsx₁, hr sx₂ hsx₂]
-- 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
ps : Set P
n : ℕ
inst_4 : FiniteDimensional ℝ V
hd : finrank ℝ V = n
hc : Cospherical ps
sx₁ sx₂ : Simplex ℝ P n
hsx₁ : Set.range sx₁.points ⊆ ps
hsx₂ : Set.range sx₂.points ⊆ ps
r : ℝ
hr : ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumradius = r
rw : r = sx₂.circumradius
⊢ sx₁.circumradius = sx₂.circumradius
have rw₁ : r = r
Tactic: rw [hr sx₁ hsx₁, hr sx₂ hsx₂]
-- 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
ps : Set P
h : ps ⊆ (↑s : Set P)
inst_4 : Nonempty.{u_2 + 1} ↥s
n : ℕ
inst_5 : FiniteDimensional.{0, u_1} ℝ ↥s.direction
hd : finrank.{0, u_1} ℝ ↥s.direction = n
hc : Cospherical ps
⊢ ∃ (c : P), ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumcenter = c
have hc₁ : ∃ center ∈ s, ∃ (radius : ℝ), ∀ p ∈ ps, dist p center = radius
Tactic: rw [cospherical_iff_exists_mem_of_finiteDimensional h] at hc
Cleared hypotheses: hc
-- 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
ps : Set P
h : ps ⊆ (↑s : Set P)
inst_4 : Nonempty.{u_2 + 1} ↥s
n : ℕ
inst_5 : FiniteDimensional.{0, u_1} ℝ ↥s.direction
hd : finrank.{0, u_1} ℝ ↥s.direction = n
hc : ∃ center ∈ s, ∃ (radius : ℝ), ∀ p ∈ ps, dist p center = radius
⊢ ∃ (c : P), ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumcenter = c
have rcases : ∀ (c : P) (hc : c ∈ s) (r : ℝ) (hcr : ∀ p ∈ ps, dist p c = r),
  ∃ (c : P), ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumcenter = c
Tactic: rcases hc with ⟨c, hc, r, hcr⟩
Cleared hypotheses: hc
-- 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
ps : Set P
h : ps ⊆ (↑s : Set P)
inst_4 : Nonempty.{u_2 + 1} ↥s
n : ℕ
inst_5 : FiniteDimensional.{0, u_1} ℝ ↥s.direction
hd : finrank.{0, u_1} ℝ ↥s.direction = n
c : P
hc : c ∈ s
r : ℝ
hcr : ∀ p ∈ ps, dist p c = r
⊢ ∃ (c : P), ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumcenter = c
have h₁ : ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumcenter = c
Tactic: use c
-- 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
ps : Set P
h : ps ⊆ (↑s : Set P)
inst_4 : Nonempty.{u_2 + 1} ↥s
n : ℕ
inst_5 : FiniteDimensional.{0, u_1} ℝ ↥s.direction
hd : finrank.{0, u_1} ℝ ↥s.direction = n
c : P
hc : c ∈ s
r : ℝ
hcr : ∀ p ∈ ps, dist p c = r
sx : Simplex ℝ P n
hsxps : Set.range sx.points ⊆ ps
⊢ sx.circumcenter = c
have hsx : affineSpan ℝ (Set.range sx.points) = s
Tactic: have hsx : affineSpan ℝ (Set.range sx.points) = s := by
    refine
      sx.independent.affineSpan_eq_of_le_of_card_eq_finrank_add_one
        (affineSpan_le_of_subset_coe (hsxps.trans h)) ?_
    simp [hd]
-- 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
ps : Set P
h : ps ⊆ (↑s : Set P)
inst_4 : Nonempty.{u_2 + 1} ↥s
n : ℕ
inst_5 : FiniteDimensional.{0, u_1} ℝ ↥s.direction
hd : finrank.{0, u_1} ℝ ↥s.direction = n
c : P
hc : c ∈ s
r : ℝ
hcr : ∀ p ∈ ps, dist p c = r
sx : Simplex ℝ P n
hsxps : Set.range sx.points ⊆ ps
hsx : affineSpan ℝ (Set.range sx.points) = s
⊢ sx.circumcenter = c
have hc₁ : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range sx.points)) c
Tactic: have hc : c ∈ affineSpan ℝ (Set.range sx.points) := hsx.symm ▸ hc
-- 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
ps : Set P
h : ps ⊆ (↑s : Set P)
inst_4 : Nonempty.{u_2 + 1} ↥s
n : ℕ
inst_5 : FiniteDimensional.{0, u_1} ℝ ↥s.direction
hd : finrank.{0, u_1} ℝ ↥s.direction = n
hc : Cospherical ps
sx₁ sx₂ : Simplex ℝ P n
hsx₁ : Set.range sx₁.points ⊆ ps
hsx₂ : Set.range sx₂.points ⊆ ps
⊢ sx₁.circumcenter = sx₂.circumcenter
have rcases : ∀ (r : P) (hr : ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumcenter = r),
  sx₁.circumcenter = sx₂.circumcenter
Tactic: rcases exists_circumcenter_eq_of_cospherical_subset h hd hc with ⟨r, hr⟩
-- 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
ps : Set P
h : ps ⊆ (↑s : Set P)
inst_4 : Nonempty.{u_2 + 1} ↥s
n : ℕ
inst_5 : FiniteDimensional.{0, u_1} ℝ ↥s.direction
hd : finrank.{0, u_1} ℝ ↥s.direction = n
hc : Cospherical ps
sx₁ sx₂ : Simplex ℝ P n
hsx₁ : Set.range sx₁.points ⊆ ps
hsx₂ : Set.range sx₂.points ⊆ ps
r : P
hr : ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumcenter = r
⊢ sx₁.circumcenter = sx₂.circumcenter
have rw : r = sx₂.circumcenter
Tactic: rw [hr sx₁ hsx₁, hr sx₂ hsx₂]
-- 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
ps : Set P
h : ps ⊆ (↑s : Set P)
inst_4 : Nonempty.{u_2 + 1} ↥s
n : ℕ
inst_5 : FiniteDimensional.{0, u_1} ℝ ↥s.direction
hd : finrank.{0, u_1} ℝ ↥s.direction = n
hc : Cospherical ps
sx₁ sx₂ : Simplex ℝ P n
hsx₁ : Set.range sx₁.points ⊆ ps
hsx₂ : Set.range sx₂.points ⊆ ps
r : P
hr : ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumcenter = r
rw : r = sx₂.circumcenter
⊢ sx₁.circumcenter = sx₂.circumcenter
have rw₁ : r = r
Tactic: rw [hr sx₁ hsx₁, hr sx₂ hsx₂]
-- 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
ps : Set P
n : ℕ
inst_4 : FiniteDimensional ℝ V
hd : finrank ℝ V = n
hc : Cospherical ps
⊢ ∃ (c : P), ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumcenter = c
have hd₁ : finrank.{0, u_1} ℝ ↥(direction.{0, u_1, u_2} (P := P) ⊤) = n
Tactic: rw [← finrank_top, ← direction_top ℝ V P] at hd
Cleared hypotheses: hd, hc
-- 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
ps : Set P
n : ℕ
inst_4 : FiniteDimensional ℝ V
hd : finrank.{0, u_1} ℝ ↥(direction.{0, u_1, u_2} (P := P) ⊤) = n
hc : Cospherical ps
⊢ ∃ (c : P), ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumcenter = c
have refine : ps ⊆ (↑⊤ : Set P)
Tactic: refine exists_circumcenter_eq_of_cospherical_subset ?_ hd hc
-- 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
ps : Set P
n : ℕ
inst_4 : FiniteDimensional ℝ V
hd : finrank ℝ V = n
hc : Cospherical ps
sx₁ sx₂ : Simplex ℝ P n
hsx₁ : Set.range sx₁.points ⊆ ps
hsx₂ : Set.range sx₂.points ⊆ ps
⊢ sx₁.circumcenter = sx₂.circumcenter
have rcases : ∀ (r : P) (hr : ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumcenter = r),
  sx₁.circumcenter = sx₂.circumcenter
Tactic: rcases exists_circumcenter_eq_of_cospherical hd hc with ⟨r, hr⟩
-- 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
ps : Set P
n : ℕ
inst_4 : FiniteDimensional ℝ V
hd : finrank ℝ V = n
hc : Cospherical ps
sx₁ sx₂ : Simplex ℝ P n
hsx₁ : Set.range sx₁.points ⊆ ps
hsx₂ : Set.range sx₂.points ⊆ ps
r : P
hr : ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumcenter = r
⊢ sx₁.circumcenter = sx₂.circumcenter
have rw : r = sx₂.circumcenter
Tactic: rw [hr sx₁ hsx₁, hr sx₂ hsx₂]
-- 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
ps : Set P
n : ℕ
inst_4 : FiniteDimensional ℝ V
hd : finrank ℝ V = n
hc : Cospherical ps
sx₁ sx₂ : Simplex ℝ P n
hsx₁ : Set.range sx₁.points ⊆ ps
hsx₂ : Set.range sx₂.points ⊆ ps
r : P
hr : ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumcenter = r
rw : r = sx₂.circumcenter
⊢ sx₁.circumcenter = sx₂.circumcenter
have rw₁ : r = r
Tactic: rw [hr sx₁ hsx₁, hr sx₂ hsx₂]
-- 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
ps : Set P
h : ps ⊆ (↑s : Set P)
inst_4 : Nonempty.{u_2 + 1} ↥s
n : ℕ
inst_5 : FiniteDimensional.{0, u_1} ℝ ↥s.direction
hd : finrank.{0, u_1} ℝ ↥s.direction = n
hc : Cospherical ps
⊢ ∃ (c : Sphere P), ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumsphere = c
have obtain : ∀ (r : ℝ) (hr : ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumradius = r),
  ∃ (c : Sphere P), ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumsphere = c
Tactic: obtain ⟨r, hr⟩ := exists_circumradius_eq_of_cospherical_subset h hd hc
-- 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
ps : Set P
h : ps ⊆ (↑s : Set P)
inst_4 : Nonempty.{u_2 + 1} ↥s
n : ℕ
inst_5 : FiniteDimensional.{0, u_1} ℝ ↥s.direction
hd : finrank.{0, u_1} ℝ ↥s.direction = n
hc : Cospherical ps
r : ℝ
hr : ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumradius = r
⊢ ∃ (c : Sphere P), ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumsphere = c
have obtain : ∀ (c : P) (hc : ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumcenter = c),
  ∃ (c : Sphere P), ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumsphere = c
Tactic: obtain ⟨c, hc⟩ := exists_circumcenter_eq_of_cospherical_subset h hd hc
-- 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
ps : Set P
h : ps ⊆ (↑s : Set P)
inst_4 : Nonempty.{u_2 + 1} ↥s
n : ℕ
inst_5 : FiniteDimensional.{0, u_1} ℝ ↥s.direction
hd : finrank.{0, u_1} ℝ ↥s.direction = n
hc : Cospherical ps
sx₁ sx₂ : Simplex ℝ P n
hsx₁ : Set.range sx₁.points ⊆ ps
hsx₂ : Set.range sx₂.points ⊆ ps
⊢ sx₁.circumsphere = sx₂.circumsphere
have rcases : ∀ (r : Sphere P) (hr : ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumsphere = r),
  sx₁.circumsphere = sx₂.circumsphere
Tactic: rcases exists_circumsphere_eq_of_cospherical_subset h hd hc with ⟨r, hr⟩
-- 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
ps : Set P
h : ps ⊆ (↑s : Set P)
inst_4 : Nonempty.{u_2 + 1} ↥s
n : ℕ
inst_5 : FiniteDimensional.{0, u_1} ℝ ↥s.direction
hd : finrank.{0, u_1} ℝ ↥s.direction = n
hc : Cospherical ps
sx₁ sx₂ : Simplex ℝ P n
hsx₁ : Set.range sx₁.points ⊆ ps
hsx₂ : Set.range sx₂.points ⊆ ps
r : Sphere P
hr : ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumsphere = r
⊢ sx₁.circumsphere = sx₂.circumsphere
have rw : r = sx₂.circumsphere
Tactic: rw [hr sx₁ hsx₁, hr sx₂ hsx₂]
-- 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
ps : Set P
h : ps ⊆ (↑s : Set P)
inst_4 : Nonempty.{u_2 + 1} ↥s
n : ℕ
inst_5 : FiniteDimensional.{0, u_1} ℝ ↥s.direction
hd : finrank.{0, u_1} ℝ ↥s.direction = n
hc : Cospherical ps
sx₁ sx₂ : Simplex ℝ P n
hsx₁ : Set.range sx₁.points ⊆ ps
hsx₂ : Set.range sx₂.points ⊆ ps
r : Sphere P
hr : ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumsphere = r
rw : r = sx₂.circumsphere
⊢ sx₁.circumsphere = sx₂.circumsphere
have rw₁ : r = r
Tactic: rw [hr sx₁ hsx₁, hr sx₂ hsx₂]
-- 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
ps : Set P
n : ℕ
inst_4 : FiniteDimensional ℝ V
hd : finrank ℝ V = n
hc : Cospherical ps
⊢ ∃ (c : Sphere P), ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumsphere = c
have hd₁ : finrank.{0, u_1} ℝ ↥(direction.{0, u_1, u_2} (P := P) ⊤) = n
Tactic: rw [← finrank_top, ← direction_top ℝ V P] at hd
Cleared hypotheses: hd, hc
-- 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
ps : Set P
n : ℕ
inst_4 : FiniteDimensional ℝ V
hd : finrank.{0, u_1} ℝ ↥(direction.{0, u_1, u_2} (P := P) ⊤) = n
hc : Cospherical ps
⊢ ∃ (c : Sphere P), ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumsphere = c
have refine : ps ⊆ (↑⊤ : Set P)
Tactic: refine exists_circumsphere_eq_of_cospherical_subset ?_ hd hc
-- 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
ps : Set P
n : ℕ
inst_4 : FiniteDimensional ℝ V
hd : finrank ℝ V = n
hc : Cospherical ps
sx₁ sx₂ : Simplex ℝ P n
hsx₁ : Set.range sx₁.points ⊆ ps
hsx₂ : Set.range sx₂.points ⊆ ps
⊢ sx₁.circumsphere = sx₂.circumsphere
have rcases : ∀ (r : Sphere P) (hr : ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumsphere = r),
  sx₁.circumsphere = sx₂.circumsphere
Tactic: rcases exists_circumsphere_eq_of_cospherical hd hc with ⟨r, hr⟩
-- 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
ps : Set P
n : ℕ
inst_4 : FiniteDimensional ℝ V
hd : finrank ℝ V = n
hc : Cospherical ps
sx₁ sx₂ : Simplex ℝ P n
hsx₁ : Set.range sx₁.points ⊆ ps
hsx₂ : Set.range sx₂.points ⊆ ps
r : Sphere P
hr : ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumsphere = r
⊢ sx₁.circumsphere = sx₂.circumsphere
have rw : r = sx₂.circumsphere
Tactic: rw [hr sx₁ hsx₁, hr sx₂ hsx₂]