dsimp [tri_nums]
case a
n : ℕ
h : 2 * tri_nums n = n * (n + 1)
⊢ 2 * tri_nums (n + 1) = (n + 1) * (n + 1 + 1)
case a
n : ℕ
h : 2 * tri_nums n = n * (n + 1)
⊢ 2 * (tri_nums (n + 0) + (n + 0 + 1)) = (n + 1) * (n + 1 + 1)