Module: Mathlib.Geometry.Euclidean.Circumcenter

Goal state before:
pp: case «0».«0»
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
hi hj : (fun i ↦ i) ⟨0, ⋯⟩ ∈ Set.univ
hij : (fun i ↦ i) ⟨0, ⋯⟩ ≠ (fun i ↦ i) ⟨0, ⋯⟩
⊢ ‖1 • (s.points ((fun i ↦ i) ⟨0, ⋯⟩) -ᵥ s.points 0) - 2⁻¹ • (s.points 1 -ᵥ s.points 0)‖ =
    ‖1 • (s.points ((fun i ↦ i) ⟨0, ⋯⟩) -ᵥ s.points 0) - 2⁻¹ • (s.points 1 -ᵥ s.points 0)‖

pp: case «0».«1»
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
hi : (fun i ↦ i) ⟨0, ⋯⟩ ∈ Set.univ
hj : (fun i ↦ i) ⟨1, ⋯⟩ ∈ Set.univ
hij : (fun i ↦ i) ⟨0, ⋯⟩ ≠ (fun i ↦ i) ⟨1, ⋯⟩
⊢ ‖1 • (s.points ((fun i ↦ i) ⟨0, ⋯⟩) -ᵥ s.points 0) - 2⁻¹ • (s.points 1 -ᵥ s.points 0)‖ =
    ‖1 • (s.points ((fun i ↦ i) ⟨1, ⋯⟩) -ᵥ s.points 0) - 2⁻¹ • (s.points 1 -ᵥ s.points 0)‖

pp: case «1».«0»
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
hi : (fun i ↦ i) ⟨1, ⋯⟩ ∈ Set.univ
hj : (fun i ↦ i) ⟨0, ⋯⟩ ∈ Set.univ
hij : (fun i ↦ i) ⟨1, ⋯⟩ ≠ (fun i ↦ i) ⟨0, ⋯⟩
⊢ ‖1 • (s.points ((fun i ↦ i) ⟨1, ⋯⟩) -ᵥ s.points 0) - 2⁻¹ • (s.points 1 -ᵥ s.points 0)‖ =
    ‖1 • (s.points ((fun i ↦ i) ⟨0, ⋯⟩) -ᵥ s.points 0) - 2⁻¹ • (s.points 1 -ᵥ s.points 0)‖

pp: case «1».«1»
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
hi hj : (fun i ↦ i) ⟨1, ⋯⟩ ∈ Set.univ
hij : (fun i ↦ i) ⟨1, ⋯⟩ ≠ (fun i ↦ i) ⟨1, ⋯⟩
⊢ ‖1 • (s.points ((fun i ↦ i) ⟨1, ⋯⟩) -ᵥ s.points 0) - 2⁻¹ • (s.points 1 -ᵥ s.points 0)‖ =
    ‖1 • (s.points ((fun i ↦ i) ⟨1, ⋯⟩) -ᵥ s.points 0) - 2⁻¹ • (s.points 1 -ᵥ s.points 0)‖

Tactic:
<;>

Goal state after:
case «0».«0»
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
hi hj : (fun i ↦ i) ⟨0, ⋯⟩ ∈ Set.univ
hij : (fun i ↦ i) ⟨0, ⋯⟩ ≠ (fun i ↦ i) ⟨0, ⋯⟩
⊢ ‖1 • (s.points ((fun i ↦ i) ⟨0, ⋯⟩) -ᵥ s.points 0) - 2⁻¹ • (s.points 1 -ᵥ s.points 0)‖ =
    ‖1 • (s.points ((fun i ↦ i) ⟨0, ⋯⟩) -ᵥ s.points 0) - 2⁻¹ • (s.points 1 -ᵥ s.points 0)‖

case «0».«1»
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
hi : (fun i ↦ i) ⟨0, ⋯⟩ ∈ Set.univ
hj : (fun i ↦ i) ⟨1, ⋯⟩ ∈ Set.univ
hij : (fun i ↦ i) ⟨0, ⋯⟩ ≠ (fun i ↦ i) ⟨1, ⋯⟩
⊢ ‖1 • (s.points ((fun i ↦ i) ⟨0, ⋯⟩) -ᵥ s.points 0) - 2⁻¹ • (s.points 1 -ᵥ s.points 0)‖ =
    ‖1 • (s.points ((fun i ↦ i) ⟨1, ⋯⟩) -ᵥ s.points 0) - 2⁻¹ • (s.points 1 -ᵥ s.points 0)‖

case «1».«0»
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
hi : (fun i ↦ i) ⟨1, ⋯⟩ ∈ Set.univ
hj : (fun i ↦ i) ⟨0, ⋯⟩ ∈ Set.univ
hij : (fun i ↦ i) ⟨1, ⋯⟩ ≠ (fun i ↦ i) ⟨0, ⋯⟩
⊢ ‖1 • (s.points ((fun i ↦ i) ⟨1, ⋯⟩) -ᵥ s.points 0) - 2⁻¹ • (s.points 1 -ᵥ s.points 0)‖ =
    ‖1 • (s.points ((fun i ↦ i) ⟨0, ⋯⟩) -ᵥ s.points 0) - 2⁻¹ • (s.points 1 -ᵥ s.points 0)‖

case «1».«1»
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
hi hj : (fun i ↦ i) ⟨1, ⋯⟩ ∈ Set.univ
hij : (fun i ↦ i) ⟨1, ⋯⟩ ≠ (fun i ↦ i) ⟨1, ⋯⟩
⊢ ‖1 • (s.points ((fun i ↦ i) ⟨1, ⋯⟩) -ᵥ s.points 0) - 2⁻¹ • (s.points 1 -ᵥ s.points 0)‖ =
    ‖1 • (s.points ((fun i ↦ i) ⟨1, ⋯⟩) -ᵥ s.points 0) - 2⁻¹ • (s.points 1 -ᵥ s.points 0)‖