case zero

⊢ fib (zero + 1) = ∑ k in Finset.range zero, fib k + 1

case succ
n : ℕ
ih : fib (n + 1) = ∑ k in Finset.range n, fib k + 1
⊢ fib (succ n + 1) = ∑ k in Finset.range (succ n), fib k + 1
n : ℕ
⊢ fib (n + 1) = ∑ k in Finset.range n, fib k + 1
induction' n with n ih
no goals
case zero

⊢ fib (zero + 1) = ∑ k in Finset.range zero, fib k + 1
simp
no goals
case succ
n : ℕ
ih : fib (n + 1) = ∑ k in Finset.range n, fib k + 1
⊢ fib (succ n + 1) = ∑ k in Finset.range (succ n), fib k + 1
calc
  fib (n + 2) = fib n + fib (n + 1) := fib_add_two
  _ = (fib n + ∑ k in Finset.range n, fib k) + 1 := by rw [ih, add_assoc]
  _ = (∑ k in Finset.range (n + 1), fib k) + 1 := by simp [Finset.range_add_one]
no goals
n : ℕ
ih : fib (n + 1) = ∑ k in Finset.range n, fib k + 1
⊢ fib n + fib (n + 1) = fib n + ∑ k in Finset.range n, fib k + 1
rw [ih, add_assoc]
no goals
n : ℕ
ih : fib (n + 1) = ∑ k in Finset.range n, fib k + 1
⊢ fib n + ∑ k in Finset.range n, fib k + 1 = ∑ k in Finset.range (n + 1), fib k + 1
simp [Finset.range_add_one]