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
inst_4 : s.direction.HasOrthogonalProjection
ps : Set P
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
p0 : P
hp0 : p0 ∈ ps
⊢ cr₃ = √(cr * cr + t₃ * y * (t₃ * y))
have h' : (↑(Subtype.mk (p := fun (x : P) ↦ x ∈ s) cc hcc₃') : P) = cc
Tactic: have h' : ↑(⟨cc, hcc₃'⟩ : s) = cc := rfl
-- 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
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
p0 : P
hp0 : p0 ∈ ps
h' : (↑(Subtype.mk (p := fun (x : P) ↦ x ∈ s) cc hcc₃') : P) = cc
⊢ cr₃ = √(cr * cr + t₃ * y * (t₃ * y))
have rw : cr * cr +
    t₃ * t₃ * dist p (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) *
      dist p (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) =
  cr * cr + t₃ * y * (t₃ * y)
Tactic: rw [← dist_of_mem_subset_mk_sphere (Set.mem_insert_of_mem _ hp0) hcr₃, hcc₃'', ←
        mul_self_inj_of_nonneg dist_nonneg (Real.sqrt_nonneg _),
        Real.mul_self_sqrt (add_nonneg (mul_self_nonneg _) (mul_self_nonneg _)),
        dist_sq_eq_dist_orthogonalProjection_sq_add_dist_orthogonalProjection_sq _ (hps hp0),
        orthogonalProjection_vadd_smul_vsub_orthogonalProjection _ _ hcc₃', h',
        dist_of_mem_subset_mk_sphere hp0 hcr, dist_eq_norm_vsub V _ cc, vadd_vsub, norm_smul, ←
        dist_eq_norm_vsub V p, Real.norm_eq_abs, ← mul_assoc, mul_comm _ |t₃|, ← mul_assoc,
        abs_mul_abs_self]
-- 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₃ : ℝ
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
⊢ Eq (α := Sphere P) { center := cc₃, radius := cr₃ } { center := cc₂, radius := cr₂ }
have hcr₃val : cr₃ = √(cr * cr + t₃ * y * (t₃ * y))
Tactic: have hcr₃val : cr₃ = √(cr * cr + t₃ * y * (t₃ * y)) := by
      obtain ⟨p0, hp0⟩ := hnps
      have h' : ↑(⟨cc, hcc₃'⟩ : s) = cc := rfl
      rw [← dist_of_mem_subset_mk_sphere (Set.mem_insert_of_mem _ hp0) hcr₃, hcc₃'', ←
        mul_self_inj_of_nonneg dist_nonneg (Real.sqrt_nonneg _),
        Real.mul_self_sqrt (add_nonneg (mul_self_nonneg _) (mul_self_nonneg _)),
        dist_sq_eq_dist_orthogonalProjection_sq_add_dist_orthogonalProjection_sq _ (hps hp0),
        orthogonalProjection_vadd_smul_vsub_orthogonalProjection _ _ hcc₃', h',
        dist_of_mem_subset_mk_sphere hp0 hcr, dist_eq_norm_vsub V _ cc, vadd_vsub, norm_smul, ←
        dist_eq_norm_vsub V p, Real.norm_eq_abs, ← mul_assoc, mul_comm _ |t₃|, ← mul_assoc,
        abs_mul_abs_self]
      ring
-- 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₃ : ℝ
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
hcr₃val : cr₃ = √(cr * cr + t₃ * y * (t₃ * y))
⊢ Eq (α := Sphere P) { center := cc₃, radius := cr₃ } { center := cc₂, radius := cr₂ }
have hcr₄ : dist p cc₃ = cr₃
Tactic: replace hcr₃ := dist_of_mem_subset_mk_sphere (Set.mem_insert _ _) 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₃
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
hcr₃val : cr₃ = √(cr * cr + t₃ * y * (t₃ * y))
hcr₃ : dist p cc₃ = cr₃
⊢ Eq (α := Sphere P) { center := cc₃, radius := cr₃ } { center := cc₂, radius := cr₂ }
have hcr₄ : dist cc (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) *
      dist cc (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) +
    (1 - t₃) * (1 - t₃) *
      (dist p (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) *
        dist p (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)) =
  cr * cr + t₃ * y * (t₃ * y)
