-- Mathlib/Geometry/Euclidean/Circumcenter.lean
theorem eq_or_eq_reflection_of_dist_eq {n : ℕ} {s : Simplex ℝ P n} {p p₁ p₂ : P} {r : ℝ}
    (hp₁ : p₁ ∈ affineSpan ℝ (insert p (Set.range s.points)))
    (hp₂ : p₂ ∈ affineSpan ℝ (insert p (Set.range s.points))) (h₁ : ∀ i, dist (s.points i) p₁ = r)
    (h₂ : ∀ i, dist (s.points i) p₂ = r) :
    p₁ = p₂ ∨ p₁ = reflection (affineSpan ℝ (Set.range s.points)) p₂

Proof state:
case neg
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : 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 p₁) = s.circumcenter
h₂' : ↑(s.orthogonalProjectionSpan p₂) = s.circumcenter
r₁ r₂ : ℝ
hp₁o : ↑(s.orthogonalProjectionSpan p₁) ∈ affineSpan ℝ (Set.range s.points)
hp₁ : p₁ = r₁ • (p -ᵥ ↑((orthogonalProjection (affineSpan ℝ (Set.range s.points))) p)) +ᵥ s.circumcenter
hp₂o : ↑(s.orthogonalProjectionSpan p₂) ∈ affineSpan ℝ (Set.range s.points)
hp₂ : p₂ = r₂ • (p -ᵥ ↑((orthogonalProjection (affineSpan ℝ (Set.range s.points))) 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 p)
hz : inner (p -ᵥ ↑((orthogonalProjection span_s) p)) (p -ᵥ ↑((orthogonalProjection span_s) p)) ≠ 0
⊢ r₁ • (p -ᵥ ↑((orthogonalProjection (affineSpan ℝ (Set.range s.points))) p)) +ᵥ s.circumcenter =
      r₂ • (p -ᵥ ↑((orthogonalProjection (affineSpan ℝ (Set.range s.points))) p)) +ᵥ s.circumcenter ∨
    r₁ • (p -ᵥ ↑((orthogonalProjection (affineSpan ℝ (Set.range s.points))) p)) +ᵥ s.circumcenter =
      (reflection (affineSpan ℝ (Set.range s.points)))
        (r₂ • (p -ᵥ ↑((orthogonalProjection (affineSpan ℝ (Set.range s.points))) p)) +ᵥ s.circumcenter)

Tactic:
rcases hd₁ with hd₁ | hd₁

Result:
case neg.inl
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : 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 p₁) = s.circumcenter
h₂' : ↑(s.orthogonalProjectionSpan p₂) = s.circumcenter
r₁ r₂ : ℝ
hp₁o : ↑(s.orthogonalProjectionSpan p₁) ∈ affineSpan ℝ (Set.range s.points)
hp₁ : p₁ = r₁ • (p -ᵥ ↑((orthogonalProjection (affineSpan ℝ (Set.range s.points))) p)) +ᵥ s.circumcenter
hp₂o : ↑(s.orthogonalProjectionSpan p₂) ∈ affineSpan ℝ (Set.range s.points)
hp₂ : p₂ = r₂ • (p -ᵥ ↑((orthogonalProjection (affineSpan ℝ (Set.range s.points))) 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 p)
hz : inner (p -ᵥ ↑((orthogonalProjection span_s) p)) (p -ᵥ ↑((orthogonalProjection span_s) p)) ≠ 0
hd₁ : r₁ = r₂
⊢ r₁ • (p -ᵥ ↑((orthogonalProjection (affineSpan ℝ (Set.range s.points))) p)) +ᵥ s.circumcenter =
      r₂ • (p -ᵥ ↑((orthogonalProjection (affineSpan ℝ (Set.range s.points))) p)) +ᵥ s.circumcenter ∨
    r₁ • (p -ᵥ ↑((orthogonalProjection (affineSpan ℝ (Set.range s.points))) p)) +ᵥ s.circumcenter =
      (reflection (affineSpan ℝ (Set.range s.points)))
        (r₂ • (p -ᵥ ↑((orthogonalProjection (affineSpan ℝ (Set.range s.points))) p)) +ᵥ s.circumcenter)

case neg.inr
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : 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 p₁) = s.circumcenter
h₂' : ↑(s.orthogonalProjectionSpan p₂) = s.circumcenter
r₁ r₂ : ℝ
hp₁o : ↑(s.orthogonalProjectionSpan p₁) ∈ affineSpan ℝ (Set.range s.points)
hp₁ : p₁ = r₁ • (p -ᵥ ↑((orthogonalProjection (affineSpan ℝ (Set.range s.points))) p)) +ᵥ s.circumcenter
hp₂o : ↑(s.orthogonalProjectionSpan p₂) ∈ affineSpan ℝ (Set.range s.points)
hp₂ : p₂ = r₂ • (p -ᵥ ↑((orthogonalProjection (affineSpan ℝ (Set.range s.points))) 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 p)
hz : inner (p -ᵥ ↑((orthogonalProjection span_s) p)) (p -ᵥ ↑((orthogonalProjection span_s) p)) ≠ 0
hd₁ : r₁ = -r₂
⊢ r₁ • (p -ᵥ ↑((orthogonalProjection (affineSpan ℝ (Set.range s.points))) p)) +ᵥ s.circumcenter =
      r₂ • (p -ᵥ ↑((orthogonalProjection (affineSpan ℝ (Set.range s.points))) p)) +ᵥ s.circumcenter ∨
    r₁ • (p -ᵥ ↑((orthogonalProjection (affineSpan ℝ (Set.range s.points))) p)) +ᵥ s.circumcenter =
      (reflection (affineSpan ℝ (Set.range s.points)))
        (r₂ • (p -ᵥ ↑((orthogonalProjection (affineSpan ℝ (Set.range s.points))) p)) +ᵥ s.circumcenter)

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : 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 p₁) = s.circumcenter
r₁ r₂ : ℝ
p₂o : P
hp₂o : p₂o ∈ affineSpan ℝ (Set.range s.points)
hp₁o : ↑(s.orthogonalProjectionSpan p₁) ∈ affineSpan ℝ (Set.range s.points)
hp₁ : p₁ = r₁ • (p -ᵥ ↑((orthogonalProjection (affineSpan ℝ (Set.range s.points))) p)) +ᵥ s.circumcenter
h₂ :
  ∀ (i : Fin (n + 1)),
    dist (s.points i) (r₂ • (p -ᵥ ↑((orthogonalProjection (affineSpan ℝ (Set.range s.points))) p)) +ᵥ p₂o) = r
h₂' :
  ↑(s.orthogonalProjectionSpan (r₂ • (p -ᵥ ↑((orthogonalProjection (affineSpan ℝ (Set.range s.points))) p)) +ᵥ p₂o)) =
    s.circumcenter
⊢ ↑(s.orthogonalProjectionSpan (r₂ • (p -ᵥ ↑((orthogonalProjection (affineSpan ℝ (Set.range s.points))) p)) +ᵥ p₂o)) =
    p₂o

Tactic:
exact s.coe_orthogonalProjection_vadd_smul_vsub_orthogonalProjection hp₂o

Result:
no goals