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

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