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
n : ℕ
s : Simplex ℝ P n
p p₁ p₂ : P
r : ℝ
hp₁ : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (insert p (Set.range s.points))) p₁
hp₂ : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (insert p (Set.range s.points))) p₂
h₁ : ∀ (i : Fin (n + 1)), dist (s.points i) p₁ = r
h₂ : ∀ (i : Fin (n + 1)), dist (s.points i) p₂ = r
span_s : AffineSubspace ℝ P := affineSpan ℝ (Set.range s.points)
h₁' : (↑((s.orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range s.points))) p₁) : P) = s.circumcenter
h₂' : (↑((s.orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range s.points))) p₂) : P) = s.circumcenter
⊢ ∃ (r : ℝ) (p0 : P),
    Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points)) p0 ∧
      p₁ =
        r •
            (p -ᵥ
              (↑((orthogonalProjection (affineSpan ℝ (Set.range s.points)) :
                      (a : P) → ↥(affineSpan ℝ (Set.range s.points)))
                    p) :
                P)) +ᵥ
          p0

Tactic:
rw [← affineSpan_insert_affineSpan, mem_affineSpan_insert_iff (orthogonalProjection_mem p)]
    at hp₁ hp₂

Premises used: AffineSubspace.mem_affineSpan_insert_iff, EuclideanGeometry.orthogonalProjection_mem, affineSpan_insert_affineSpan
-- 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
n : ℕ
s : Simplex ℝ P n
p p₁ p₂ : P
r : ℝ
hp₁ : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (insert p (Set.range s.points))) p₁
hp₂ : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (insert p (Set.range s.points))) p₂
h₁ : ∀ (i : Fin (n + 1)), dist (s.points i) p₁ = r
h₂ : ∀ (i : Fin (n + 1)), dist (s.points i) p₂ = r
span_s : AffineSubspace ℝ P := affineSpan ℝ (Set.range s.points)
h₁' : (↑((s.orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range s.points))) p₁) : P) = s.circumcenter
h₂' : (↑((s.orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range s.points))) p₂) : P) = s.circumcenter
hp₃ :
  ∃ (r : ℝ) (p0 : P),
    Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points)) p0 ∧
      p₁ =
        r •
            (p -ᵥ
              (↑((orthogonalProjection (affineSpan ℝ (Set.range s.points)) :
                      (a : P) → ↥(affineSpan ℝ (Set.range s.points)))
                    p) :
                P)) +ᵥ
          p0
⊢ ∃ (r : ℝ) (p0 : P),
    Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points)) p0 ∧
      p₂ =
        r •
            (p -ᵥ
              (↑((orthogonalProjection (affineSpan ℝ (Set.range s.points)) :
                      (a : P) → ↥(affineSpan ℝ (Set.range s.points)))
                    p) :
                P)) +ᵥ
          p0

Tactic:
rw [← affineSpan_insert_affineSpan, mem_affineSpan_insert_iff (orthogonalProjection_mem p)]
    at hp₁ hp₂

Premises used: AffineSubspace.mem_affineSpan_insert_iff, EuclideanGeometry.orthogonalProjection_mem, affineSpan_insert_affineSpan
-- 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
n : ℕ
s : Simplex ℝ P n
p p₁ p₂ : P
r : ℝ
hp₁ : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (insert p (Set.range s.points))) p₁
hp₂ : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (insert p (Set.range s.points))) p₂
h₁ : ∀ (i : Fin (n + 1)), dist (s.points i) p₁ = r
h₂ : ∀ (i : Fin (n + 1)), dist (s.points i) p₂ = r
span_s : AffineSubspace ℝ P := affineSpan ℝ (Set.range s.points)
h₁' : (↑((s.orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range s.points))) p₁) : P) = s.circumcenter
h₂' : (↑((s.orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range s.points))) p₂) : P) = s.circumcenter
hp₃ :
  ∃ (r : ℝ) (p0 : P),
    Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points)) p0 ∧
      p₁ =
        r •
            (p -ᵥ
              (↑((orthogonalProjection (affineSpan ℝ (Set.range s.points)) :
                      (a : P) → ↥(affineSpan ℝ (Set.range s.points)))
                    p) :
                P)) +ᵥ
          p0
