import Mathlib.Algebra.BigOperators.Intervals
import Mathlib.Tactic.Ring

theorem sum_odd_sq (n : Nat) : Finset.sum (Finset.range n) (fun i => 2 * i + 1) = n * n := by
  induction n with
  | zero => simp
  | succ n ih =>
    rw [Finset.sum_range_succ]
    ring_nf
    linarith