import Mathlib.Tactic

theorem sum_square_identity (n : Nat) : (n + 1) ^ 2 = n ^ 2 + 2 * n * 1 + 1 ^ 2 := by ring_nf