induction n with
| zero => rfl
| succ n ih =>
  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]
n : Nat
⊢ 2 * n.tri = n * (n + 1)
no goals