Theorem: list_app_length (Katydid/Std/Lists.lean)

State before:
α : Type u_1
xs ys : List α
⊢ length (xs ++ ys) = length xs + length ys
Tactic:
cases xs with
| nil => simp only [nil_append, length_nil, zero_add]
| cons _ tailx => simp only [cons_append, length_cons, length_append, succ_add]
State after:
no goals

State before:
case nil
α : Type u_1
ys : List α
⊢ length ([] ++ ys) = length [] + length ys
Tactic:
simp only [nil_append, length_nil, zero_add]
State after:
no goals

State before:
case cons
α : Type u_1
ys : List α
head✝ : α
tailx : List α
⊢ length (head✝ :: tailx ++ ys) = length (head✝ :: tailx) + length ys
Tactic:
simp only [cons_append, length_cons, length_append, succ_add]
State after:
no goals