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

State before:
α : Type u_1
l l' l₀ l₁ l₂ : List α
a b : α
m n : ℕ
hl : l <:+ l'
h : l.length ≤ n
⊢ l <:+ l'.rtake n
Tactic:
rw [hl.eq_rtake]
State after:
α : 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

State before:
α : 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
Tactic:
exact rtake_suffix_rtake h
State after:
no goals