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

State before:
α : Type u_1
xs : List α
⊢ drop (length xs) xs = []
Tactic:
induction xs with
| nil =>
  rw [list_drop_nil]
| cons head tail ih =>
  rw [length]
  rw [drop]
  exact ih
State after:
no goals

State before:
case nil
α : Type u_1
⊢ drop (length []) [] = []
Tactic:
rw [list_drop_nil]
State after:
no goals

State before:
case cons
α : Type u_1
head : α
tail : List α
ih : drop (length tail) tail = []
⊢ drop (length (head :: tail)) (head :: tail) = []
Tactic:
rw [length]
State after:
case cons
α : Type u_1
head : α
tail : List α
ih : drop (length tail) tail = []
⊢ drop (length tail + 1) (head :: tail) = []

State before:
case cons
α : Type u_1
head : α
tail : List α
ih : drop (length tail) tail = []
⊢ drop (length tail + 1) (head :: tail) = []
Tactic:
rw [drop]
State after:
case cons
α : Type u_1
head : α
tail : List α
ih : drop (length tail) tail = []
⊢ drop (length tail) tail = []

State before:
case cons
α : Type u_1
head : α
tail : List α
ih : drop (length tail) tail = []
⊢ drop (length tail) tail = []
Tactic:
exact ih
State after:
no goals