Theorem: List.sum_append (test/NatLE.lean)

State before:
α : Type u
inst✝ : AddMonoid α
as bs : List α
⊢ sum (as ++ bs) = sum as + sum bs
Tactic:
induction as
State after:
case nil
α : Type u
inst✝ : AddMonoid α
bs : List α
⊢ sum ([] ++ bs) = sum [] + sum bs

case cons
α : Type u
inst✝ : AddMonoid α
bs : List α
head✝ : α
tail✝ : List α
tail_ih✝ : sum (tail✝ ++ bs) = sum tail✝ + sum bs
⊢ sum (head✝ :: tail✝ ++ bs) = sum (head✝ :: tail✝) + sum bs

State before:
α : Type u
inst✝ : AddMonoid α
bs : List α
⊢ sum ([] ++ bs) = sum [] + sum bs
Tactic:
case nil =>
  change sum bs = 0 + sum bs
  rw [AddMonoid.zero_add]
State after:
no goals

State before:
α : Type u
inst✝ : AddMonoid α
bs : List α
a : α
as : List α
h_ind : sum (as ++ bs) = sum as + sum bs
⊢ sum (a :: as ++ bs) = sum (a :: as) + sum bs
Tactic:
case cons a as h_ind =>
  dsimp
  change a + sum (as++bs) = a + sum as + sum bs
  rw [h_ind]
  rw [AddSemigroup.add_assoc]
State after:
no goals

State before:
α : Type u
inst✝ : AddMonoid α
bs : List α
⊢ sum ([] ++ bs) = sum [] + sum bs
Tactic:
change sum bs = 0 + sum bs
State after:
α : Type u
inst✝ : AddMonoid α
bs : List α
⊢ sum bs = 0 + sum bs

State before:
α : Type u
inst✝ : AddMonoid α
bs : List α
⊢ sum bs = 0 + sum bs
Tactic:
rw [AddMonoid.zero_add]
State after:
no goals

State before:
α : Type u
inst✝ : AddMonoid α
bs : List α
a : α
as : List α
h_ind : sum (as ++ bs) = sum as + sum bs
⊢ sum (a :: as ++ bs) = sum (a :: as) + sum bs
Tactic:
dsimp
State after:
α : Type u
inst✝ : AddMonoid α
bs : List α
a : α
as : List α
h_ind : sum (as ++ bs) = sum as + sum bs
⊢ sum (a :: (as ++ bs)) = sum (a :: as) + sum bs

State before:
α : Type u
inst✝ : AddMonoid α
bs : List α
a : α
as : List α
h_ind : sum (as ++ bs) = sum as + sum bs
⊢ sum (a :: (as ++ bs)) = sum (a :: as) + sum bs
Tactic:
change a + sum (as++bs) = a + sum as + sum bs
State after:
α : Type u
inst✝ : AddMonoid α
bs : List α
a : α
as : List α
h_ind : sum (as ++ bs) = sum as + sum bs
⊢ a + sum (as ++ bs) = a + sum as + sum bs

State before:
α : Type u
inst✝ : AddMonoid α
bs : List α
a : α
as : List α
h_ind : sum (as ++ bs) = sum as + sum bs
⊢ a + sum (as ++ bs) = a + sum as + sum bs
Tactic:
rw [h_ind]
State after:
α : Type u
inst✝ : AddMonoid α
bs : List α
a : α
as : List α
h_ind : sum (as ++ bs) = sum as + sum bs
⊢ a + (sum as + sum bs) = a + sum as + sum bs

State before:
α : Type u
inst✝ : AddMonoid α
bs : List α
a : α
as : List α
h_ind : sum (as ++ bs) = sum as + sum bs
⊢ a + (sum as + sum bs) = a + sum as + sum bs
Tactic:
rw [AddSemigroup.add_assoc]
State after:
no goals