Theorem: List.isInfix_of_isInfix_lastN (One.lean)

State before:
α✝ : Type u_1
l₁ : List α✝
n : ℕ
l₂ : List α✝
h : l₁ <:+: lastN n l₂
⊢ l₁ <:+: l₂
Tactic:
rw [lastN] at h
State after:
α✝ : Type u_1
l₁ : List α✝
n : ℕ
l₂ : List α✝
h : l₁ <:+: drop (length l₂ - n) l₂
⊢ l₁ <:+: l₂

State before:
α✝ : Type u_1
l₁ : List α✝
n : ℕ
l₂ : List α✝
h : l₁ <:+: drop (length l₂ - n) l₂
⊢ l₁ <:+: l₂
Tactic:
apply List.isInfix_of_isInfix_drop h
State after:
no goals