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

theorem geom_sum_pow_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