Theorem: List.extract_all (Extra/List.lean)

State before:
α : Type u_1
as : List α
⊢ as.extract 0 as.length = as
Tactic:
unfold extract
State after:
α : Type u_1
as : List α
⊢ take (as.length - 0) (drop 0 as) = as

State before:
α : Type u_1
as : List α
⊢ take (as.length - 0) (drop 0 as) = as
Tactic:
rw [Nat.sub_zero]
State after:
α : Type u_1
as : List α
⊢ take as.length (drop 0 as) = as

State before:
α : Type u_1
as : List α
⊢ take as.length (drop 0 as) = as
Tactic:
rw [List.drop]
State after:
α : Type u_1
as : List α
⊢ take as.length as = as

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