hp₄ :
  ∃ (r : ℝ) (p0 : P),
    Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points)) p0 ∧
      p₂ =
        r •
            (p -ᵥ
              (↑((orthogonalProjection (affineSpan ℝ (Set.range s.points)) :
                      (a : P) → ↥(affineSpan ℝ (Set.range s.points)))
                    p) :
                P)) +ᵥ
          p0
⊢ ∀ (i : Fin (n + 1)), dist (s.points i) p₁ = r

Tactic:
rw [← affineSpan_insert_affineSpan, mem_affineSpan_insert_iff (orthogonalProjection_mem p)]
    at hp₁ hp₂

Premises used: AffineSubspace.mem_affineSpan_insert_iff, EuclideanGeometry.orthogonalProjection_mem, affineSpan_insert_affineSpan
-- 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
n : ℕ
s : Simplex ℝ P n
p p₁ p₂ : P
r : ℝ
hp₁ : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (insert p (Set.range s.points))) p₁
hp₂ : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (insert p (Set.range s.points))) p₂
h₁ : ∀ (i : Fin (n + 1)), dist (s.points i) p₁ = r
h₂ : ∀ (i : Fin (n + 1)), dist (s.points i) p₂ = r
span_s : AffineSubspace ℝ P := affineSpan ℝ (Set.range s.points)
h₁' : (↑((s.orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range s.points))) p₁) : P) = s.circumcenter
h₂' : (↑((s.orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range s.points))) p₂) : P) = s.circumcenter
hp₃ :
  ∃ (r : ℝ) (p0 : P),
    Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points)) p0 ∧
      p₁ =
        r •
            (p -ᵥ
              (↑((orthogonalProjection (affineSpan ℝ (Set.range s.points)) :
                      (a : P) → ↥(affineSpan ℝ (Set.range s.points)))
                    p) :
                P)) +ᵥ
          p0
hp₄ :
  ∃ (r : ℝ) (p0 : P),
    Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points)) p0 ∧
      p₂ =
        r •
            (p -ᵥ
              (↑((orthogonalProjection (affineSpan ℝ (Set.range s.points)) :
                      (a : P) → ↥(affineSpan ℝ (Set.range s.points)))
                    p) :
                P)) +ᵥ
          p0
h₃ : ∀ (i : Fin (n + 1)), dist (s.points i) p₁ = r
⊢ ∀ (i : Fin (n + 1)), dist (s.points i) p₂ = r

Tactic:
rw [← affineSpan_insert_affineSpan, mem_affineSpan_insert_iff (orthogonalProjection_mem p)]
    at hp₁ hp₂

Premises used: AffineSubspace.mem_affineSpan_insert_iff, EuclideanGeometry.orthogonalProjection_mem, affineSpan_insert_affineSpan
-- 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
n : ℕ
s : Simplex ℝ P n
p p₁ p₂ : P
r : ℝ
hp₁ : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (insert p (Set.range s.points))) p₁
hp₂ : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (insert p (Set.range s.points))) p₂
h₁ : ∀ (i : Fin (n + 1)), dist (s.points i) p₁ = r
h₂ : ∀ (i : Fin (n + 1)), dist (s.points i) p₂ = r
span_s : AffineSubspace ℝ P := affineSpan ℝ (Set.range s.points)
h₁' : (↑((s.orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range s.points))) p₁) : P) = s.circumcenter
h₂' : (↑((s.orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range s.points))) p₂) : P) = s.circumcenter
hp₃ :
  ∃ (r : ℝ) (p0 : P),
    Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points)) p0 ∧
      p₁ =
        r •
            (p -ᵥ
              (↑((orthogonalProjection (affineSpan ℝ (Set.range s.points)) :
                      (a : P) → ↥(affineSpan ℝ (Set.range s.points)))
                    p) :
                P)) +ᵥ
          p0
