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

State before:
α : Type u_1
xs ys : List α
⊢ drop (length xs) (xs ++ ys) = ys
Tactic:
induction xs with
| nil =>
  simp only [drop, nil_append]
| cons x xs ih =>
  simp only [drop, add_eq, add_zero, append_eq]
  exact ih
State after:
no goals

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

State before:
case cons
α : Type u_1
ys : List α
x : α
xs : List α
ih : drop (length xs) (xs ++ ys) = ys
⊢ drop (length (x :: xs)) (x :: xs ++ ys) = ys
Tactic:
simp only [drop, add_eq, add_zero, append_eq]
State after:
case cons
α : Type u_1
ys : List α
x : α
xs : List α
ih : drop (length xs) (xs ++ ys) = ys
⊢ drop (length xs) (xs ++ ys) = ys

State before:
case cons
α : Type u_1
ys : List α
x : α
xs : List α
ih : drop (length xs) (xs ++ ys) = ys
⊢ drop (length xs) (xs ++ ys) = ys
Tactic:
exact ih
State after:
no goals