{
  dsimp [tri_nums]
}
case a

⊢ 2 * tri_nums 0 = 0 * (0 + 1)

case a

⊢ ∀ (n : ℕ), 2 * tri_nums n = n * (n + 1) → 2 * tri_nums (n + 1) = (n + 1) * (n + 1 + 1)
case a

⊢ ∀ (n : ℕ), 2 * tri_nums n = n * (n + 1) → 2 * tri_nums (n + 1) = (n + 1) * (n + 1 + 1)