Theorem: List.rtake_rtake (LeanCamCombi/Mathlib/Data/List/DropRight.lean)

State before:
α : 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)
Tactic:
rw [rtake_eq_reverse_take_reverse, ← take_reverse, take_take, rtake_eq_reverse_take_reverse]
State after:
no goals