case intro
α : Type u_1
p : α → Bool
l₁ xs : List α
⊢ List.filter p l₁ <:+ List.filter p (xs ++ l₁)
α : Type u_1
p : α → Bool
l₁ l₂ : List α
h : l₁ <:+ l₂
⊢ List.filter p l₁ <:+ List.filter p l₂
obtain ⟨xs, rfl⟩ := h
case intro
α : Type u_1
p : α → Bool
l₁ xs : List α
⊢ List.filter p l₁ <:+ List.filter p xs ++ List.filter p l₁
case intro
α : Type u_1
p : α → Bool
l₁ xs : List α
⊢ List.filter p l₁ <:+ List.filter p (xs ++ l₁)
rw [filter_append]
no goals
case intro
α : Type u_1
p : α → Bool
l₁ xs : List α
⊢ List.filter p l₁ <:+ List.filter p xs ++ List.filter p l₁
apply suffix_append