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

State before:
α : Type u_1
as : List α
stop : Nat
⊢ as.extract stop stop = []
Tactic:
unfold extract
State after:
α : Type u_1
as : List α
stop : Nat
⊢ take (stop - stop) (drop stop as) = []

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

State before:
α : Type u_1
as : List α
stop : Nat
⊢ take 0 (drop stop as) = []
Tactic:
rw [take_zero]
State after:
no goals