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

State before:
α : Type u
inst✝ : AddMonoid α
ass : List (List α)
⊢ sum (join ass) = sum (map sum ass)
Tactic:
induction ass
State after:
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✝))

State before:
α : Type u
inst✝ : AddMonoid α
⊢ sum (join []) = sum (map sum [])
Tactic:
case nil => rfl
State after:
no goals

State before:
α : 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))
Tactic:
case cons n ns h_ind =>
  dsimp
  rw [sum_append, sum_cons, h_ind]
State after:
no goals

State before:
α : Type u
inst✝ : AddMonoid α
⊢ sum (join []) = sum (map sum [])
Tactic:
rfl
State after:
no goals

State before:
α : 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))
Tactic:
dsimp
State after:
α : 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)

State before:
α : 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)
Tactic:
rw [sum_append, sum_cons, h_ind]
State after:
no goals