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

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

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

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

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