awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst_4 : s.direction.HasOrthogonalProjection
ps : Set P
hnps : ps.Nonempty
p : P
hps : ps ⊆ (↑s : Set P)
hp : p ∉ s
this : Nonempty.{u_2 + 1} ↥s
cc : P
cr : ℝ
hcccru : ∀ (y : Sphere P), y.center ∈ s ∧ ps ⊆ Metric.sphere y.center y.radius → y = { center := cc, radius := cr }
hcc : cc ∈ s
hcr : ps ⊆ Metric.sphere cc cr
x : ℝ := dist cc (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)
y : ℝ := dist p (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)
hy0 : y ≠ 0
ycc₂ : ℝ := (x * x + y * y - cr * cr) / (2 * y)
cc₂ : P := (ycc₂ / y) • (p -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)) +ᵥ cc
cr₂ : ℝ := √(cr * cr + ycc₂ * ycc₂)
hpo :
  p =
    HVAdd.hVAdd (β := P) (HSMul.hSMul (α := ℝ) 1 (p -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)))
      (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)
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₃
⊢ 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₃

Premises used: mul_self_nonneg, EuclideanGeometry.vsub_orthogonalProjection_mem_direction_orthogonal, mul_self_inj_of_nonneg, dist_nonneg, Real.mul_self_sqrt, add_nonneg, dist_comm, EuclideanGeometry.orthogonalProjection_mem, EuclideanGeometry.dist_sq_smul_orthogonal_vadd_smul_orthogonal_vadd, abs_mul_abs_self, dist_eq_norm_vsub, Real.sqrt_nonneg, Real.norm_eq_abs
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst_4 : s.direction.HasOrthogonalProjection
ps : Set P
hnps : ps.Nonempty
p : P
hps : ps ⊆ (↑s : Set P)
hp : p ∉ s
this : Nonempty.{u_2 + 1} ↥s
cc : P
cr : ℝ
hcccru : ∀ (y : Sphere P), y.center ∈ s ∧ ps ⊆ Metric.sphere y.center y.radius → y = { center := cc, radius := cr }
hcc : cc ∈ s
hcr : ps ⊆ Metric.sphere cc cr
x : ℝ := dist cc (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)
y : ℝ := dist p (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)
hy0 : y ≠ 0
ycc₂ : ℝ := (x * x + y * y - cr * cr) / (2 * y)
cc₂ : P := (ycc₂ / y) • (p -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)) +ᵥ cc
cr₂ : ℝ := √(cr * cr + ycc₂ * ycc₂)
hpo :
  p =
    HVAdd.hVAdd (β := P) (HSMul.hSMul (α := ℝ) 1 (p -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)))
      (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)
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)
⊢ t₃ * y = ycc₂

Tactic:
grind
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst_4 : s.direction.HasOrthogonalProjection
ps : Set P
hnps : ps.Nonempty
p : P
hps : ps ⊆ (↑s : Set P)
hp : p ∉ s
this : Nonempty.{u_2 + 1} ↥s
cc : P
cr : ℝ
hcccru : ∀ (y : Sphere P), y.center ∈ s ∧ ps ⊆ Metric.sphere y.center y.radius → y = { center := cc, radius := cr }
hcc : cc ∈ s
hcr : ps ⊆ Metric.sphere cc cr
x : ℝ := dist cc (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)
y : ℝ := dist p (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)
hy0 : y ≠ 0
ycc₂ : ℝ := (x * x + y * y - cr * cr) / (2 * y)
cc₂ : P := (ycc₂ / y) • (p -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)) +ᵥ cc
cr₂ : ℝ := √(cr * cr + ycc₂ * ycc₂)
hpo :
  p =
    HVAdd.hVAdd (β := P) (HSMul.hSMul (α := ℝ) 1 (p -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)))
      (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)
cc₃ : P
cr₃ : ℝ
hcc₃ : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (insert p (↑s : Set P))) cc₃
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)
⊢ t₃ * y = ycc₂

Tactic:
have : t₃ * y = ycc₂ := by grind
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst_4 : s.direction.HasOrthogonalProjection
ps : Set P
hnps : ps.Nonempty
p : P
hps : ps ⊆ (↑s : Set P)
hp : p ∉ s
this_1 : 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)
this : t₃ * y = ycc₂
⊢ Eq (α := Sphere P) { center := cc₃, radius := cr₃ } { center := cc₂, radius := cr₂ }