Tactic: rw [hpo, hcc₃'', hcr₃val, ← mul_self_inj_of_nonneg dist_nonneg (Real.sqrt_nonneg _),
      dist_sq_smul_orthogonal_vadd_smul_orthogonal_vadd (orthogonalProjection_mem p) hcc₃' _ _
        (vsub_orthogonalProjection_mem_direction_orthogonal s p),
      Real.norm_eq_abs, abs_mul_abs_self, dist_comm, ← dist_eq_norm_vsub V p,
      Real.mul_self_sqrt (add_nonneg (mul_self_nonneg _) (mul_self_nonneg _))] at 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₃
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
hcr₃val : cr₃ = √(cr * cr + t₃ * y * (t₃ * y))
hcr₃ :
  dist cc (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) *
        dist cc (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) +
      (1 - t₃) * (1 - t₃) *
        (dist p (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) *
          dist p (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)) =
    cr * cr + t₃ * y * (t₃ * y)
⊢ Eq (α := Sphere P) { center := cc₃, radius := cr₃ } { center := cc₂, radius := cr₂ }
have this₁ : t₃ * y = ycc₂
Tactic: have : t₃ * y = ycc₂ := by grind
-- 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
ι : Type u_3
hne : Nonempty ι
inst_4 : Finite ι
p : ι → P
ha : AffineIndependent ℝ p
⊢ ∃! cs : Sphere P,
    Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range p)) cs.center ∧
      Set.range p ⊆ Metric.sphere cs.center cs.radius
have intro : ∀ (val : Fintype ι),
  ∃! cs : Sphere P,
    Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range p)) cs.center ∧
      Set.range p ⊆ Metric.sphere cs.center cs.radius
Tactic: cases nonempty_fintype ι
-- 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
ι : Type u_3
hne : Nonempty ι
inst_4 : Finite ι
p : ι → P
ha : AffineIndependent ℝ p
val : Fintype ι
hn : Fintype.card ι = 0
⊢ ∃! cs : Sphere P,
    Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range p)) cs.center ∧
      Set.range p ⊆ Metric.sphere cs.center cs.radius
have intro : False
Tactic: exfalso
-- 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
ι : Type u_3
hne : Nonempty ι
inst_4 : Finite ι
p : ι → P
ha : AffineIndependent ℝ p
val : Fintype ι
hn : Fintype.card ι = 0
⊢ False
have h : 0 < Fintype.card ι
Tactic: have h := Fintype.card_pos_iff.2 hne
-- 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
m : ℕ
hm :
  ∀ {ι : Type u_3} [hne : Nonempty ι] [Finite ι] {p : ι → P} (ha : AffineIndependent ℝ p) (val : Fintype ι)
    (hn : Fintype.card ι = m),
    ∃! cs : Sphere P,
      Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range p)) cs.center ∧
        Set.range p ⊆ Metric.sphere cs.center cs.radius
ι : Type u_3
hne : Nonempty ι
inst_4 : Finite ι
p : ι → P
ha : AffineIndependent ℝ p
val : Fintype ι
hn : Fintype.card ι = m + 1
⊢ ∃! cs : Sphere P,
    Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range p)) cs.center ∧
      Set.range p ⊆ Metric.sphere cs.center cs.radius
have intro : ∀
  (hm :
    ∀ {ι : Type u_3} [hne : Nonempty ι] [Finite ι] {p : ι → P} (ha : AffineIndependent ℝ p) (val : Fintype ι)
      (hn : Fintype.card ι = 0),
      ∃! cs : Sphere P,
        Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range p)) cs.center ∧
          Set.range p ⊆ Metric.sphere cs.center cs.radius)
  (hn : Fintype.card ι = HAdd.hAdd (α := ℕ) 0 1),
  ∃! cs : Sphere P,
    Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range p)) cs.center ∧
      Set.range p ⊆ Metric.sphere cs.center cs.radius
Tactic: rcases m with - | m
Cleared hypotheses: m, hm, hn
-- 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
m : ℕ
hm :
  ∀ {ι : Type u_3} [hne : Nonempty ι] [Finite ι] {p : ι → P} (ha : AffineIndependent ℝ p) (val : Fintype ι)
    (hn : Fintype.card ι = m),
    ∃! cs : Sphere P,
      Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range p)) cs.center ∧
        Set.range p ⊆ Metric.sphere cs.center cs.radius
