awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Circumcenter (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
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
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
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)
⊢ p₁ = p₂ ∨ p₁ = (reflection (affineSpan ℝ (Set.range s.points)) : (a : P) → P) p₂
have h₁' : (↑((s.orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range s.points))) p₁) : P) = s.circumcenter
Tactic: have h₁' := s.orthogonalProjection_eq_circumcenter_of_dist_eq 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
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
⊢ p₁ = p₂ ∨ p₁ = (reflection (affineSpan ℝ (Set.range s.points)) : (a : P) → P) p₂
have h₂' : (↑((s.orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range s.points))) p₂) : P) = s.circumcenter
Tactic: have h₂' := s.orthogonalProjection_eq_circumcenter_of_dist_eq 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
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
⊢ p₁ = p₂ ∨ p₁ = (reflection (affineSpan ℝ (Set.range s.points)) : (a : P) → P) p₂
have 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
Tactic: rw [← affineSpan_insert_affineSpan, mem_affineSpan_insert_iff (orthogonalProjection_mem p)]
    at hp₁ hp₂
Cleared hypotheses: hp₁, hp₂, h₁, h₂, span_s, h₁', 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
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
⊢ p₁ = p₂ ∨ p₁ = (reflection (affineSpan ℝ (Set.range s.points)) : (a : P) → P) p₂
have 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
Tactic: rw [← affineSpan_insert_affineSpan, mem_affineSpan_insert_iff (orthogonalProjection_mem p)]
    at hp₁ hp₂
Cleared hypotheses: hp₁, hp₂, h₁, h₂, span_s, h₁', h₂'
-- 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
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
⊢ p₁ = p₂ ∨ p₁ = (reflection (affineSpan ℝ (Set.range s.points)) : (a : P) → P) p₂
have 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₂
Tactic: obtain ⟨r₁, p₁o, hp₁o, hp₁⟩ := hp₁
Cleared hypotheses: hp₁
-- 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
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
⊢ p₁ = p₂ ∨ p₁ = (reflection (affineSpan ℝ (Set.range s.points)) : (a : P) → P) p₂
have 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₂
Tactic: obtain ⟨r₂, p₂o, hp₂o, hp₂⟩ := hp₂
Cleared hypotheses: hp₂
-- 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
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
⊢ (↑((s.orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range s.points))) p₁) : P) = p₁o
have 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
Tactic: subst hp₁
Cleared hypotheses: p₁, h₁, h₁', hp₁
-- 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
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
⊢ p₁ = p₂ ∨ p₁ = (reflection (affineSpan ℝ (Set.range s.points)) : (a : P) → P) p₂
have hp₁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
Cleared hypotheses: p₁o, hp₁o, hp₁
-- 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
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
hp₁o₁ :
  Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points))
    (↑((s.orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range s.points))) p₁) : P)
⊢ p₁ = p₂ ∨ p₁ = (reflection (affineSpan ℝ (Set.range s.points)) : (a : P) → P) p₂
have hp₃ : p₁ =
  HVAdd.hVAdd (β := P)
    (r₁ •
      (p -ᵥ
        (↑((orthogonalProjection (affineSpan ℝ (Set.range s.points)) : (a : P) → ↥(affineSpan ℝ (Set.range s.points)))
              p) :
          P)))
    (↑((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
Cleared hypotheses: p₁o, hp₁o, hp₁
-- 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
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₁ 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
hp₁o :
  Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points))
    (↑((s.orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range s.points))) p₁) : P)
hp₁ :
  p₁ =
    HVAdd.hVAdd (β := P)
      (r₁ •
        (p -ᵥ
          (↑((orthogonalProjection (affineSpan ℝ (Set.range s.points)) : (a : P) → ↥(affineSpan ℝ (Set.range s.points)))
                p) :
            P)))
      (↑((s.orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range s.points))) p₁) : P)
⊢ p₁ = p₂ ∨ p₁ = (reflection (affineSpan ℝ (Set.range s.points)) : (a : P) → P) p₂
have hp₃ : p₁ =
  r₁ •
      (p -ᵥ
        (↑((orthogonalProjection (affineSpan ℝ (Set.range s.points)) : (a : P) → ↥(affineSpan ℝ (Set.range s.points)))
              p) :
          P)) +ᵥ
    s.circumcenter
Tactic: rw [h₁'] at hp₁
Cleared hypotheses: hp₁
-- 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
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₁ 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
hp₁o :
  Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points))
    (↑((s.orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range s.points))) p₁) : P)
hp₁ :
  p₁ =
    r₁ •
        (p -ᵥ
          (↑((orthogonalProjection (affineSpan ℝ (Set.range s.points)) : (a : P) → ↥(affineSpan ℝ (Set.range s.points)))
                p) :
            P)) +ᵥ
      s.circumcenter
⊢ (↑((s.orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range s.points))) p₂) : P) = p₂o
have 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
Tactic: subst hp₂
Cleared hypotheses: p₂, h₂, h₂', hp₂
-- 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
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₁ 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
hp₁o :
  Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points))
    (↑((s.orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range s.points))) p₁) : P)
hp₁ :
  p₁ =
    r₁ •
        (p -ᵥ
          (↑((orthogonalProjection (affineSpan ℝ (Set.range s.points)) : (a : P) → ↥(affineSpan ℝ (Set.range s.points)))
                p) :
            P)) +ᵥ
      s.circumcenter
⊢ p₁ = p₂ ∨ p₁ = (reflection (affineSpan ℝ (Set.range s.points)) : (a : P) → P) p₂
have hp₂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
Cleared hypotheses: p₂o, hp₂o, hp₂
-- 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
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₁ 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
hp₁o :
  Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points))
    (↑((s.orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range s.points))) p₁) : P)
hp₁ :
  p₁ =
    r₁ •
        (p -ᵥ
          (↑((orthogonalProjection (affineSpan ℝ (Set.range s.points)) : (a : P) → ↥(affineSpan ℝ (Set.range s.points)))
                p) :
            P)) +ᵥ
      s.circumcenter
hp₂o₁ :
  Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points))
    (↑((s.orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range s.points))) p₂) : P)
⊢ p₁ = p₂ ∨ p₁ = (reflection (affineSpan ℝ (Set.range s.points)) : (a : P) → P) p₂
have hp₃ : p₂ =
  HVAdd.hVAdd (β := P)
    (r₂ •
      (p -ᵥ
        (↑((orthogonalProjection (affineSpan ℝ (Set.range s.points)) : (a : P) → ↥(affineSpan ℝ (Set.range s.points)))
              p) :
          P)))
    (↑((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
Cleared hypotheses: p₂o, hp₂o, hp₂