-- Mathlib/Geometry/Euclidean/Circumcenter.lean
theorem circumcenter_eq_centroid (s : Simplex ℝ P 1) :
    s.circumcenter = Finset.univ.centroid ℝ s.points

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Simplex ℝ P 1
hr : ∃ z, ∀ x ∈ Set.univ, dist (s.points x) (centroid ℝ univ s.points) = z
⊢ s.circumcenter = centroid ℝ univ s.points

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
s : Simplex ℝ P 1
r : ℝ
hr : ∀ x ∈ Set.univ, dist (s.points x) (centroid ℝ univ s.points) = r
⊢ s.circumcenter = centroid ℝ univ s.points

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
s : Simplex ℝ P 1
r : ℝ
hr : ∀ x ∈ Set.univ, dist (s.points x) (centroid ℝ univ s.points) = r
⊢ s.circumcenter = centroid ℝ univ s.points

Tactic:
exact
  (s.eq_circumcenter_of_dist_eq
      (centroid_mem_affineSpan_of_card_eq_add_one ℝ _ (Finset.card_fin 2)) fun i =>
      hr i (Set.mem_univ _)).symm

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
s : Simplex ℝ P 1
⊢ Set.univ.Pairwise fun i j =>
    dist (s.points i) (centroid ℝ univ s.points) = dist (s.points j) (centroid ℝ univ s.points)

Tactic:
intro i hi j hj hij

Result:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Simplex ℝ P 1
i : Fin 2
hi : i ∈ Set.univ
j : Fin 2
hj : j ∈ Set.univ
hij : i ≠ j
⊢ dist (s.points i) (centroid ℝ univ s.points) = dist (s.points j) (centroid ℝ univ s.points)

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Simplex ℝ P 1
hr :
  Set.univ.Pairwise fun i j =>
    dist (s.points i) (centroid ℝ univ s.points) = dist (s.points j) (centroid ℝ univ s.points)
⊢ s.circumcenter = centroid ℝ univ s.points

Tactic:
rw [Set.pairwise_eq_iff_exists_eq] at hr

Result:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Simplex ℝ P 1
hr : ∃ z, ∀ x ∈ Set.univ, dist (s.points x) (centroid ℝ univ s.points) = z
⊢ s.circumcenter = centroid ℝ univ s.points

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Simplex ℝ P 1
i : Fin 2
hi : i ∈ Set.univ
j : Fin 2
hj : j ∈ Set.univ
hij : i ≠ j
⊢ ‖1 • (s.points i -ᵥ s.points 0) - 2⁻¹ • (s.points 1 -ᵥ s.points 0)‖ =
    ‖1 • (s.points j -ᵥ s.points 0) - 2⁻¹ • (s.points 1 -ᵥ s.points 0)‖

Tactic:
fin_cases i <;> fin_cases j <;> simp [-one_smul, ← sub_smul] <;> norm_num

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
s : Simplex ℝ P 1
i : Fin 2
hi : i ∈ Set.univ
j : Fin 2
hj : j ∈ Set.univ
hij : i ≠ j
⊢ dist (s.points i) (centroid ℝ univ s.points) = dist (s.points j) (centroid ℝ univ s.points)

Tactic:
rw [Finset.centroid_pair_fin, dist_eq_norm_vsub V (s.points i),
  dist_eq_norm_vsub V (s.points j), vsub_vadd_eq_vsub_sub, vsub_vadd_eq_vsub_sub, ←
  one_smul ℝ (s.points i -ᵥ s.points 0), ← one_smul ℝ (s.points j -ᵥ s.points 0)]

Result:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Simplex ℝ P 1
i : Fin 2
hi : i ∈ Set.univ
j : Fin 2
hj : j ∈ Set.univ
hij : i ≠ j
⊢ ‖1 • (s.points i -ᵥ s.points 0) - 2⁻¹ • (s.points 1 -ᵥ s.points 0)‖ =
    ‖1 • (s.points j -ᵥ s.points 0) - 2⁻¹ • (s.points 1 -ᵥ s.points 0)‖

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Simplex ℝ P 1
⊢ s.circumcenter = centroid ℝ univ s.points

Tactic:
have hr :
  Set.Pairwise Set.univ fun i j : Fin 2 =>
    dist (s.points i) (Finset.univ.centroid ℝ s.points) =
      dist (s.points j) (Finset.univ.centroid ℝ s.points) := by
  intro i hi j hj hij
  rw [Finset.centroid_pair_fin, dist_eq_norm_vsub V (s.points i),
    dist_eq_norm_vsub V (s.points j), vsub_vadd_eq_vsub_sub, vsub_vadd_eq_vsub_sub, ←
    one_smul ℝ (s.points i -ᵥ s.points 0), ← one_smul ℝ (s.points j -ᵥ s.points 0)]
  fin_cases i <;> fin_cases j <;> simp [-one_smul, ← sub_smul] <;> norm_num

Result:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Simplex ℝ P 1
hr :
  Set.univ.Pairwise fun i j =>
    dist (s.points i) (centroid ℝ univ s.points) = dist (s.points j) (centroid ℝ univ s.points)
⊢ s.circumcenter = centroid ℝ univ s.points