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

State before:
α : Type u_1
xs : List α
⊢ take (length xs) xs = xs
Tactic:
induction xs with
| nil => rfl
| cons head tail ih =>
  have h : take (length (head::tail)) (head::tail) =
      head :: (take (length tail) tail) := by
    apply list_take_cons
  rw [ih] at h
  trivial
State after:
no goals

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

State before:
case cons
α : Type u_1
head : α
tail : List α
ih : take (length tail) tail = tail
⊢ take (length (head :: tail)) (head :: tail) = head :: tail
Tactic:
have h : take (length (head::tail)) (head::tail) =
    head :: (take (length tail) tail) := by
  apply list_take_cons
State after:
case cons
α : Type u_1
head : α
tail : List α
ih : take (length tail) tail = tail
h : take (length (head :: tail)) (head :: tail) = head :: take (length tail) tail
⊢ take (length (head :: tail)) (head :: tail) = head :: tail

State before:
case cons
α : Type u_1
head : α
tail : List α
ih : take (length tail) tail = tail
h : take (length (head :: tail)) (head :: tail) = head :: take (length tail) tail
⊢ take (length (head :: tail)) (head :: tail) = head :: tail
Tactic:
rw [ih] at h
State after:
case cons
α : Type u_1
head : α
tail : List α
ih : take (length tail) tail = tail
h : take (length (head :: tail)) (head :: tail) = head :: tail
⊢ take (length (head :: tail)) (head :: tail) = head :: tail

State before:
case cons
α : Type u_1
head : α
tail : List α
ih : take (length tail) tail = tail
h : take (length (head :: tail)) (head :: tail) = head :: tail
⊢ take (length (head :: tail)) (head :: tail) = head :: tail
Tactic:
trivial
State after:
no goals

State before:
α : Type u_1
head : α
tail : List α
ih : take (length tail) tail = tail
⊢ take (length (head :: tail)) (head :: tail) = head :: take (length tail) tail
Tactic:
apply list_take_cons
State after:
no goals