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

State before:
xs : List Nat
⊢ ∀ (n : Nat), n + NonTail.sum xs = Tail.sumHelper n xs
Tactic:
induction xs with
| nil =>
  intro n
  rfl
| cons y ys ih =>
  intro n
  simp [NonTail.sum, Tail.sumHelper]
  rw [← Nat.add_assoc, Nat.add_comm y n]
  exact ih (n + y)
State after:
no goals

State before:
case nil

⊢ ∀ (n : Nat), n + NonTail.sum [] = Tail.sumHelper n []
Tactic:
intro n
State after:
case nil
n : Nat
⊢ n + NonTail.sum [] = Tail.sumHelper n []

State before:
case nil
n : Nat
⊢ n + NonTail.sum [] = Tail.sumHelper n []
Tactic:
rfl
State after:
no goals

State before:
case cons
y : Nat
ys : List Nat
ih : ∀ (n : Nat), n + NonTail.sum ys = Tail.sumHelper n ys
⊢ ∀ (n : Nat), n + NonTail.sum (y :: ys) = Tail.sumHelper n (y :: ys)
Tactic:
intro n
State after:
case cons
y : Nat
ys : List Nat
ih : ∀ (n : Nat), n + NonTail.sum ys = Tail.sumHelper n ys
n : Nat
⊢ n + NonTail.sum (y :: ys) = Tail.sumHelper n (y :: ys)

State before:
case cons
y : Nat
ys : List Nat
ih : ∀ (n : Nat), n + NonTail.sum ys = Tail.sumHelper n ys
n : Nat
⊢ n + NonTail.sum (y :: ys) = Tail.sumHelper n (y :: ys)
Tactic:
simp [NonTail.sum, Tail.sumHelper]
State after:
case cons
y : Nat
ys : List Nat
ih : ∀ (n : Nat), n + NonTail.sum ys = Tail.sumHelper n ys
n : Nat
⊢ n + (y + NonTail.sum ys) = Tail.sumHelper (y + n) ys

State before:
case cons
y : Nat
ys : List Nat
ih : ∀ (n : Nat), n + NonTail.sum ys = Tail.sumHelper n ys
n : Nat
⊢ n + (y + NonTail.sum ys) = Tail.sumHelper (y + n) ys
Tactic:
rw [← Nat.add_assoc, Nat.add_comm y n]
State after:
case cons
y : Nat
ys : List Nat
ih : ∀ (n : Nat), n + NonTail.sum ys = Tail.sumHelper n ys
n : Nat
⊢ n + y + NonTail.sum ys = Tail.sumHelper (n + y) ys

State before:
case cons
y : Nat
ys : List Nat
ih : ∀ (n : Nat), n + NonTail.sum ys = Tail.sumHelper n ys
n : Nat
⊢ n + y + NonTail.sum ys = Tail.sumHelper (n + y) ys
Tactic:
exact ih (n + y)
State after:
no goals