case cons n ns h_ind =>
  dsimp
  rw [sum_append, sum_cons, h_ind]
α : Type u
inst✝ : AddMonoid α
n : List α
ns : List (List α)
h_ind : sum (join ns) = sum (map sum ns)
⊢ sum (join (n :: ns)) = sum (map sum (n :: ns))
no goals