theorem Std.Do.Internal.ErasesTo.map_eq {α : Type u} {m : Type u → Type v} {P : α → Prop} {x : m { b : α // P b }} {y : m α} [Monad m] [LawfulMonad m] (h : ErasesTo x y) : Subtype.val <$> x = y

An ErasesTo-witnessed refinement x of y recovers y by projecting out the property.

theorem Std.Do.Internal.ErasesTo.of_attach {m : Type u_1 → Type u_2} [Monad m] [LawfulMonad m] [MonadAttach m] [WeaklyLawfulMonadAttach m] {α : Type u_1} {x : m α} : ErasesTo (MonadAttach.attach x) x

MonadAttach.attach is bind-faithful with x.

theorem Std.Do.Internal.Ensures.pure {m : Type u → Type u_1} [Monad m] [LawfulMonad m] {α : Type u} (a : α) : Ensures (fun (x : α) => x = a) (Pure.pure a)

pure a is Ensures-witnessed at the singleton predicate (· = a).

theorem Std.Do.Internal.Ensures.weaken {m : Type u → Type v} [Monad m] [LawfulMonad m] {α : Type u} {P Q : α → Prop} {x : m α} (h : Ensures P x) (hPQ : ∀ (a : α), P a → Q a) : Ensures Q x

Weaken an Ensures-witness via predicate implication.

theorem Std.Do.Internal.Ensures.bind {m : Type u → Type v} [Monad m] [LawfulMonad m] {α β : Type u} {x : m α} {P : α → Prop} {k : α → m β} {Q : β → Prop} (h : Ensures P x) (hk : ∀ (a : α), P a → Ensures Q (k a)) : Ensures Q (x >>= k)

Compose Ensures-witnesses across a monadic bind.

theorem Std.Do.Internal.Ensures.canReturn {m : Type u_1 → Type u_2} [Monad m] [LawfulMonad m] [MonadAttach m] [WeaklyLawfulMonadAttach m] {α : Type u_1} {x : m α} : Ensures (MonadAttach.CanReturn x) x

Every value returned by x satisfies MonadAttach.CanReturn x.

theorem Std.Do.Internal.MayReturn.of_canReturn {m : Type u_1 → Type u_2} {α : Type u_1} [Monad m] [LawfulMonad m] [MonadAttach m] [LawfulMonadAttach m] {x : m α} {a : α} (h : MonadAttach.CanReturn x a) : MayReturn x a

MonadAttach.CanReturn implies MayReturn for LawfulMonadAttach instances.

theorem Std.Do.Internal.MayReturn.canReturn {m : Type u_1 → Type u_2} {α : Type u_1} [Monad m] [LawfulMonad m] [MonadAttach m] [WeaklyLawfulMonadAttach m] {x : m α} {a : α} (h : MayReturn x a) : MonadAttach.CanReturn x a

MayReturn implies MonadAttach.CanReturn for WeaklyLawfulMonadAttach instances.

theorem Std.Do.Internal.MayReturn.canReturn_iff {m : Type u_1 → Type u_2} {α : Type u_1} [Monad m] [LawfulMonad m] [MonadAttach m] [LawfulMonadAttach m] (x : m α) (a : α) : MonadAttach.CanReturn x a ↔ MayReturn x a

MayReturn is equivalent to MonadAttach.CanReturn for LawfulMonadAttach instances.

theorem Std.Do.Internal.MayReturn.canReturn_eq {m : Type u_1 → Type u_2} {α : Type u_1} [Monad m] [LawfulMonad m] [MonadAttach m] [LawfulMonadAttach m] (x : m α) : MonadAttach.CanReturn x = MayReturn x

theorem Std.Do.Internal.IsAttach.of_attach {m : Type u_1 → Type u_2} [Monad m] [LawfulMonad m] [MonadAttach m] [LawfulMonadAttach m] : IsAttach fun {x : Type u_1} (x_1 : m x) => do let x_2 ← MonadAttach.attach x_1 match x_2 with | ⟨a, h⟩ => pure ⟨a, ⋯⟩

MonadAttach.attach, retagged with MayReturn proofs, witnesses IsAttach.