hp₄ :
  ∃ (r : ℝ) (p0 : P),
    Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points)) p0 ∧
      p₂ =
        r •
            (p -ᵥ
              (↑((orthogonalProjection (affineSpan ℝ (Set.range s.points)) :
                      (a : P) → ↥(affineSpan ℝ (Set.range s.points)))
                    p) :
                P)) +ᵥ
          p0
h₃ : ∀ (i : Fin (n + 1)), dist (s.points i) p₁ = r
h₄ : ∀ (i : Fin (n + 1)), dist (s.points i) p₂ = r
⊢ (↑((s.orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range s.points))) p₁) : P) = s.circumcenter

Tactic:
rw [← affineSpan_insert_affineSpan, mem_affineSpan_insert_iff (orthogonalProjection_mem p)]
    at hp₁ hp₂

Premises used: AffineSubspace.mem_affineSpan_insert_iff, EuclideanGeometry.orthogonalProjection_mem, affineSpan_insert_affineSpan
-- 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
n : ℕ
s : Simplex ℝ P n
p p₁ p₂ : P
r : ℝ
hp₁ : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (insert p (Set.range s.points))) p₁
hp₂ : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (insert p (Set.range s.points))) p₂
h₁ : ∀ (i : Fin (n + 1)), dist (s.points i) p₁ = r
h₂ : ∀ (i : Fin (n + 1)), dist (s.points i) p₂ = r
span_s : AffineSubspace ℝ P := affineSpan ℝ (Set.range s.points)
h₁' : (↑((s.orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range s.points))) p₁) : P) = s.circumcenter
h₂' : (↑((s.orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range s.points))) p₂) : P) = s.circumcenter
hp₃ :
  ∃ (r : ℝ) (p0 : P),
    Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points)) p0 ∧
      p₁ =
        r •
            (p -ᵥ
              (↑((orthogonalProjection (affineSpan ℝ (Set.range s.points)) :
                      (a : P) → ↥(affineSpan ℝ (Set.range s.points)))
                    p) :
                P)) +ᵥ
          p0
hp₄ :
  ∃ (r : ℝ) (p0 : P),
    Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points)) p0 ∧
      p₂ =
        r •
            (p -ᵥ
              (↑((orthogonalProjection (affineSpan ℝ (Set.range s.points)) :
                      (a : P) → ↥(affineSpan ℝ (Set.range s.points)))
                    p) :
                P)) +ᵥ
          p0
h₃ : ∀ (i : Fin (n + 1)), dist (s.points i) p₁ = r
h₄ : ∀ (i : Fin (n + 1)), dist (s.points i) p₂ = r
h₁'₁ : (↑((s.orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range s.points))) p₁) : P) = s.circumcenter
⊢ (↑((s.orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range s.points))) p₂) : P) = s.circumcenter

Tactic:
rw [← affineSpan_insert_affineSpan, mem_affineSpan_insert_iff (orthogonalProjection_mem p)]
    at hp₁ hp₂

Premises used: AffineSubspace.mem_affineSpan_insert_iff, EuclideanGeometry.orthogonalProjection_mem, affineSpan_insert_affineSpan
-- 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
n : ℕ
s : Simplex ℝ P n
p p₁ p₂ : P
r : ℝ
hp₁ :
  ∃ (r : ℝ) (p0 : P),
    Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points)) p0 ∧
      p₁ =
        r •
            (p -ᵥ
              (↑((orthogonalProjection (affineSpan ℝ (Set.range s.points)) :
                      (a : P) → ↥(affineSpan ℝ (Set.range s.points)))
                    p) :
                P)) +ᵥ
          p0
hp₂ :
  ∃ (r : ℝ) (p0 : P),
    Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points)) p0 ∧
      p₂ =
        r •
            (p -ᵥ
              (↑((orthogonalProjection (affineSpan ℝ (Set.range s.points)) :
                      (a : P) → ↥(affineSpan ℝ (Set.range s.points)))
                    p) :
                P)) +ᵥ
          p0
