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

State before:
α : Type u_1
xs ys zs : List α
⊢ xs ++ (ys ++ zs) = xs ++ ys ++ zs
Tactic:
induction xs with
| nil => rfl
| cons head tail ih =>
  apply (congrArg (cons head))
  exact ih
State after:
no goals

State before:
case nil
α : Type u_1
ys zs : List α
⊢ [] ++ (ys ++ zs) = [] ++ ys ++ zs
Tactic:
rfl
State after:
no goals

State before:
case cons
α : Type u_1
ys zs : List α
head : α
tail : List α
ih : tail ++ (ys ++ zs) = tail ++ ys ++ zs
⊢ head :: tail ++ (ys ++ zs) = head :: tail ++ ys ++ zs
Tactic:
apply (congrArg (cons head))
State after:
case cons
α : Type u_1
ys zs : List α
head : α
tail : List α
ih : tail ++ (ys ++ zs) = tail ++ ys ++ zs
⊢ List.append tail (ys ++ zs) = List.append (List.append tail ys) zs

State before:
case cons
α : Type u_1
ys zs : List α
head : α
tail : List α
ih : tail ++ (ys ++ zs) = tail ++ ys ++ zs
⊢ List.append tail (ys ++ zs) = List.append (List.append tail ys) zs
Tactic:
exact ih
State after:
no goals