α : Type u_1
p : α → Bool
l₁ l₂ : List α
s : l₁ <+ l₂
⊢ List.filterMap (Option.guard fun x => p x = true) l₁ <+ List.filterMap (Option.guard fun x => p x = true) l₂
α : Type u_1
p : α → Bool
l₁ l₂ : List α
s : l₁ <+ l₂
⊢ List.filter p l₁ <+ List.filter p l₂
rw [← filterMap_eq_filter]
no goals
α : Type u_1
p : α → Bool
l₁ l₂ : List α
s : l₁ <+ l₂
⊢ List.filterMap (Option.guard fun x => p x = true) l₁ <+ List.filterMap (Option.guard fun x => p x = true) l₂
apply s.filterMap