case intro.intro
α : Type uu
β : Type vv
l₁ l₂ : List α
p : α → Bool
l l' xs : List α
hp : xs ~ l
h : xs <+ l'
⊢ List.filter p l <+~ List.filter p l'
α : Type uu
β : Type vv
l₁ l₂ : List α
p : α → Bool
l l' : List α
h : l <+~ l'
⊢ List.filter p l <+~ List.filter p l'
obtain ⟨xs, hp, h⟩ := h
no goals
case intro.intro
α : Type uu
β : Type vv
l₁ l₂ : List α
p : α → Bool
l l' xs : List α
hp : xs ~ l
h : xs <+ l'
⊢ List.filter p l <+~ List.filter p l'
exact ⟨_, hp.filter p, h.filter p⟩