h₁ : ∀ (i : Fin (n + 1)), dist (s.points i) p₁ = r
h₂ : ∀ (i : Fin (n + 1)), dist (s.points i) p₂ = r
span_s : AffineSubspace ℝ P := affineSpan ℝ (Set.range s.points)
h₁' : (↑((s.orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range s.points))) p₁) : P) = s.circumcenter
h₂' : (↑((s.orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range s.points))) p₂) : P) = s.circumcenter
obtain :
  ∀ (r₁ : ℝ) (p₁o : P) (hp₁o : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points)) p₁o)
    (hp₁ :
      p₁ =
        r₁ •
            (p -ᵥ
              (↑((orthogonalProjection (affineSpan ℝ (Set.range s.points)) :
                      (a : P) → ↥(affineSpan ℝ (Set.range s.points)))
                    p) :
                P)) +ᵥ
          p₁o),
    p₁ = p₂ ∨ p₁ = (reflection (affineSpan ℝ (Set.range s.points)) : (a : P) → P) p₂
⊢ p₁ = p₂ ∨ p₁ = (reflection (affineSpan ℝ (Set.range s.points)) : (a : P) → P) p₂

Tactic:
obtain ⟨r₁, p₁o, hp₁o, hp₁⟩ := hp₁
-- 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
n : ℕ
s : Simplex ℝ P n
p p₁ p₂ : P
r : ℝ
hp₂ :
  ∃ (r : ℝ) (p0 : P),
    Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points)) p0 ∧
      p₂ =
        r •
            (p -ᵥ
              (↑((orthogonalProjection (affineSpan ℝ (Set.range s.points)) :
                      (a : P) → ↥(affineSpan ℝ (Set.range s.points)))
                    p) :
                P)) +ᵥ
          p0
h₁ : ∀ (i : Fin (n + 1)), dist (s.points i) p₁ = r
h₂ : ∀ (i : Fin (n + 1)), dist (s.points i) p₂ = r
span_s : AffineSubspace ℝ P := affineSpan ℝ (Set.range s.points)
h₁' : (↑((s.orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range s.points))) p₁) : P) = s.circumcenter
h₂' : (↑((s.orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range s.points))) p₂) : P) = s.circumcenter
r₁ : ℝ
p₁o : P
hp₁o : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points)) p₁o
hp₁ :
  p₁ =
    r₁ •
        (p -ᵥ
          (↑((orthogonalProjection (affineSpan ℝ (Set.range s.points)) : (a : P) → ↥(affineSpan ℝ (Set.range s.points)))
                p) :
            P)) +ᵥ
      p₁o
obtain :
  ∀ (r₂ : ℝ) (p₂o : P) (hp₂o : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points)) p₂o)
    (hp₂ :
      p₂ =
        r₂ •
            (p -ᵥ
              (↑((orthogonalProjection (affineSpan ℝ (Set.range s.points)) :
                      (a : P) → ↥(affineSpan ℝ (Set.range s.points)))
                    p) :
                P)) +ᵥ
          p₂o),
    p₁ = p₂ ∨ p₁ = (reflection (affineSpan ℝ (Set.range s.points)) : (a : P) → P) p₂
⊢ p₁ = p₂ ∨ p₁ = (reflection (affineSpan ℝ (Set.range s.points)) : (a : P) → P) p₂

Tactic:
obtain ⟨r₂, p₂o, hp₂o, hp₂⟩ := hp₂
-- 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
n : ℕ
s : Simplex ℝ P n
p p₁ p₂ : P
r : ℝ
h₁ : ∀ (i : Fin (n + 1)), dist (s.points i) p₁ = r
h₂ : ∀ (i : Fin (n + 1)), dist (s.points i) p₂ = r
span_s : AffineSubspace ℝ P := affineSpan ℝ (Set.range s.points)
h₁' : (↑((s.orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range s.points))) p₁) : P) = s.circumcenter
h₂' : (↑((s.orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range s.points))) p₂) : P) = s.circumcenter
r₁ : ℝ
p₁o : P
hp₁o : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points)) p₁o
hp₁ :
  p₁ =
    r₁ •
        (p -ᵥ
          (↑((orthogonalProjection (affineSpan ℝ (Set.range s.points)) : (a : P) → ↥(affineSpan ℝ (Set.range s.points)))
                p) :
            P)) +ᵥ
      p₁o
