dsimp
α : 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))
α : Type u
inst✝ : AddMonoid α
n : List α
ns : List (List α)
h_ind : sum (join ns) = sum (map sum ns)
⊢ sum (n ++ join ns) = sum (sum n :: map sum ns)