-- Mathlib/Geometry/Euclidean/Circumcenter.lean
theorem orthogonalProjection_eq_circumcenter_of_exists_dist_eq {n : ℕ} (s : Simplex ℝ P n) {p : P}
    (hr : ∃ r, ∀ i, dist (s.points i) p = r) :
    ↑(s.orthogonalProjectionSpan p) = s.circumcenter

Proof state:
case h
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
r : ℝ
hr : ∀ (i : Fin (n + 1)), (fun x => dist x p = r) (s.points i)
⊢ ∀ (i : Fin (n + 1)), dist (s.points i) p = r

Tactic:
exact hr

Result:
no goals

Proof state:
case h
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
r : ℝ
hr : ∀ (i : Fin (n + 1)), (fun x => dist x p = r) (s.points i)
⊢ ∀ a ∈ Set.range fun i => s.points i, dist a p = r

Tactic:
refine Set.forall_mem_range.mpr ?_

Result:
case h
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
r : ℝ
hr : ∀ (i : Fin (n + 1)), (fun x => dist x p = r) (s.points i)
⊢ ∀ (i : Fin (n + 1)), dist (s.points i) p = r

Proof state:
case intro
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
r : ℝ
hr : ∀ (i : Fin (n + 1)), (fun x => dist x p = r) (s.points i)
⊢ ∃ r, ∀ a ∈ Set.range fun i => s.points i, dist a p = r

Tactic:
use r

Result:
case h
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
r : ℝ
hr : ∀ (i : Fin (n + 1)), (fun x => dist x p = r) (s.points i)
⊢ ∀ a ∈ Set.range fun i => s.points i, dist a p = r

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
hr : ∃ r, ∀ (i : Fin (n + 1)), (fun x => dist x p = r) (s.points i)
⊢ ∃ r, ∀ a ∈ Set.range fun i => s.points i, dist a p = r

Tactic:
obtain ⟨r, hr⟩ := hr

Result:
case intro
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
r : ℝ
hr : ∀ (i : Fin (n + 1)), (fun x => dist x p = r) (s.points i)
⊢ ∃ r, ∀ a ∈ Set.range fun i => s.points i, dist a p = r

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
hr✝ : ∃ r, ∀ (i : Fin (n + 1)), (fun x => dist x p = r) (s.points i)
hr : ∃ r, ∀ a ∈ Set.range fun i => s.points i, dist a p = r
⊢ ↑(s.orthogonalProjectionSpan p) = s.circumcenter

Tactic:
rw [exists_dist_eq_iff_exists_dist_orthogonalProjection_eq (subset_affineSpan ℝ _) p] at hr

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
hr✝ : ∃ r, ∀ (i : Fin (n + 1)), (fun x => dist x p = r) (s.points i)
hr :
  ∃ r,
    ∀ p₁ ∈ Set.range fun i => s.points i,
      dist p₁ ↑((EuclideanGeometry.orthogonalProjection (affineSpan ℝ (Set.range fun i => s.points i))) p) = r
⊢ ↑(s.orthogonalProjectionSpan p) = s.circumcenter

Proof state:
case intro
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
hr✝ : ∃ r, ∀ (i : Fin (n + 1)), (fun x => dist x p = r) (s.points i)
r : ℝ
hr :
  ∀ p₁ ∈ Set.range fun i => s.points i,
    dist p₁ ↑((EuclideanGeometry.orthogonalProjection (affineSpan ℝ (Set.range fun i => s.points i))) p) = r
⊢ ↑(s.orthogonalProjectionSpan p) = s.circumcenter

Tactic:
exact
  s.eq_circumcenter_of_dist_eq (orthogonalProjection_mem p) fun i => hr _ (Set.mem_range_self i)

Result:
no goals

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
hr : ∃ r, ∀ (i : Fin (n + 1)), (fun x => dist x p = r) (s.points i)
⊢ ↑(s.orthogonalProjectionSpan p) = s.circumcenter

Tactic:
have hr : ∃ (r : ℝ), ∀ (a : P),
    a ∈ Set.range (fun (i : Fin (n + 1)) => s.points i) → dist a p = r := by
  obtain ⟨r, hr⟩ := hr
  use r
  refine Set.forall_mem_range.mpr ?_
  exact hr

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
hr✝ : ∃ r, ∀ (i : Fin (n + 1)), (fun x => dist x p = r) (s.points i)
hr : ∃ r, ∀ a ∈ Set.range fun i => s.points i, dist a p = r
⊢ ↑(s.orthogonalProjectionSpan 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
hr : ∃ r, ∀ (i : Fin (n + 1)), dist (s.points i) p = r
⊢ ↑(s.orthogonalProjectionSpan p) = s.circumcenter

Tactic:
change ∃ r : ℝ, ∀ i, (fun x => dist x p = r) (s.points i) at hr

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
hr : ∃ r, ∀ (i : Fin (n + 1)), (fun x => dist x p = r) (s.points i)
⊢ ↑(s.orthogonalProjectionSpan 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
hr✝ : ∃ r, ∀ (i : Fin (n + 1)), (fun x => dist x p = r) (s.points i)
hr :
  ∃ r,
    ∀ p₁ ∈ Set.range fun i => s.points i,
      dist p₁ ↑((EuclideanGeometry.orthogonalProjection (affineSpan ℝ (Set.range fun i => s.points i))) p) = r
⊢ ↑(s.orthogonalProjectionSpan p) = s.circumcenter

Tactic:
obtain ⟨r, hr⟩ := hr

Result:
case intro
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
hr✝ : ∃ r, ∀ (i : Fin (n + 1)), (fun x => dist x p = r) (s.points i)
r : ℝ
hr :
  ∀ p₁ ∈ Set.range fun i => s.points i,
    dist p₁ ↑((EuclideanGeometry.orthogonalProjection (affineSpan ℝ (Set.range fun i => s.points i))) p) = r
⊢ ↑(s.orthogonalProjectionSpan p) = s.circumcenter