-- 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:
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₂ : ℝ
p₂o : P
hp₂o : p₂o ∈ affineSpan ℝ (Set.range s.points)
hp₂ : p₂ = r₂ • (p -ᵥ ↑((orthogonalProjection (affineSpan ℝ (Set.range s.points))) p)) +ᵥ p₂o
hp₁o : ↑(s.orthogonalProjectionSpan p₁) ∈ affineSpan ℝ (Set.range s.points)
hp₁ : p₁ = r₁ • (p -ᵥ ↑((orthogonalProjection (affineSpan ℝ (Set.range s.points))) p)) +ᵥ s.circumcenter
⊢ ↑(s.orthogonalProjectionSpan p₂) = p₂o

Tactic:
subst hp₂

Result:
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

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₁ *
      inner (p -ᵥ ↑((orthogonalProjection (affineSpan ℝ (Set.range s.points))) p))
        (p -ᵥ ↑((orthogonalProjection (affineSpan ℝ (Set.range s.points))) p)) =
    r₂ * r₂ *
      inner (p -ᵥ ↑((orthogonalProjection (affineSpan ℝ (Set.range s.points))) p))
        (p -ᵥ ↑((orthogonalProjection (affineSpan ℝ (Set.range s.points))) p))
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
⊢ p₁ = p₂ ∨ p₁ = (reflection (affineSpan ℝ (Set.range s.points))) p₂

Tactic:
rw [mul_left_inj' hz, mul_self_eq_mul_self_iff] at hd₁

Result:
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
⊢ p₁ = p₂ ∨ p₁ = (reflection (affineSpan ℝ (Set.range s.points))) p₂