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

State before:
α : Type u_1
x : α
xs : List α
⊢ length (xs ++ [x]) = length xs + 1
Tactic:
induction xs with
| nil => rfl
| cons _ tail ih => simp [ih]
State after:
no goals

State before:
case nil
α : Type u_1
x : α
⊢ length ([] ++ [x]) = length [] + 1
Tactic:
rfl
State after:
no goals

State before:
case cons
α : Type u_1
x head✝ : α
tail : List α
ih : length (tail ++ [x]) = length tail + 1
⊢ length (head✝ :: tail ++ [x]) = length (head✝ :: tail) + 1
Tactic:
simp [ih]
State after:
no goals