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