Theorem: non_tail_sum_eq_tail_sum (Fpil/Chap10/Sec02.lean)

State before:
⊢ NonTail.sum = Tail.sum
Tactic:
funext xs
State after:
case h
xs : List Nat
⊢ NonTail.sum xs = Tail.sum xs

State before:
case h
xs : List Nat
⊢ NonTail.sum xs = Tail.sum xs
Tactic:
simp [Tail.sum]
State after:
case h
xs : List Nat
⊢ NonTail.sum xs = Tail.sumHelper 0 xs

State before:
case h
xs : List Nat
⊢ NonTail.sum xs = Tail.sumHelper 0 xs
Tactic:
rw [← Nat.zero_add (NonTail.sum _)]
State after:
case h
xs : List Nat
⊢ 0 + NonTail.sum xs = Tail.sumHelper 0 xs

State before:
case h
xs : List Nat
⊢ 0 + NonTail.sum xs = Tail.sumHelper 0 xs
Tactic:
exact non_tail_sum_eq_helper_acumm xs 0
State after:
no goals