Theorem: List.lastN_ge_length (One.lean)

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

State before:
α : Type u_1
n : ℕ
l : List α
h : n ≥ length l
⊢ drop (length l - n) l = l
Tactic:
simp [h]
State after:
no goals