Tactic:
grind
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
ι : Type u_3
hne : Nonempty ι
inst_4 : Finite ι
p : ι → P
ha : AffineIndependent ℝ p
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
⊢ ∃! 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 ι

Premises used: nonempty_fintype
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
ι : Type u_3
hne : Nonempty ι
inst_4 : Finite ι
p : ι → P
ha : AffineIndependent ℝ p
val : Fintype ι
hn : Fintype.card ι = 0
intro : False
⊢ ∃! cs : Sphere P,
    Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range p)) cs.center ∧
      Set.range p ⊆ Metric.sphere cs.center cs.radius

Tactic:
exfalso
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
ι : Type u_3
hne : Nonempty ι
inst_4 : Finite ι
p : ι → P
ha : AffineIndependent ℝ p
val : Fintype ι
hn : Fintype.card ι = 0
⊢ 0 < Fintype.card ι

Tactic:
have h := Fintype.card_pos_iff.2 hne
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
ι : Type u_3
hne : Nonempty ι
inst_4 : Finite ι
p : ι → P
ha : AffineIndependent ℝ p
val : Fintype ι
hn : Fintype.card ι = 0
h : 0 < Fintype.card ι
⊢ False

Tactic:
lia
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
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
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
⊢ ∃! 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
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
ι : 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
⊢ ∃ (x : ι), ∀ (y : ι), y = x

Tactic:
rw [Fintype.card_eq_one_iff] at hn

Premises used: Fintype.card_eq_one_iff
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
ι : 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
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
⊢ ∃! 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
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
ι : 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
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
⊢ ∃! 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⟩
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
ι : 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 ι
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 }
⊢ ∃! cs : Sphere P,
    Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range p)) cs.center ∧
      Set.range p ⊆ Metric.sphere cs.center cs.radius

Tactic:
use ⟨p i, 0⟩
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
ι : 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 ι
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 }
⊢ (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:
simp only [Set.range_unique, AffineSubspace.mem_affineSpan_singleton]

Premises used: Set.range_unique, AffineSubspace.mem_affineSpan_singleton
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
ι : 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 ι
h : p i = p default ∧ {p default} ⊆ Metric.sphere (p i) 0
h₁ :
  ∀ (y : Sphere P),
    y.center = p default ∧ {p default} ⊆ Metric.sphere y.center y.radius → y = { center := p i, radius := 0 }
⊢ (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:
constructor
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
ι : 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 ι
h : True ∧ p i ∈ Metric.sphere (p i) 0
⊢ p i = p default ∧ {p default} ⊆ Metric.sphere (p i) 0

Tactic:
simp_rw [hi default, Set.singleton_subset_iff]

Premises used: Set.singleton_subset_iff, Inhabited.default
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
ι : 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 ∈ Metric.sphere (p i) 0

Tactic:
simp only [Metric.sphere_zero, Set.mem_singleton_iff]

Premises used: Metric.sphere_zero, Set.mem_singleton_iff
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
ι : 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 ι
⊢ True ∧ p i ∈ Metric.sphere (p i) 0

Tactic:
exact ⟨⟨⟩, by simp only [Metric.sphere_zero, Set.mem_singleton_iff]⟩
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
ι : 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 ι
cr : ℝ
hdist :
  {p default} ⊆
    Metric.sphere (Sphere.center { center := p default, radius := cr : Sphere P })
      (Sphere.radius { center := p default, radius := cr : Sphere P })
⊢ 0 = cr

Tactic:
simpa using hdist
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
ι : 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 ι
cr : ℝ
hdist :
  {p default} ⊆
    Metric.sphere (Sphere.center { center := p default, radius := cr : Sphere P })
      (Sphere.radius { center := p default, radius := cr : Sphere P })
⊢ 0 = cr

Tactic:
replace hdist : 0 = cr := by simpa using hdist
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
ι : 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 ι
cr : ℝ
hdist : 0 = cr
h : Eq (α := Sphere P) { center := p i, radius := cr } { center := p i, radius := 0 }
h₁ h₂ : Eq (α := Sphere P) { center := p i, radius := cr } { center := p i, radius := cr }
⊢ Eq (α := Sphere P) { center := p default, radius := cr } { center := p i, radius := 0 }

Tactic:
rw [hi default, hdist]

Premises used: Inhabited.default