calc
_ = 2 * (tri n + (n + 1)) := by rfl
_ = 2 * tri n + 2 * (n + 1) := by rw [Nat.mul_add]
_ = n * (n + 1) + 2 * (n + 1) := by rw [ih]
_ = (n + 2) * (n + 1) := by rw [Nat.add_mul]
_ = (n + 1) * (n + 1 + 1) := by rw [Nat.mul_comm]
case succ
n : Nat
ih : 2 * n.tri = n * (n + 1)
⊢ 2 * (n + 1).tri = (n + 1) * (n + 1 + 1)
no goals