-- 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₂ : ℝ
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)
hp₂ :
  p₂ =
    r₂ •
        (p -ᵥ
          (↑((orthogonalProjection (affineSpan ℝ (Set.range s.points)) : (a : P) → ↥(affineSpan ℝ (Set.range s.points)))
                p) :
            P)) +ᵥ
      s.circumcenter
h : s.points 0 ∈ span_s
hd₂ : dist p₂ s.circumcenter * dist p₂ s.circumcenter = r * r - s.circumradius * s.circumradius
hp : ¬p = (↑((s.orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range s.points))) p) : P)
hz :
  ⟪p -ᵥ (↑((orthogonalProjection span_s : (a : P) → ↥span_s) p) : P),
      p -ᵥ (↑((orthogonalProjection span_s : (a : P) → ↥span_s) p) : P)⟫ ≠
    0
hd₁ : r₁ = -r₂
neg :
  -r₂ •
        (p -ᵥ
          (↑((orthogonalProjection (affineSpan ℝ (Set.range s.points)) : (a : P) → ↥(affineSpan ℝ (Set.range s.points)))
                p) :
            P)) +ᵥ
      s.circumcenter =
    (reflection (affineSpan ℝ (Set.range s.points)) : (a : P) → P)
      (r₂ •
          (p -ᵥ
            (↑((orthogonalProjection (affineSpan ℝ (Set.range s.points)) :
                    (a : P) → ↥(affineSpan ℝ (Set.range s.points)))
                  p) :
              P)) +ᵥ
        s.circumcenter)
neg₁ :
  -r₂ •
        (p -ᵥ
          (↑((orthogonalProjection (affineSpan ℝ (Set.range s.points)) : (a : P) → ↥(affineSpan ℝ (Set.range s.points)))
                p) :
            P)) +ᵥ
      s.circumcenter =
    -(r₂ •
          (p -ᵥ
            (↑((orthogonalProjection (affineSpan ℝ (Set.range s.points)) :
                    (a : P) → ↥(affineSpan ℝ (Set.range s.points)))
                  p) :
              P))) +ᵥ
      s.circumcenter
⊢ r₁ •
        (p -ᵥ
          (↑((orthogonalProjection (affineSpan ℝ (Set.range s.points)) : (a : P) → ↥(affineSpan ℝ (Set.range s.points)))
                p) :
            P)) +ᵥ
      s.circumcenter =
    (reflection (affineSpan ℝ (Set.range s.points)) : (a : P) → P)
      (r₂ •
          (p -ᵥ
            (↑((orthogonalProjection (affineSpan ℝ (Set.range s.points)) :
                    (a : P) → ↥(affineSpan ℝ (Set.range s.points)))
                  p) :
              P)) +ᵥ
        s.circumcenter)
have neg₂ : -(r₂ •
        (p -ᵥ
          (↑((orthogonalProjection (affineSpan ℝ (Set.range s.points)) : (a : P) → ↥(affineSpan ℝ (Set.range s.points)))
                p) :
            P))) +ᵥ
    s.circumcenter =
  -(r₂ •
        (p -ᵥ
          (↑((orthogonalProjection (affineSpan ℝ (Set.range s.points)) : (a : P) → ↥(affineSpan ℝ (Set.range s.points)))
                p) :
            P))) +ᵥ
    s.circumcenter
Tactic: rw [hd₁, reflection_vadd_smul_vsub_orthogonalProjection p r₂ s.circumcenter_mem_affineSpan,
        neg_smul]