rw [hl.eq_rtake]
α : Type u_1
l l' l₀ l₁ l₂ : List α
a b : α
m n : ℕ
hl : l <:+ l'
h : l.length ≤ n
⊢ l <:+ l'.rtake n
α : Type u_1
l l' l₀ l₁ l₂ : List α
a b : α
m n : ℕ
hl : l <:+ l'
h : l.length ≤ n
⊢ l'.rtake l.length <:+ l'.rtake n