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

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

State before:
case nil
α : Type u_1
⊢ [] ++ [] = []
Tactic:
rfl
State after:
no goals

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

State before:
case cons
α : Type u_1
head : α
tail : List α
ih : tail ++ [] = tail
⊢ List.append tail [] = tail
Tactic:
assumption
State after:
no goals