induction ass
α : Type u
inst✝ : AddMonoid α
ass : List (List α)
⊢ sum (join ass) = sum (map sum ass)
case nil
α : Type u
inst✝ : AddMonoid α
⊢ sum (join []) = sum (map sum [])

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