α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
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 uu
β : Type vv
l₁✝ l₂✝ : List α
p : α → Bool
l₁ l₂ : List α
s : l₁ ~ l₂
⊢ List.filter p l₁ ~ List.filter p l₂
rw [← filterMap_eq_filter]
no goals
α : Type uu
β : Type vv
l₁✝ l₂✝ : List α
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 _