rw [rtake_eq_reverse_take_reverse, ← take_reverse, take_take, rtake_eq_reverse_take_reverse]
α : Type u_1
l✝ l' l₀ l₁ l₂ : List α
a b : α
m✝ n✝ n m : ℕ
l : List α
⊢ (l.rtake m).rtake n = l.rtake (min n m)
no goals