∀ {α : Type u_1} {β : Type u_2} {o : Option α} {f : α → Option β},
  (o.bind f).attach =
    o.attach.bind fun x =>
      match x with
      | ⟨x, h⟩ =>
        Option.map
          (fun x_1 =>
            match x_1 with
            | ⟨y, h'⟩ => ⟨y, ⋯⟩)
          (f x).attach