r₂ : ℝ
p₂o : P
hp₂o : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points)) p₂o
hp₂ :
  p₂ =
    r₂ •
        (p -ᵥ
          (↑((orthogonalProjection (affineSpan ℝ (Set.range s.points)) : (a : P) → ↥(affineSpan ℝ (Set.range s.points)))
                p) :
            P)) +ᵥ
      p₂o
subst :
  ∀
    (h₁ :
      ∀ (i : Fin (n + 1)),
        dist (s.points i)
            (r₁ •
                (p -ᵥ
                  (↑((orthogonalProjection (affineSpan ℝ (Set.range s.points)) :
                          (a : P) → ↥(affineSpan ℝ (Set.range s.points)))
                        p) :
                    P)) +ᵥ
              p₁o) =
          r)
    (h₁' :
      (↑((s.orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range s.points)))
              (r₁ •
                  (p -ᵥ
                    (↑((orthogonalProjection (affineSpan ℝ (Set.range s.points)) :
                            (a : P) → ↥(affineSpan ℝ (Set.range s.points)))
                          p) :
                      P)) +ᵥ
                p₁o)) :
          P) =
        s.circumcenter),
    (↑((s.orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range s.points)))
            (r₁ •
                (p -ᵥ
                  (↑((orthogonalProjection (affineSpan ℝ (Set.range s.points)) :
                          (a : P) → ↥(affineSpan ℝ (Set.range s.points)))
                        p) :
                    P)) +ᵥ
              p₁o)) :
        P) =
      p₁o
⊢ (↑((s.orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range s.points))) p₁) : P) = p₁o

Tactic:
subst hp₁
-- 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
n : ℕ
s : Simplex ℝ P n
p p₂ : P
r : ℝ
h₂ : ∀ (i : Fin (n + 1)), dist (s.points i) p₂ = r
span_s : AffineSubspace ℝ P := affineSpan ℝ (Set.range s.points)
h₂' : (↑((s.orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range s.points))) p₂) : P) = s.circumcenter
r₁ : ℝ
p₁o : P
hp₁o : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points)) p₁o
r₂ : ℝ
p₂o : P
hp₂o : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points)) p₂o
hp₂ :
  p₂ =
    r₂ •
        (p -ᵥ
          (↑((orthogonalProjection (affineSpan ℝ (Set.range s.points)) : (a : P) → ↥(affineSpan ℝ (Set.range s.points)))
                p) :
            P)) +ᵥ
      p₂o
h₁ :
  ∀ (i : Fin (n + 1)),
    dist (s.points i)
        (r₁ •
            (p -ᵥ
              (↑((orthogonalProjection (affineSpan ℝ (Set.range s.points)) :
                      (a : P) → ↥(affineSpan ℝ (Set.range s.points)))
                    p) :
                P)) +ᵥ
          p₁o) =
      r
h₁' :
  (↑((s.orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range s.points)))
          (r₁ •
              (p -ᵥ
                (↑((orthogonalProjection (affineSpan ℝ (Set.range s.points)) :
                        (a : P) → ↥(affineSpan ℝ (Set.range s.points)))
                      p) :
                  P)) +ᵥ
            p₁o)) :
      P) =
    s.circumcenter
⊢ (↑((s.orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range s.points)))
          (r₁ •
              (p -ᵥ
                (↑((orthogonalProjection (affineSpan ℝ (Set.range s.points)) :
                        (a : P) → ↥(affineSpan ℝ (Set.range s.points)))
                      p) :
                  P)) +ᵥ
            p₁o)) :
      P) =
    p₁o

Tactic:
s.coe_orthogonalProjection_vadd_smul_vsub_orthogonalProjection hp₁o

