Theorem: List.take_all (GMLInit/Data/List/Basic.lean)

State before:
α : Type u_1
as : List α
⊢ take as.length as = as
Tactic:
induction as with
| nil => rfl
| cons a as ih =>
  rw [length_cons]
  rw [take_cons_succ]
  rw [ih]
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
a : α
as : List α
ih : take as.length as = as
⊢ take (a :: as).length (a :: as) = a :: as
Tactic:
rw [length_cons]
State after:
case cons
α : Type u_1
a : α
as : List α
ih : take as.length as = as
⊢ take as.length.succ (a :: as) = a :: as

State before:
case cons
α : Type u_1
a : α
as : List α
ih : take as.length as = as
⊢ take as.length.succ (a :: as) = a :: as
Tactic:
rw [take_cons_succ]
State after:
case cons
α : Type u_1
a : α
as : List α
ih : take as.length as = as
⊢ a :: take as.length as = a :: as

State before:
case cons
α : Type u_1
a : α
as : List α
ih : take as.length as = as
⊢ a :: take as.length as = a :: as
Tactic:
rw [ih]
State after:
no goals