-- 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₁ : r₁ = r₂ ∨ r₁ = -r₂
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
⊢ 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 : ∀ (hd₁ : r₁ = r₂),
  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)
Tactic: rcases hd₁ with hd₁ | hd₁
Cleared hypotheses: hd₁