ι : Type u_3
hne : Nonempty ι
inst_4 : Finite ι
p : ι → P
ha : AffineIndependent ℝ p
val : Fintype ι
hn : Fintype.card ι = m + 1
intro :
  ∀
    (hm :
      ∀ {ι : Type u_3} [hne : Nonempty ι] [Finite ι] {p : ι → P} (ha : AffineIndependent ℝ p) (val : Fintype ι)
        (hn : Fintype.card ι = 0),
        ∃! cs : Sphere P,
          Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range p)) cs.center ∧
            Set.range p ⊆ Metric.sphere cs.center cs.radius)
    (hn : Fintype.card ι = HAdd.hAdd (α := ℕ) 0 1),
    ∃! cs : Sphere P,
      Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range p)) cs.center ∧
        Set.range p ⊆ Metric.sphere cs.center cs.radius
⊢ ∃! cs : Sphere P,
    Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range p)) cs.center ∧
      Set.range p ⊆ Metric.sphere cs.center cs.radius
have intro₁ : ∀ (m : ℕ)
  (hm :
    ∀ {ι : Type u_3} [hne : Nonempty ι] [Finite ι] {p : ι → P} (ha : AffineIndependent ℝ p) (val : Fintype ι)
      (hn : Fintype.card ι = m + 1),
      ∃! cs : Sphere P,
        Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range p)) cs.center ∧
          Set.range p ⊆ Metric.sphere cs.center cs.radius)
  (hn : Fintype.card ι = m + 1 + 1),
  ∃! cs : Sphere P,
    Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range p)) cs.center ∧
      Set.range p ⊆ Metric.sphere cs.center cs.radius
Tactic: rcases m with - | m
Cleared hypotheses: m, hm, hn
-- 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
ι : Type u_3
hne : Nonempty ι
inst_4 : Finite ι
p : ι → P
ha : AffineIndependent ℝ p
val : Fintype ι
hm :
  ∀ {ι : Type u_3} [hne : Nonempty ι] [Finite ι] {p : ι → P} (ha : AffineIndependent ℝ p) (val : Fintype ι)
    (hn : Fintype.card ι = 0),
    ∃! cs : Sphere P,
      Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range p)) cs.center ∧
        Set.range p ⊆ Metric.sphere cs.center cs.radius
hn : Fintype.card ι = HAdd.hAdd (α := ℕ) 0 1
⊢ ∃! cs : Sphere P,
    Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range p)) cs.center ∧
      Set.range p ⊆ Metric.sphere cs.center cs.radius
have hn₁ : ∃ (x : ι), ∀ (y : ι), y = x
Tactic: rw [Fintype.card_eq_one_iff] at hn
Cleared hypotheses: hn
-- 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
ι : Type u_3
hne : Nonempty ι
inst_4 : Finite ι
p : ι → P
ha : AffineIndependent ℝ p
val : Fintype ι
hm :
  ∀ {ι : Type u_3} [hne : Nonempty ι] [Finite ι] {p : ι → P} (ha : AffineIndependent ℝ p) (val : Fintype ι)
    (hn : Fintype.card ι = 0),
    ∃! cs : Sphere P,
      Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range p)) cs.center ∧
        Set.range p ⊆ Metric.sphere cs.center cs.radius
hn : ∃ (x : ι), ∀ (y : ι), y = x
⊢ ∃! cs : Sphere P,
    Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range p)) cs.center ∧
      Set.range p ⊆ Metric.sphere cs.center cs.radius
have intro : ∀ (i : ι) (hi : ∀ (y : ι), y = i),
  ∃! cs : Sphere P,
    Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range p)) cs.center ∧
      Set.range p ⊆ Metric.sphere cs.center cs.radius
Tactic: obtain ⟨i, hi⟩ := hn
Cleared hypotheses: hn
-- 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
ι : Type u_3
hne : Nonempty ι
inst_4 : Finite ι
p : ι → P
ha : AffineIndependent ℝ p
val : Fintype ι
hm :
  ∀ {ι : Type u_3} [hne : Nonempty ι] [Finite ι] {p : ι → P} (ha : AffineIndependent ℝ p) (val : Fintype ι)
    (hn : Fintype.card ι = 0),
    ∃! cs : Sphere P,
      Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range p)) cs.center ∧
        Set.range p ⊆ Metric.sphere cs.center cs.radius
