Prove that \[ 1 + 2 + 2^2 + 2^3 + ... + 2^{n-1} = 2^n - 1 \]

To do this, complete the following Lean4 theory:

import Mathlib.Tactic

open Finset Nat

variable (n : ℕ)

example :
  ∑ k in range n, 2^k = 2^n - 1 :=
by sorry

1. Proof in natural language

By induction on \(n\).

Base case: Let \(n = 0\). Then, \begin{align} \sum_{k<0} 2^k &= 0 \newline &= 2^0 - 1 \newline &= 2^n - 1 \newline \end{align}

Induction step: Let \(n = m+1\) and suppose the induction hypothesis (IH) \[ \sum_{k