Premises used: Set.Mem, Affine.Simplex.coe_orthogonalProjection_vadd_smul_vsub_orthogonalProjection
-- 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
n : ℕ
s : Simplex ℝ P n
p p₂ : P
r : ℝ
h₂ : ∀ (i : Fin (n + 1)), dist (s.points i) p₂ = r
span_s : AffineSubspace ℝ P := affineSpan ℝ (Set.range s.points)
h₂' : (↑((s.orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range s.points))) p₂) : P) = s.circumcenter
r₁ : ℝ
p₁o : P
hp₁o : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points)) p₁o
r₂ : ℝ
p₂o : P
hp₂o : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points)) p₂o
hp₂ :
  p₂ =
    r₂ •
        (p -ᵥ
          (↑((orthogonalProjection (affineSpan ℝ (Set.range s.points)) : (a : P) → ↥(affineSpan ℝ (Set.range s.points)))
                p) :
            P)) +ᵥ
      p₂o
h₁ :
  ∀ (i : Fin (n + 1)),
    dist (s.points i)
        (r₁ •
            (p -ᵥ
              (↑((orthogonalProjection (affineSpan ℝ (Set.range s.points)) :
                      (a : P) → ↥(affineSpan ℝ (Set.range s.points)))
                    p) :
                P)) +ᵥ
          p₁o) =
      r
h₁' :
  (↑((s.orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range s.points)))
          (r₁ •
              (p -ᵥ
                (↑((orthogonalProjection (affineSpan ℝ (Set.range s.points)) :
                        (a : P) → ↥(affineSpan ℝ (Set.range s.points)))
                      p) :
                  P)) +ᵥ
            p₁o)) :
      P) =
    s.circumcenter
⊢ (↑((s.orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range s.points)))
          (r₁ •
              (p -ᵥ
                (↑((orthogonalProjection (affineSpan ℝ (Set.range s.points)) :
                        (a : P) → ↥(affineSpan ℝ (Set.range s.points)))
                      p) :
                  P)) +ᵥ
            p₁o)) :
      P) =
    p₁o

Tactic:
exact s.coe_orthogonalProjection_vadd_smul_vsub_orthogonalProjection hp₁o

Premises used: Affine.Simplex.coe_orthogonalProjection_vadd_smul_vsub_orthogonalProjection
-- 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
n : ℕ
s : Simplex ℝ P n
p p₁ p₂ : P
r : ℝ
h₁ : ∀ (i : Fin (n + 1)), dist (s.points i) p₁ = r
h₂ : ∀ (i : Fin (n + 1)), dist (s.points i) p₂ = r
span_s : AffineSubspace ℝ P := affineSpan ℝ (Set.range s.points)
h₁' : (↑((s.orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range s.points))) p₁) : P) = s.circumcenter
h₂' : (↑((s.orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range s.points))) p₂) : P) = s.circumcenter
r₁ : ℝ
p₁o : P
hp₁o : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points)) p₁o
hp₁ :
  p₁ =
    r₁ •
        (p -ᵥ
          (↑((orthogonalProjection (affineSpan ℝ (Set.range s.points)) : (a : P) → ↥(affineSpan ℝ (Set.range s.points)))
                p) :
            P)) +ᵥ
      p₁o
r₂ : ℝ
p₂o : P
hp₂o : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points)) p₂o
hp₂ :
  p₂ =
    r₂ •
        (p -ᵥ
          (↑((orthogonalProjection (affineSpan ℝ (Set.range s.points)) : (a : P) → ↥(affineSpan ℝ (Set.range s.points)))
                p) :
            P)) +ᵥ
      p₂o
⊢ Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points))
    (↑((s.orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range s.points))) p₁) : P)

Tactic:
obtain rfl : ↑(s.orthogonalProjectionSpan p₁) = p₁o := by
    subst hp₁
    exact s.coe_orthogonalProjection_vadd_smul_vsub_orthogonalProjection hp₁o

Premises used: Affine.Simplex.orthogonalProjectionSpan, DFunLike.coe, rfl