case cons a as h_ind =>
  dsimp
  change a + sum (as++bs) = a + sum as + sum bs
  rw [h_ind]
  rw [AddSemigroup.add_assoc]
α : 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
no goals