Module: Mathlib.Geometry.Euclidean.Simplex

Goal state before:
pp: case «0»
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
t : Triangle ℝ P
x✝ :
  ∠ (t.points 0) (t.points 1) (t.points 2) < π / 2 ∧
    ∠ (t.points 1) (t.points 2) (t.points 0) < π / 2 ∧ ∠ (t.points 2) (t.points 0) (t.points 1) < π / 2
h012 : ∠ (t.points 0) (t.points 1) (t.points 2) < π / 2
h120 : ∠ (t.points 1) (t.points 2) (t.points 0) < π / 2
h201 : ∠ (t.points 2) (t.points 0) (t.points 1) < π / 2
h210 : ∠ (t.points 2) (t.points 1) (t.points 0) < π / 2
h021 : ∠ (t.points 0) (t.points 2) (t.points 1) < π / 2
h102 : ∠ (t.points 1) (t.points 0) (t.points 2) < π / 2
i₂ i₃ : Fin (2 + 1)
h₂₃ : i₂ ≠ i₃
h₁₂ : (fun i ↦ i) ⟨0, ⋯⟩ ≠ i₂
h₁₃ : (fun i ↦ i) ⟨0, ⋯⟩ ≠ i₃
⊢ ∠ (t.points ((fun i ↦ i) ⟨0, ⋯⟩)) (t.points i₂) (t.points i₃) < π / 2

pp: case «1»
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
t : Triangle ℝ P
x✝ :
  ∠ (t.points 0) (t.points 1) (t.points 2) < π / 2 ∧
    ∠ (t.points 1) (t.points 2) (t.points 0) < π / 2 ∧ ∠ (t.points 2) (t.points 0) (t.points 1) < π / 2
h012 : ∠ (t.points 0) (t.points 1) (t.points 2) < π / 2
h120 : ∠ (t.points 1) (t.points 2) (t.points 0) < π / 2
h201 : ∠ (t.points 2) (t.points 0) (t.points 1) < π / 2
h210 : ∠ (t.points 2) (t.points 1) (t.points 0) < π / 2
h021 : ∠ (t.points 0) (t.points 2) (t.points 1) < π / 2
h102 : ∠ (t.points 1) (t.points 0) (t.points 2) < π / 2
i₂ i₃ : Fin (2 + 1)
h₂₃ : i₂ ≠ i₃
h₁₂ : (fun i ↦ i) ⟨1, ⋯⟩ ≠ i₂
h₁₃ : (fun i ↦ i) ⟨1, ⋯⟩ ≠ i₃
⊢ ∠ (t.points ((fun i ↦ i) ⟨1, ⋯⟩)) (t.points i₂) (t.points i₃) < π / 2

pp: case «2»
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
t : Triangle ℝ P
x✝ :
  ∠ (t.points 0) (t.points 1) (t.points 2) < π / 2 ∧
    ∠ (t.points 1) (t.points 2) (t.points 0) < π / 2 ∧ ∠ (t.points 2) (t.points 0) (t.points 1) < π / 2
h012 : ∠ (t.points 0) (t.points 1) (t.points 2) < π / 2
h120 : ∠ (t.points 1) (t.points 2) (t.points 0) < π / 2
h201 : ∠ (t.points 2) (t.points 0) (t.points 1) < π / 2
h210 : ∠ (t.points 2) (t.points 1) (t.points 0) < π / 2
h021 : ∠ (t.points 0) (t.points 2) (t.points 1) < π / 2
h102 : ∠ (t.points 1) (t.points 0) (t.points 2) < π / 2
i₂ i₃ : Fin (2 + 1)
h₂₃ : i₂ ≠ i₃
h₁₂ : (fun i ↦ i) ⟨2, ⋯⟩ ≠ i₂
h₁₃ : (fun i ↦ i) ⟨2, ⋯⟩ ≠ i₃
⊢ ∠ (t.points ((fun i ↦ i) ⟨2, ⋯⟩)) (t.points i₂) (t.points i₃) < π / 2

