-- Mathlib/Geometry/Euclidean/Circumcenter.lean
theorem circumcenter_eq_point (s : Simplex ℝ P 0) (i : Fin 1) : s.circumcenter = s.points i

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 0
i : Fin 1
h : s.circumcenter ∈ affineSpan ℝ (Set.range s.points)
⊢ s.circumcenter = s.points i

Tactic:
have : Unique (Fin 1) := ⟨⟨0, by decide⟩, fun a => by simp only [Fin.eq_zero]⟩

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 0
i : Fin 1
h : s.circumcenter ∈ affineSpan ℝ (Set.range s.points)
this : Unique (Fin 1)
⊢ s.circumcenter = s.points i

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 0
i : Fin 1
⊢ s.circumcenter = s.points i

Tactic:
have h := s.circumcenter_mem_affineSpan

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 0
i : Fin 1
h : s.circumcenter ∈ affineSpan ℝ (Set.range s.points)
⊢ s.circumcenter = s.points i

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 0
i : Fin 1
this : Unique (Fin 1)
h : s.circumcenter = s.points default
⊢ s.circumcenter = s.points i

Tactic:
rw [h]

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 0
i : Fin 1
this : Unique (Fin 1)
h : s.circumcenter = s.points default
⊢ s.points default = s.points i

Proof state:
case e_a
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Simplex ℝ P 0
i : Fin 1
this : Unique (Fin 1)
h : s.circumcenter = s.points default
⊢ default = i

Tactic:
simp only [eq_iff_true_of_subsingleton]

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 0
i : Fin 1
h : s.circumcenter ∈ affineSpan ℝ (Set.range s.points)
a : Fin 1
⊢ a = default

Tactic:
simp only [Fin.eq_zero]

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 0
i : Fin 1
h : s.circumcenter ∈ affineSpan ℝ (Set.range s.points)
⊢ 0 < 1

Tactic:
decide

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 0
i : Fin 1
h : s.circumcenter ∈ affineSpan ℝ (Set.range s.points)
this : Unique (Fin 1)
⊢ s.circumcenter = s.points i

Tactic:
simp only [Set.range_unique, AffineSubspace.mem_affineSpan_singleton] at h

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 0
i : Fin 1
this : Unique (Fin 1)
h : s.circumcenter = s.points default
⊢ s.circumcenter = s.points i

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 0
i : Fin 1
this : Unique (Fin 1)
h : s.circumcenter = s.points default
⊢ s.points default = s.points i

Tactic:
congr

Result:
case e_a
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Simplex ℝ P 0
i : Fin 1
this : Unique (Fin 1)
h : s.circumcenter = s.points default
⊢ default = i