-- Module: Mathlib.Geometry.Euclidean.Simplex
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
t : Triangle ℝ P
h :
  ∠ (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₃ : Fin (HAdd.hAdd (α := ℕ) 2 1)
h₁₃ : (fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨2, ⋯⟩ ≠ i₃
h₂₃ : (fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨1, ⋯⟩ ≠ i₃
h₁₂ :
  Ne (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨2, ⋯⟩)
    ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨1, ⋯⟩)
2 :
  ∀
    (h₁₃ :
      Ne (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨2, ⋯⟩)
        ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨0, ⋯⟩))
    (h₂₃ :
      Ne (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨1, ⋯⟩)
        ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨0, ⋯⟩)),
    ∠ (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))))
        (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))))
        (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))) <
      π / 2
h_1 :
  ∀
    (h₁₃ :
      Ne (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨2, ⋯⟩)
        ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨1, ⋯⟩))
    (h₂₃ :
      Ne (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨1, ⋯⟩)
        ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨1, ⋯⟩)),
    ∠ (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))))
        (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))))
        (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))) <
      π / 2
h_2 :
  ∀
    (h₁₃ :
      Ne (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨2, ⋯⟩)
        ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨2, ⋯⟩))
    (h₂₃ :
      Ne (α := Fin (HAdd.hAdd (α := ℕ) 2 1)) ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨1, ⋯⟩)
        ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) ⟨2, ⋯⟩)),
    ∠ (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))))
        (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))))
        (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))) <
      π / 2
⊢ ∠ (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1))))
      (t.points ((fun (i : Fin (HAdd.hAdd (α := ℕ) 2 1)) ↦ i) (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 2 1)))) (t.points i₃) <
    π / 2

Tactic:
fin_cases i₃