Theorem: List.lastN_length_eq_self (One.lean)

State before:
α : Type u_1
l : List α
⊢ lastN (length l) l = l
Tactic:
unfold List.lastN
State after:
α : Type u_1
l : List α
⊢ drop (length l - length l) l = l

State before:
α : Type u_1
l : List α
⊢ drop (length l - length l) l = l
Tactic:
simp
State after:
no goals