Tactic:
<;>

Goal state after:
case «0»
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
t : Triangle ℝ P
x✝ :
  ∠ (t.points 0) (t.points 1) (t.points 2) < π / 2 ∧
    ∠ (t.points 1) (t.points 2) (t.points 0) < π / 2 ∧ ∠ (t.points 2) (t.points 0) (t.points 1) < π / 2
h012 : ∠ (t.points 0) (t.points 1) (t.points 2) < π / 2
h120 : ∠ (t.points 1) (t.points 2) (t.points 0) < π / 2
h201 : ∠ (t.points 2) (t.points 0) (t.points 1) < π / 2
h210 : ∠ (t.points 2) (t.points 1) (t.points 0) < π / 2
h021 : ∠ (t.points 0) (t.points 2) (t.points 1) < π / 2
h102 : ∠ (t.points 1) (t.points 0) (t.points 2) < π / 2
i₂ i₃ : Fin (2 + 1)
h₂₃ : i₂ ≠ i₃
h₁₂ : (fun i ↦ i) ⟨0, ⋯⟩ ≠ i₂
h₁₃ : (fun i ↦ i) ⟨0, ⋯⟩ ≠ i₃
⊢ ∠ (t.points ((fun i ↦ i) ⟨0, ⋯⟩)) (t.points i₂) (t.points i₃) < π / 2

case «1»
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
t : Triangle ℝ P
x✝ :
  ∠ (t.points 0) (t.points 1) (t.points 2) < π / 2 ∧
    ∠ (t.points 1) (t.points 2) (t.points 0) < π / 2 ∧ ∠ (t.points 2) (t.points 0) (t.points 1) < π / 2
h012 : ∠ (t.points 0) (t.points 1) (t.points 2) < π / 2
h120 : ∠ (t.points 1) (t.points 2) (t.points 0) < π / 2
h201 : ∠ (t.points 2) (t.points 0) (t.points 1) < π / 2
h210 : ∠ (t.points 2) (t.points 1) (t.points 0) < π / 2
h021 : ∠ (t.points 0) (t.points 2) (t.points 1) < π / 2
h102 : ∠ (t.points 1) (t.points 0) (t.points 2) < π / 2
i₂ i₃ : Fin (2 + 1)
h₂₃ : i₂ ≠ i₃
h₁₂ : (fun i ↦ i) ⟨1, ⋯⟩ ≠ i₂
h₁₃ : (fun i ↦ i) ⟨1, ⋯⟩ ≠ i₃
⊢ ∠ (t.points ((fun i ↦ i) ⟨1, ⋯⟩)) (t.points i₂) (t.points i₃) < π / 2

case «2»
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
t : Triangle ℝ P
x✝ :
  ∠ (t.points 0) (t.points 1) (t.points 2) < π / 2 ∧
    ∠ (t.points 1) (t.points 2) (t.points 0) < π / 2 ∧ ∠ (t.points 2) (t.points 0) (t.points 1) < π / 2
h012 : ∠ (t.points 0) (t.points 1) (t.points 2) < π / 2
h120 : ∠ (t.points 1) (t.points 2) (t.points 0) < π / 2
h201 : ∠ (t.points 2) (t.points 0) (t.points 1) < π / 2
h210 : ∠ (t.points 2) (t.points 1) (t.points 0) < π / 2
h021 : ∠ (t.points 0) (t.points 2) (t.points 1) < π / 2
h102 : ∠ (t.points 1) (t.points 0) (t.points 2) < π / 2
i₂ i₃ : Fin (2 + 1)
h₂₃ : i₂ ≠ i₃
h₁₂ : (fun i ↦ i) ⟨2, ⋯⟩ ≠ i₂
h₁₃ : (fun i ↦ i) ⟨2, ⋯⟩ ≠ i₃
⊢ ∠ (t.points ((fun i ↦ i) ⟨2, ⋯⟩)) (t.points i₂) (t.points i₃) < π / 2