∀ {m : Type u_1 → Type u_2} {β α : Type u_1} [inst : Monad m] [inst_1 : MonadAttach m] [LawfulMonad m]
  [WeaklyLawfulMonadAttach m] [inst_4 : Nonempty (m β)] {x : m α} {f : Subtype (MonadAttach.CanReturn x) → m β},
  MonadAttach.attach x >>= f = do
    let a ← x
    if ha : MonadAttach.CanReturn x a then f ⟨a, ha⟩ else Classical.ofNonempty