∀ {α : Type u_1} {β : Type u_2} {l : List α} {f : α → Option β},
  (List.filterMap f l).attach =
    List.filterMap
      (fun x =>
        match x with
        | ⟨x, h⟩ => (f x).pbind fun b m => some ⟨b, ⋯⟩)
      l.attach