theorem LawfulMonadAttach.canReturn_bind_imp' {m : Type u_1 → Type u_2} {α β : Type u_1} {b : β} [Monad m] [LawfulMonad m] [MonadAttach m] [LawfulMonadAttach m] {x : m α} {f : α → m β} : MonadAttach.CanReturn (x >>= f) b → ∃ (a : α), MonadAttach.CanReturn x a ∧ MonadAttach.CanReturn (f a) b

theorem LawfulMonadAttach.eq_of_canReturn_pure {m : Type u_1 → Type u_2} {α : Type u_1} [Monad m] [MonadAttach m] [LawfulMonad m] [LawfulMonadAttach m] {a b : α} (h : MonadAttach.CanReturn (pure a) b) : a = b

theorem LawfulMonadAttach.canReturn_map_imp' {m : Type u_1 → Type u_2} {α β : Type u_1} {b : β} [Monad m] [LawfulMonad m] [MonadAttach m] [LawfulMonadAttach m] {x : m α} {f : α → β} : MonadAttach.CanReturn (f <$> x) b → ∃ (a : α), MonadAttach.CanReturn x a ∧ f a = b

theorem LawfulMonadAttach.canReturn_liftM_imp' {m : Type u_1 → Type u_2} {n : Type u_1 → Type u_3} {α : Type u_1} [Monad m] [MonadAttach m] [LawfulMonad m] [LawfulMonadAttach m] [Monad n] [MonadAttach n] [LawfulMonad n] [LawfulMonadAttach n] [MonadLiftT m n] [LawfulMonadLiftT m n] {x : m α} {a : α} : MonadAttach.CanReturn (liftM x) a → MonadAttach.CanReturn x a

theorem WeaklyLawfulMonadAttach.attach_bind_val {m : Type u_1 → Type u_2} {α β : Type u_1} [Monad m] [MonadAttach m] [LawfulMonad m] [WeaklyLawfulMonadAttach m] {x : m α} {f : α → m β} : (do let a ← MonadAttach.attach x f a.val) = x >>= f

theorem WeaklyLawfulMonadAttach.bind_attach_of_nonempty {m : Type u_1 → Type u_2} {β α : Type u_1} [Monad m] [MonadAttach m] [LawfulMonad m] [WeaklyLawfulMonadAttach m] [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

theorem MonadAttach.attach_bind_eq_pbind {m : Type u_1 → Type u_2} {α β : Type u_1} [Monad m] [MonadAttach m] {x : m α} {f : Subtype (CanReturn x) → m β} : attach x >>= f = pbind x fun (a : α) (ha : CanReturn x a) => f ⟨a, ha⟩

theorem WeaklyLawfulMonadAttach.pbind_eq_bind {m : Type u_1 → Type u_2} {α β : Type u_1} [Monad m] [MonadAttach m] [LawfulMonad m] [WeaklyLawfulMonadAttach m] {x : m α} {f : α → m β} : (MonadAttach.pbind x fun (a : α) (x : MonadAttach.CanReturn x a) => f a) = x >>= f

theorem WeaklyLawfulMonadAttach.pbind_eq_bind' {m : Type u_1 → Type u_2} {α β : Type u_1} [Monad m] [MonadAttach m] [LawfulMonad m] [WeaklyLawfulMonadAttach m] {x : m α} {f : α → m β} : (MonadAttach.pbind x fun (a : α) (x : MonadAttach.CanReturn x a) => f a) = x >>= f