i : ι
hi : ∀ (y : ι), y = i
⊢ ∃! cs : Sphere P,
    Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range p)) cs.center ∧
      Set.range p ⊆ Metric.sphere cs.center cs.radius
have intro : ∀ (this : Unique ι),
  ∃! cs : Sphere P,
    Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range p)) cs.center ∧
      Set.range p ⊆ Metric.sphere cs.center cs.radius
Tactic: haveI : Unique ι := ⟨⟨i⟩, hi⟩
-- 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
ι : Type u_3
hne : Nonempty ι
inst_4 : Finite ι
p : ι → P
ha : AffineIndependent ℝ p
val : Fintype ι
hm :
  ∀ {ι : Type u_3} [hne : Nonempty ι] [Finite ι] {p : ι → P} (ha : AffineIndependent ℝ p) (val : Fintype ι)
    (hn : Fintype.card ι = 0),
    ∃! cs : Sphere P,
      Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range p)) cs.center ∧
        Set.range p ⊆ Metric.sphere cs.center cs.radius
i : ι
hi : ∀ (y : ι), y = i
this : Unique ι
⊢ ∃! cs : Sphere P,
    Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range p)) cs.center ∧
      Set.range p ⊆ Metric.sphere cs.center cs.radius
have h : (fun (cs : Sphere P) ↦
      Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range p)) cs.center ∧
        Set.range p ⊆ Metric.sphere cs.center cs.radius)
    { center := p i, radius := 0 } ∧
  ∀ (y : Sphere P),
    (fun (cs : Sphere P) ↦
          Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range p)) cs.center ∧
            Set.range p ⊆ Metric.sphere cs.center cs.radius)
        y →
      y = { center := p i, radius := 0 }
Tactic: use ⟨p i, 0⟩
-- 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
ι : Type u_3
hne : Nonempty ι
inst_4 : Finite ι
p : ι → P
ha : AffineIndependent ℝ p
val : Fintype ι
hm :
  ∀ {ι : Type u_3} [hne : Nonempty ι] [Finite ι] {p : ι → P} (ha : AffineIndependent ℝ p) (val : Fintype ι)
    (hn : Fintype.card ι = 0),
    ∃! cs : Sphere P,
      Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range p)) cs.center ∧
        Set.range p ⊆ Metric.sphere cs.center cs.radius
i : ι
hi : ∀ (y : ι), y = i
this : Unique ι
⊢ (fun (cs : Sphere P) ↦
        Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range p)) cs.center ∧
          Set.range p ⊆ Metric.sphere cs.center cs.radius)
      { center := p i, radius := 0 } ∧
    ∀ (y : Sphere P),
      (fun (cs : Sphere P) ↦
            Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range p)) cs.center ∧
              Set.range p ⊆ Metric.sphere cs.center cs.radius)
          y →
        y = { center := p i, radius := 0 }
have h : (p i = p default ∧ {p default} ⊆ Metric.sphere (p i) 0) ∧
  ∀ (y : Sphere P),
    y.center = p default ∧ {p default} ⊆ Metric.sphere y.center y.radius → y = { center := p i, radius := 0 }
Tactic: simp only [Set.range_unique, AffineSubspace.mem_affineSpan_singleton]
-- 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
ι : Type u_3
hne : Nonempty ι
inst_4 : Finite ι
p : ι → P
ha : AffineIndependent ℝ p
val : Fintype ι
hm :
  ∀ {ι : Type u_3} [hne : Nonempty ι] [Finite ι] {p : ι → P} (ha : AffineIndependent ℝ p) (val : Fintype ι)
    (hn : Fintype.card ι = 0),
    ∃! cs : Sphere P,
      Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range p)) cs.center ∧
        Set.range p ⊆ Metric.sphere cs.center cs.radius
i : ι
hi : ∀ (y : ι), y = i
this : Unique ι
⊢ (p i = p default ∧ {p default} ⊆ Metric.sphere (p i) 0) ∧
    ∀ (y : Sphere P),
      y.center = p default ∧ {p default} ⊆ Metric.sphere y.center y.radius → y = { center := p i, radius := 0 }
have h : p i = p default ∧ {p default} ⊆ Metric.sphere (p i) 0
Tactic: constructor