case intro
α : Type u_1
p : α → Bool
l₁ xs : List α
⊢ List.filter p l₁ <+: List.filter p (l₁ ++ xs)
α : 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 l₁ ++ List.filter p xs
case intro
α : Type u_1
p : α → Bool
l₁ xs : List α
⊢ List.filter p l₁ <+: List.filter p (l₁ ++ xs)
rw [filter_append]
no goals
case intro
α : Type u_1
p : α → Bool
l₁ xs : List α
⊢ List.filter p l₁ <+: List.filter p l₁ ++ List.filter p xs
apply prefix_append