Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓to navigate, Ctrl+🖱️to focus. On Mac, use Cmdinstead of Ctrl.
```/-
Authors: Mario Carneiro
-/
import Std.Logic

/--
An alternative constructor for `LawfulMonad` which has more
defaultable fields in the common case.
-/
theorem LawfulMonad.mk': ∀ (m : Type u → Type v) [inst : Monad m],
(∀ {α : Type u} (x : m α), id <\$> x = x) →
(∀ {α β : Type u} (x : α) (f : α → m β), pure x >>= f = f x) →
(∀ {α β γ : Type u} (x : m α) (f : α → m β) (g : β → m γ), x >>= f >>= g = x >>= fun x => f x >>= g) →
autoParam (∀ {α β : Type u} (x : α) (y : m β), Functor.mapConst x y = Function.const β x <\$> y) _auto✝ →
autoParam
(∀ {α β : Type u} (x : m α) (y : m β),
(SeqLeft.seqLeft x fun x => y) = do
let a ← x
let _ ← y
pure a)
_auto✝¹ →
autoParam
(∀ {α β : Type u} (x : m α) (y : m β),
(SeqRight.seqRight x fun x => y) = do
let _ ← x
y)
_auto✝² →
autoParam
(∀ {α β : Type u} (f : α → β) (x : m α),
(do
let y ← x
pure (f y)) =                       f <\$> x)
_auto✝³ →
autoParam
(∀ {α β : Type u} (f : m (α → β)) (x : m α),
(do
let x_1 ← f
x_1 <\$> x) =                         Seq.seq f fun x_1 => x)
_auto✝⁴ →
LawfulMonad mLawfulMonad.mk' (m: Type u → Type vm : Type u: Type (u+1)Type u → Type v: Type (v+1)Type v) [Monad: (Type ?u.7 → Type ?u.6) → Type (max(?u.7+1)?u.6)Monad m: Type u → Type vm]
(id_map: ∀ {α : Type u} (x : m α), id <\$> x = xid_map : ∀ {α: ?m.14α} (x: m αx : m: Type u → Type vm α: ?m.14α), id: {α : Sort ?u.26} → α → αid <\$> x: m αx = x: m αx)
(pure_bind: ∀ {α : Sort ?u.71} {β : Type u} (x : α) (f : α → m β), pure x >>= f = f xpure_bind : ∀ {α: ?m.66α β: ?m.69β} (x: αx : α: ?m.66α) (f: α → m βf : α: ?m.66α → m: Type u → Type vm β: ?m.69β), pure: {f : Type ?u.86 → Type ?u.85} → [self : Pure f] → {α : Type ?u.86} → α → f αpure x: αx >>= f: α → m βf = f: α → m βf x: αx)
(bind_assoc: ∀ {α β γ : Type u} (x : m α) (f : α → m β) (g : β → m γ), x >>= f >>= g = x >>= fun x => f x >>= gbind_assoc : ∀ {α: ?m.179α β: ?m.182β γ: ?m.185γ} (x: m αx : m: Type u → Type vm α: ?m.179α) (f: α → m βf : α: ?m.179α → m: Type u → Type vm β: ?m.182β) (g: β → m γg : β: ?m.182β → m: Type u → Type vm γ: ?m.185γ),
x: m αx >>= f: α → m βf >>= g: β → m γg = x: m αx >>= fun x: ?m.255x => f: α → m βf x: ?m.255x >>= g: β → m γg)
(map_const: autoParam (∀ {α β : Type u} (x : α) (y : m β), Functor.mapConst x y = Function.const β x <\$> y) _auto✝map_const : ∀ {α: ?m.372α β: ?m.375β} (x: αx : α: ?m.372α) (y: m βy : m: Type u → Type vm β: ?m.375β),
Functor.mapConst: {f : Type ?u.384 → Type ?u.383} → [self : Functor f] → {α β : Type ?u.384} → α → f β → f αFunctor.mapConst x: αx y: m βy = Function.const: {α : Sort ?u.397} → (β : Sort ?u.396) → α → β → αFunction.const β: ?m.375β x: αx <\$> y: m βy := by intros; rfl)
(seqLeft_eq: autoParam
(∀ {α β : Type u} (x : m α) (y : m β),
(SeqLeft.seqLeft x fun x => y) = do
let a ← x
let _ ← y
pure a)
_auto✝seqLeft_eq : ∀ {α: ?m.481α β: ?m.484β} (x: m αx : m: Type u → Type vm α: ?m.481α) (y: m βy : m: Type u → Type vm β: ?m.484β),
x: m αx <* y: m βy = (x: m αx >>= fun a: ?m.531a => y: m βy >>= fun _: ?m.568_ => pure: {f : Type ?u.571 → Type ?u.570} → [self : Pure f] → {α : Type ?u.571} → α → f αpure a: ?m.531a) := by intros; rfl)
(seqRight_eq: autoParam
(∀ {α β : Type u} (x : m α) (y : m β),
(SeqRight.seqRight x fun x => y) = do
let _ ← x
y)
_auto✝seqRight_eq : ∀ {α: ?m.675α β: ?m.678β} (x: m αx : m: Type u → Type vm α: ?m.675α) (y: m βy : m: Type u → Type vm β: ?m.678β), x: m αx *> y: m βy = (x: m αx >>= fun _: ?m.725_ => y: m βy) := by intros; rfl)
(bind_pure_comp: autoParam
(∀ {α β : Type u} (f : α → β) (x : m α),
(do
let y ← x
pure (f y)) =       f <\$> x)
_auto✝bind_pure_comp : ∀ {α: ?m.805α β: ?m.808β} (f: α → βf : α: ?m.805α → β: ?m.808β) (x: m αx : m: Type u → Type vm α: ?m.805α),
x: m αx >>= (fun y: ?m.826y => pure: {f : Type ?u.829 → Type ?u.828} → [self : Pure f] → {α : Type ?u.829} → α → f αpure (f: α → βf y: ?m.826y)) = f: α → βf <\$> x: m αx := by intros; rfl)
(bind_map: autoParam
(∀ {α β : Type u} (f : m (α → β)) (x : m α),
(do
let x_1 ← f
x_1 <\$> x) =       Seq.seq f fun x_1 => x)
_auto✝bind_map : ∀ {α: ?m.942α β: ?m.945β} (f: m (α → β)f : m: Type u → Type vm (α: ?m.942α → β: ?m.945β)) (x: m αx : m: Type u → Type vm α: ?m.942α), f: m (α → β)f >>= (. <\$> x: m αx) = f: m (α → β)f <*> x: m αx := by intros; rfl)
: LawfulMonad: (m : Type ?u.1033 → Type ?u.1032) → [inst : Monad m] → PropLawfulMonad m: Type u → Type vm :=
have map_pure: ∀ {α β : Type u} (g : α → β) (x : α), g <\$> pure x = pure (g x)map_pure {α: ?m.1071α β: ?m.1074β} (g: α → βg : α: ?m.1071α → β: ?m.1074β) (x: αx : α: ?m.1071α) : g: α → βg <\$> (pure: {f : Type ?u.1095 → Type ?u.1094} → [self : Pure f] → {α : Type ?u.1095} → α → f αpure x: αx : m: Type u → Type vm α: ?m.1071α) = pure: {f : Type ?u.1153 → Type ?u.1152} → [self : Pure f] → {α : Type ?u.1153} → α → f αpure (g: α → βg x: αx) := byGoals accomplished! 🐙
m: Type u → Type vinst✝: Monad mid_map: ∀ {α : Type u} (x : m α), id <\$> x = xpure_bind: ∀ {α β : Type u} (x : α) (f : α → m β), pure x >>= f = f xbind_assoc: ∀ {α β γ : Type u} (x : m α) (f : α → m β) (g : β → m γ), x >>= f >>= g = x >>= fun x => f x >>= gmap_const: autoParam (∀ {α β : Type u} (x : α) (y : m β), Functor.mapConst x y = Function.const β x <\$> y) _auto✝seqLeft_eq: autoParam
(∀ {α β : Type u} (x : m α) (y : m β),
(SeqLeft.seqLeft x fun x => y) = do
let a ← x
let _ ← y
pure a)
_auto✝seqRight_eq: autoParam
(∀ {α β : Type u} (x : m α) (y : m β),
(SeqRight.seqRight x fun x => y) = do
let _ ← x
y)
_auto✝bind_pure_comp: autoParam
(∀ {α β : Type u} (f : α → β) (x : m α),
(do
let y ← x
pure (f y)) =       f <\$> x)
_auto✝bind_map: autoParam
(∀ {α β : Type u} (f : m (α → β)) (x : m α),
(do
let x_1 ← f
x_1 <\$> x) =       Seq.seq f fun x_1 => x)
_auto✝α, β: Type ug: α → βx: αg <\$> pure x = pure (g x)rw [m: Type u → Type vinst✝: Monad mid_map: ∀ {α : Type u} (x : m α), id <\$> x = xpure_bind: ∀ {α β : Type u} (x : α) (f : α → m β), pure x >>= f = f xbind_assoc: ∀ {α β γ : Type u} (x : m α) (f : α → m β) (g : β → m γ), x >>= f >>= g = x >>= fun x => f x >>= gmap_const: autoParam (∀ {α β : Type u} (x : α) (y : m β), Functor.mapConst x y = Function.const β x <\$> y) _auto✝seqLeft_eq: autoParam
(∀ {α β : Type u} (x : m α) (y : m β),
(SeqLeft.seqLeft x fun x => y) = do
let a ← x
let _ ← y
pure a)
_auto✝seqRight_eq: autoParam
(∀ {α β : Type u} (x : m α) (y : m β),
(SeqRight.seqRight x fun x => y) = do
let _ ← x
y)
_auto✝bind_pure_comp: autoParam
(∀ {α β : Type u} (f : α → β) (x : m α),
(do
let y ← x
pure (f y)) =       f <\$> x)
_auto✝bind_map: autoParam
(∀ {α β : Type u} (f : m (α → β)) (x : m α),
(do
let x_1 ← f
x_1 <\$> x) =       Seq.seq f fun x_1 => x)
_auto✝α, β: Type ug: α → βx: αg <\$> pure x = pure (g x)← bind_pure_comp: autoParam
(∀ {α β : Type u} (f : α → β) (x : m α),
(do
let y ← x
pure (f y)) =       f <\$> x)
_auto✝bind_pure_compm: Type u → Type vinst✝: Monad mid_map: ∀ {α : Type u} (x : m α), id <\$> x = xpure_bind: ∀ {α β : Type u} (x : α) (f : α → m β), pure x >>= f = f xbind_assoc: ∀ {α β γ : Type u} (x : m α) (f : α → m β) (g : β → m γ), x >>= f >>= g = x >>= fun x => f x >>= gmap_const: autoParam (∀ {α β : Type u} (x : α) (y : m β), Functor.mapConst x y = Function.const β x <\$> y) _auto✝seqLeft_eq: autoParam
(∀ {α β : Type u} (x : m α) (y : m β),
(SeqLeft.seqLeft x fun x => y) = do
let a ← x
let _ ← y
pure a)
_auto✝seqRight_eq: autoParam
(∀ {α β : Type u} (x : m α) (y : m β),
(SeqRight.seqRight x fun x => y) = do
let _ ← x
y)
_auto✝bind_pure_comp: autoParam
(∀ {α β : Type u} (f : α → β) (x : m α),
(do
let y ← x
pure (f y)) =       f <\$> x)
_auto✝bind_map: autoParam
(∀ {α β : Type u} (f : m (α → β)) (x : m α),
(do
let x_1 ← f
x_1 <\$> x) =       Seq.seq f fun x_1 => x)
_auto✝α, β: Type ug: α → βx: α(do
let y ← pure x
pure (g y)) =   pure (g x)]m: Type u → Type vinst✝: Monad mid_map: ∀ {α : Type u} (x : m α), id <\$> x = xpure_bind: ∀ {α β : Type u} (x : α) (f : α → m β), pure x >>= f = f xbind_assoc: ∀ {α β γ : Type u} (x : m α) (f : α → m β) (g : β → m γ), x >>= f >>= g = x >>= fun x => f x >>= gmap_const: autoParam (∀ {α β : Type u} (x : α) (y : m β), Functor.mapConst x y = Function.const β x <\$> y) _auto✝seqLeft_eq: autoParam
(∀ {α β : Type u} (x : m α) (y : m β),
(SeqLeft.seqLeft x fun x => y) = do
let a ← x
let _ ← y
pure a)
_auto✝seqRight_eq: autoParam
(∀ {α β : Type u} (x : m α) (y : m β),
(SeqRight.seqRight x fun x => y) = do
let _ ← x
y)
_auto✝bind_pure_comp: autoParam
(∀ {α β : Type u} (f : α → β) (x : m α),
(do
let y ← x
pure (f y)) =       f <\$> x)
_auto✝bind_map: autoParam
(∀ {α β : Type u} (f : m (α → β)) (x : m α),
(do
let x_1 ← f
x_1 <\$> x) =       Seq.seq f fun x_1 => x)
_auto✝α, β: Type ug: α → βx: α(do
let y ← pure x
pure (g y)) =   pure (g x);m: Type u → Type vinst✝: Monad mid_map: ∀ {α : Type u} (x : m α), id <\$> x = xpure_bind: ∀ {α β : Type u} (x : α) (f : α → m β), pure x >>= f = f xbind_assoc: ∀ {α β γ : Type u} (x : m α) (f : α → m β) (g : β → m γ), x >>= f >>= g = x >>= fun x => f x >>= gmap_const: autoParam (∀ {α β : Type u} (x : α) (y : m β), Functor.mapConst x y = Function.const β x <\$> y) _auto✝seqLeft_eq: autoParam
(∀ {α β : Type u} (x : m α) (y : m β),
(SeqLeft.seqLeft x fun x => y) = do
let a ← x
let _ ← y
pure a)
_auto✝seqRight_eq: autoParam
(∀ {α β : Type u} (x : m α) (y : m β),
(SeqRight.seqRight x fun x => y) = do
let _ ← x
y)
_auto✝bind_pure_comp: autoParam
(∀ {α β : Type u} (f : α → β) (x : m α),
(do
let y ← x
pure (f y)) =       f <\$> x)
_auto✝bind_map: autoParam
(∀ {α β : Type u} (f : m (α → β)) (x : m α),
(do
let x_1 ← f
x_1 <\$> x) =       Seq.seq f fun x_1 => x)
_auto✝α, β: Type ug: α → βx: α(do
let y ← pure x
pure (g y)) =   pure (g x) m: Type u → Type vinst✝: Monad mid_map: ∀ {α : Type u} (x : m α), id <\$> x = xpure_bind: ∀ {α β : Type u} (x : α) (f : α → m β), pure x >>= f = f xbind_assoc: ∀ {α β γ : Type u} (x : m α) (f : α → m β) (g : β → m γ), x >>= f >>= g = x >>= fun x => f x >>= gmap_const: autoParam (∀ {α β : Type u} (x : α) (y : m β), Functor.mapConst x y = Function.const β x <\$> y) _auto✝seqLeft_eq: autoParam
(∀ {α β : Type u} (x : m α) (y : m β),
(SeqLeft.seqLeft x fun x => y) = do
let a ← x
let _ ← y
pure a)
_auto✝seqRight_eq: autoParam
(∀ {α β : Type u} (x : m α) (y : m β),
(SeqRight.seqRight x fun x => y) = do
let _ ← x
y)
_auto✝bind_pure_comp: autoParam
(∀ {α β : Type u} (f : α → β) (x : m α),
(do
let y ← x
pure (f y)) =       f <\$> x)
_auto✝bind_map: autoParam
(∀ {α β : Type u} (f : m (α → β)) (x : m α),
(do
let x_1 ← f
x_1 <\$> x) =       Seq.seq f fun x_1 => x)
_auto✝α, β: Type ug: α → βx: αg <\$> pure x = pure (g x)simp [pure_bind: ∀ {α β : Type u} (x : α) (f : α → m β), pure x >>= f = f xpure_bind]Goals accomplished! 🐙
{ id_map: ∀ {α : Type u} (x : m α), id <\$> x = xid_map, bind_pure_comp: autoParam
(∀ {α β : Type u} (f : α → β) (x : m α),
(do
let y ← x
pure (f y)) =       f <\$> x)
_auto✝bind_pure_comp, bind_map: autoParam
(∀ {α β : Type u} (f : m (α → β)) (x : m α),
(do
let x_1 ← f
x_1 <\$> x) =       Seq.seq f fun x_1 => x)
_auto✝bind_map, pure_bind: ∀ {α β : Type u} (x : α) (f : α → m β), pure x >>= f = f xpure_bind, bind_assoc: ∀ {α β γ : Type u} (x : m α) (f : α → m β) (g : β → m γ), x >>= f >>= g = x >>= fun x => f x >>= gbind_assoc, map_pure: ∀ {α β : Type u} (g : α → β) (x : α), g <\$> pure x = pure (g x)map_pure,
comp_map := byGoals accomplished! 🐙 m: Type u → Type vinst✝: Monad mid_map: ∀ {α : Type u} (x : m α), id <\$> x = xpure_bind: ∀ {α β : Type u} (x : α) (f : α → m β), pure x >>= f = f xbind_assoc: ∀ {α β γ : Type u} (x : m α) (f : α → m β) (g : β → m γ), x >>= f >>= g = x >>= fun x => f x >>= gmap_const: autoParam (∀ {α β : Type u} (x : α) (y : m β), Functor.mapConst x y = Function.const β x <\$> y) _auto✝seqLeft_eq: autoParam
(∀ {α β : Type u} (x : m α) (y : m β),
(SeqLeft.seqLeft x fun x => y) = do
let a ← x
let _ ← y
pure a)
_auto✝seqRight_eq: autoParam
(∀ {α β : Type u} (x : m α) (y : m β),
(SeqRight.seqRight x fun x => y) = do
let _ ← x
y)
_auto✝bind_pure_comp: autoParam
(∀ {α β : Type u} (f : α → β) (x : m α),
(do
let y ← x
pure (f y)) =       f <\$> x)
_auto✝bind_map: autoParam
(∀ {α β : Type u} (f : m (α → β)) (x : m α),
(do
let x_1 ← f
x_1 <\$> x) =       Seq.seq f fun x_1 => x)
_auto✝map_pure: ∀ {α β : Type u} (g : α → β) (x : α), g <\$> pure x = pure (g x)∀ {α β γ : Type u} (g : α → β) (h : β → γ) (x : m α), (h ∘ g) <\$> x = h <\$> g <\$> xsimp [← bind_pure_comp: autoParam
(∀ {α β : Type u} (f : α → β) (x : m α),
(do
let y ← x
pure (f y)) =       f <\$> x)
_auto✝bind_pure_comp, bind_assoc: ∀ {α β γ : Type u} (x : m α) (f : α → m β) (g : β → m γ), x >>= f >>= g = x >>= fun x => f x >>= gbind_assoc, pure_bind: ∀ {α β : Type u} (x : α) (f : α → m β), pure x >>= f = f xpure_bind]Goals accomplished! 🐙
pure_seq := byGoals accomplished! 🐙 m: Type u → Type vinst✝: Monad mid_map: ∀ {α : Type u} (x : m α), id <\$> x = xpure_bind: ∀ {α β : Type u} (x : α) (f : α → m β), pure x >>= f = f xbind_assoc: ∀ {α β γ : Type u} (x : m α) (f : α → m β) (g : β → m γ), x >>= f >>= g = x >>= fun x => f x >>= gmap_const: autoParam (∀ {α β : Type u} (x : α) (y : m β), Functor.mapConst x y = Function.const β x <\$> y) _auto✝seqLeft_eq: autoParam
(∀ {α β : Type u} (x : m α) (y : m β),
(SeqLeft.seqLeft x fun x => y) = do
let a ← x
let _ ← y
pure a)
_auto✝seqRight_eq: autoParam
(∀ {α β : Type u} (x : m α) (y : m β),
(SeqRight.seqRight x fun x => y) = do
let _ ← x
y)
_auto✝bind_pure_comp: autoParam
(∀ {α β : Type u} (f : α → β) (x : m α),
(do
let y ← x
pure (f y)) =       f <\$> x)
_auto✝bind_map: autoParam
(∀ {α β : Type u} (f : m (α → β)) (x : m α),
(do
let x_1 ← f
x_1 <\$> x) =       Seq.seq f fun x_1 => x)
_auto✝map_pure: ∀ {α β : Type u} (g : α → β) (x : α), g <\$> pure x = pure (g x)∀ {α β : Type u} (g : α → β) (x : m α), (Seq.seq (pure g) fun x_1 => x) = g <\$> xintrosm: Type u → Type vinst✝: Monad mid_map: ∀ {α : Type u} (x : m α), id <\$> x = xpure_bind: ∀ {α β : Type u} (x : α) (f : α → m β), pure x >>= f = f xbind_assoc: ∀ {α β γ : Type u} (x : m α) (f : α → m β) (g : β → m γ), x >>= f >>= g = x >>= fun x => f x >>= gmap_const: autoParam (∀ {α β : Type u} (x : α) (y : m β), Functor.mapConst x y = Function.const β x <\$> y) _auto✝seqLeft_eq: autoParam
(∀ {α β : Type u} (x : m α) (y : m β),
(SeqLeft.seqLeft x fun x => y) = do
let a ← x
let _ ← y
pure a)
_auto✝seqRight_eq: autoParam
(∀ {α β : Type u} (x : m α) (y : m β),
(SeqRight.seqRight x fun x => y) = do
let _ ← x
y)
_auto✝bind_pure_comp: autoParam
(∀ {α β : Type u} (f : α → β) (x : m α),
(do
let y ← x
pure (f y)) =       f <\$> x)
_auto✝bind_map: autoParam
(∀ {α β : Type u} (f : m (α → β)) (x : m α),
(do
let x_1 ← f
x_1 <\$> x) =       Seq.seq f fun x_1 => x)
_auto✝map_pure: ∀ {α β : Type u} (g : α → β) (x : α), g <\$> pure x = pure (g x)α✝, β✝: Type ug✝: α✝ → β✝x✝: m α✝(Seq.seq (pure g✝) fun x => x✝) = g✝ <\$> x✝;m: Type u → Type vinst✝: Monad mid_map: ∀ {α : Type u} (x : m α), id <\$> x = xpure_bind: ∀ {α β : Type u} (x : α) (f : α → m β), pure x >>= f = f xbind_assoc: ∀ {α β γ : Type u} (x : m α) (f : α → m β) (g : β → m γ), x >>= f >>= g = x >>= fun x => f x >>= gmap_const: autoParam (∀ {α β : Type u} (x : α) (y : m β), Functor.mapConst x y = Function.const β x <\$> y) _auto✝seqLeft_eq: autoParam
(∀ {α β : Type u} (x : m α) (y : m β),
(SeqLeft.seqLeft x fun x => y) = do
let a ← x
let _ ← y
pure a)
_auto✝seqRight_eq: autoParam
(∀ {α β : Type u} (x : m α) (y : m β),
(SeqRight.seqRight x fun x => y) = do
let _ ← x
y)
_auto✝bind_pure_comp: autoParam
(∀ {α β : Type u} (f : α → β) (x : m α),
(do
let y ← x
pure (f y)) =       f <\$> x)
_auto✝bind_map: autoParam
(∀ {α β : Type u} (f : m (α → β)) (x : m α),
(do
let x_1 ← f
x_1 <\$> x) =       Seq.seq f fun x_1 => x)
_auto✝map_pure: ∀ {α β : Type u} (g : α → β) (x : α), g <\$> pure x = pure (g x)α✝, β✝: Type ug✝: α✝ → β✝x✝: m α✝(Seq.seq (pure g✝) fun x => x✝) = g✝ <\$> x✝ m: Type u → Type vinst✝: Monad mid_map: ∀ {α : Type u} (x : m α), id <\$> x = xpure_bind: ∀ {α β : Type u} (x : α) (f : α → m β), pure x >>= f = f xbind_assoc: ∀ {α β γ : Type u} (x : m α) (f : α → m β) (g : β → m γ), x >>= f >>= g = x >>= fun x => f x >>= gmap_const: autoParam (∀ {α β : Type u} (x : α) (y : m β), Functor.mapConst x y = Function.const β x <\$> y) _auto✝seqLeft_eq: autoParam
(∀ {α β : Type u} (x : m α) (y : m β),
(SeqLeft.seqLeft x fun x => y) = do
let a ← x
let _ ← y
pure a)
_auto✝seqRight_eq: autoParam
(∀ {α β : Type u} (x : m α) (y : m β),
(SeqRight.seqRight x fun x => y) = do
let _ ← x
y)
_auto✝bind_pure_comp: autoParam
(∀ {α β : Type u} (f : α → β) (x : m α),
(do
let y ← x
pure (f y)) =       f <\$> x)
_auto✝bind_map: autoParam
(∀ {α β : Type u} (f : m (α → β)) (x : m α),
(do
let x_1 ← f
x_1 <\$> x) =       Seq.seq f fun x_1 => x)
_auto✝map_pure: ∀ {α β : Type u} (g : α → β) (x : α), g <\$> pure x = pure (g x)∀ {α β : Type u} (g : α → β) (x : m α), (Seq.seq (pure g) fun x_1 => x) = g <\$> xrw [m: Type u → Type vinst✝: Monad mid_map: ∀ {α : Type u} (x : m α), id <\$> x = xpure_bind: ∀ {α β : Type u} (x : α) (f : α → m β), pure x >>= f = f xbind_assoc: ∀ {α β γ : Type u} (x : m α) (f : α → m β) (g : β → m γ), x >>= f >>= g = x >>= fun x => f x >>= gmap_const: autoParam (∀ {α β : Type u} (x : α) (y : m β), Functor.mapConst x y = Function.const β x <\$> y) _auto✝seqLeft_eq: autoParam
(∀ {α β : Type u} (x : m α) (y : m β),
(SeqLeft.seqLeft x fun x => y) = do
let a ← x
let _ ← y
pure a)
_auto✝seqRight_eq: autoParam
(∀ {α β : Type u} (x : m α) (y : m β),
(SeqRight.seqRight x fun x => y) = do
let _ ← x
y)
_auto✝bind_pure_comp: autoParam
(∀ {α β : Type u} (f : α → β) (x : m α),
(do
let y ← x
pure (f y)) =       f <\$> x)
_auto✝bind_map: autoParam
(∀ {α β : Type u} (f : m (α → β)) (x : m α),
(do
let x_1 ← f
x_1 <\$> x) =       Seq.seq f fun x_1 => x)
_auto✝map_pure: ∀ {α β : Type u} (g : α → β) (x : α), g <\$> pure x = pure (g x)α✝, β✝: Type ug✝: α✝ → β✝x✝: m α✝(Seq.seq (pure g✝) fun x => x✝) = g✝ <\$> x✝← bind_map: autoParam
(∀ {α β : Type u} (f : m (α → β)) (x : m α),
(do
let x_1 ← f
x_1 <\$> x) =       Seq.seq f fun x_1 => x)
_auto✝bind_mapm: Type u → Type vinst✝: Monad mid_map: ∀ {α : Type u} (x : m α), id <\$> x = xpure_bind: ∀ {α β : Type u} (x : α) (f : α → m β), pure x >>= f = f xbind_assoc: ∀ {α β γ : Type u} (x : m α) (f : α → m β) (g : β → m γ), x >>= f >>= g = x >>= fun x => f x >>= gmap_const: autoParam (∀ {α β : Type u} (x : α) (y : m β), Functor.mapConst x y = Function.const β x <\$> y) _auto✝seqLeft_eq: autoParam
(∀ {α β : Type u} (x : m α) (y : m β),
(SeqLeft.seqLeft x fun x => y) = do
let a ← x
let _ ← y
pure a)
_auto✝seqRight_eq: autoParam
(∀ {α β : Type u} (x : m α) (y : m β),
(SeqRight.seqRight x fun x => y) = do
let _ ← x
y)
_auto✝bind_pure_comp: autoParam
(∀ {α β : Type u} (f : α → β) (x : m α),
(do
let y ← x
pure (f y)) =       f <\$> x)
_auto✝bind_map: autoParam
(∀ {α β : Type u} (f : m (α → β)) (x : m α),
(do
let x_1 ← f
x_1 <\$> x) =       Seq.seq f fun x_1 => x)
_auto✝map_pure: ∀ {α β : Type u} (g : α → β) (x : α), g <\$> pure x = pure (g x)α✝, β✝: Type ug✝: α✝ → β✝x✝: m α✝(do
let x ← pure g✝
x <\$> x✝) =   g✝ <\$> x✝]m: Type u → Type vinst✝: Monad mid_map: ∀ {α : Type u} (x : m α), id <\$> x = xpure_bind: ∀ {α β : Type u} (x : α) (f : α → m β), pure x >>= f = f xbind_assoc: ∀ {α β γ : Type u} (x : m α) (f : α → m β) (g : β → m γ), x >>= f >>= g = x >>= fun x => f x >>= gmap_const: autoParam (∀ {α β : Type u} (x : α) (y : m β), Functor.mapConst x y = Function.const β x <\$> y) _auto✝seqLeft_eq: autoParam
(∀ {α β : Type u} (x : m α) (y : m β),
(SeqLeft.seqLeft x fun x => y) = do
let a ← x
let _ ← y
pure a)
_auto✝seqRight_eq: autoParam
(∀ {α β : Type u} (x : m α) (y : m β),
(SeqRight.seqRight x fun x => y) = do
let _ ← x
y)
_auto✝bind_pure_comp: autoParam
(∀ {α β : Type u} (f : α → β) (x : m α),
(do
let y ← x
pure (f y)) =       f <\$> x)
_auto✝bind_map: autoParam
(∀ {α β : Type u} (f : m (α → β)) (x : m α),
(do
let x_1 ← f
x_1 <\$> x) =       Seq.seq f fun x_1 => x)
_auto✝map_pure: ∀ {α β : Type u} (g : α → β) (x : α), g <\$> pure x = pure (g x)α✝, β✝: Type ug✝: α✝ → β✝x✝: m α✝(do
let x ← pure g✝
x <\$> x✝) =   g✝ <\$> x✝;m: Type u → Type vinst✝: Monad mid_map: ∀ {α : Type u} (x : m α), id <\$> x = xpure_bind: ∀ {α β : Type u} (x : α) (f : α → m β), pure x >>= f = f xbind_assoc: ∀ {α β γ : Type u} (x : m α) (f : α → m β) (g : β → m γ), x >>= f >>= g = x >>= fun x => f x >>= gmap_const: autoParam (∀ {α β : Type u} (x : α) (y : m β), Functor.mapConst x y = Function.const β x <\$> y) _auto✝seqLeft_eq: autoParam
(∀ {α β : Type u} (x : m α) (y : m β),
(SeqLeft.seqLeft x fun x => y) = do
let a ← x
let _ ← y
pure a)
_auto✝seqRight_eq: autoParam
(∀ {α β : Type u} (x : m α) (y : m β),
(SeqRight.seqRight x fun x => y) = do
let _ ← x
y)
_auto✝bind_pure_comp: autoParam
(∀ {α β : Type u} (f : α → β) (x : m α),
(do
let y ← x
pure (f y)) =       f <\$> x)
_auto✝bind_map: autoParam
(∀ {α β : Type u} (f : m (α → β)) (x : m α),
(do
let x_1 ← f
x_1 <\$> x) =       Seq.seq f fun x_1 => x)
_auto✝map_pure: ∀ {α β : Type u} (g : α → β) (x : α), g <\$> pure x = pure (g x)α✝, β✝: Type ug✝: α✝ → β✝x✝: m α✝(do
let x ← pure g✝
x <\$> x✝) =   g✝ <\$> x✝ m: Type u → Type vinst✝: Monad mid_map: ∀ {α : Type u} (x : m α), id <\$> x = xpure_bind: ∀ {α β : Type u} (x : α) (f : α → m β), pure x >>= f = f xbind_assoc: ∀ {α β γ : Type u} (x : m α) (f : α → m β) (g : β → m γ), x >>= f >>= g = x >>= fun x => f x >>= gmap_const: autoParam (∀ {α β : Type u} (x : α) (y : m β), Functor.mapConst x y = Function.const β x <\$> y) _auto✝seqLeft_eq: autoParam
(∀ {α β : Type u} (x : m α) (y : m β),
(SeqLeft.seqLeft x fun x => y) = do
let a ← x
let _ ← y
pure a)
_auto✝seqRight_eq: autoParam
(∀ {α β : Type u} (x : m α) (y : m β),
(SeqRight.seqRight x fun x => y) = do
let _ ← x
y)
_auto✝bind_pure_comp: autoParam
(∀ {α β : Type u} (f : α → β) (x : m α),
(do
let y ← x
pure (f y)) =       f <\$> x)
_auto✝bind_map: autoParam
(∀ {α β : Type u} (f : m (α → β)) (x : m α),
(do
let x_1 ← f
x_1 <\$> x) =       Seq.seq f fun x_1 => x)
_auto✝map_pure: ∀ {α β : Type u} (g : α → β) (x : α), g <\$> pure x = pure (g x)∀ {α β : Type u} (g : α → β) (x : m α), (Seq.seq (pure g) fun x_1 => x) = g <\$> xsimp [pure_bind: ∀ {α β : Type u} (x : α) (f : α → m β), pure x >>= f = f xpure_bind]Goals accomplished! 🐙
seq_pure := byGoals accomplished! 🐙 m: Type u → Type vinst✝: Monad mid_map: ∀ {α : Type u} (x : m α), id <\$> x = xpure_bind: ∀ {α β : Type u} (x : α) (f : α → m β), pure x >>= f = f xbind_assoc: ∀ {α β γ : Type u} (x : m α) (f : α → m β) (g : β → m γ), x >>= f >>= g = x >>= fun x => f x >>= gmap_const: autoParam (∀ {α β : Type u} (x : α) (y : m β), Functor.mapConst x y = Function.const β x <\$> y) _auto✝seqLeft_eq: autoParam
(∀ {α β : Type u} (x : m α) (y : m β),
(SeqLeft.seqLeft x fun x => y) = do
let a ← x
let _ ← y
pure a)
_auto✝seqRight_eq: autoParam
(∀ {α β : Type u} (x : m α) (y : m β),
(SeqRight.seqRight x fun x => y) = do
let _ ← x
y)
_auto✝bind_pure_comp: autoParam
(∀ {α β : Type u} (f : α → β) (x : m α),
(do
let y ← x
pure (f y)) =       f <\$> x)
_auto✝bind_map: autoParam
(∀ {α β : Type u} (f : m (α → β)) (x : m α),
(do
let x_1 ← f
x_1 <\$> x) =       Seq.seq f fun x_1 => x)
_auto✝map_pure: ∀ {α β : Type u} (g : α → β) (x : α), g <\$> pure x = pure (g x)∀ {α β : Type u} (g : m (α → β)) (x : α), (Seq.seq g fun x_1 => pure x) = (fun h => h x) <\$> gintrosm: Type u → Type vinst✝: Monad mid_map: ∀ {α : Type u} (x : m α), id <\$> x = xpure_bind: ∀ {α β : Type u} (x : α) (f : α → m β), pure x >>= f = f xbind_assoc: ∀ {α β γ : Type u} (x : m α) (f : α → m β) (g : β → m γ), x >>= f >>= g = x >>= fun x => f x >>= gmap_const: autoParam (∀ {α β : Type u} (x : α) (y : m β), Functor.mapConst x y = Function.const β x <\$> y) _auto✝seqLeft_eq: autoParam
(∀ {α β : Type u} (x : m α) (y : m β),
(SeqLeft.seqLeft x fun x => y) = do
let a ← x
let _ ← y
pure a)
_auto✝seqRight_eq: autoParam
(∀ {α β : Type u} (x : m α) (y : m β),
(SeqRight.seqRight x fun x => y) = do
let _ ← x
y)
_auto✝bind_pure_comp: autoParam
(∀ {α β : Type u} (f : α → β) (x : m α),
(do
let y ← x
pure (f y)) =       f <\$> x)
_auto✝bind_map: autoParam
(∀ {α β : Type u} (f : m (α → β)) (x : m α),
(do
let x_1 ← f
x_1 <\$> x) =       Seq.seq f fun x_1 => x)
_auto✝map_pure: ∀ {α β : Type u} (g : α → β) (x : α), g <\$> pure x = pure (g x)α✝, β✝: Type ug✝: m (α✝ → β✝)x✝: α✝(Seq.seq g✝ fun x => pure x✝) = (fun h => h x✝) <\$> g✝;m: Type u → Type vinst✝: Monad mid_map: ∀ {α : Type u} (x : m α), id <\$> x = xpure_bind: ∀ {α β : Type u} (x : α) (f : α → m β), pure x >>= f = f xbind_assoc: ∀ {α β γ : Type u} (x : m α) (f : α → m β) (g : β → m γ), x >>= f >>= g = x >>= fun x => f x >>= gmap_const: autoParam (∀ {α β : Type u} (x : α) (y : m β), Functor.mapConst x y = Function.const β x <\$> y) _auto✝seqLeft_eq: autoParam
(∀ {α β : Type u} (x : m α) (y : m β),
(SeqLeft.seqLeft x fun x => y) = do
let a ← x
let _ ← y
pure a)
_auto✝seqRight_eq: autoParam
(∀ {α β : Type u} (x : m α) (y : m β),
(SeqRight.seqRight x fun x => y) = do
let _ ← x
y)
_auto✝bind_pure_comp: autoParam
(∀ {α β : Type u} (f : α → β) (x : m α),
(do
let y ← x
pure (f y)) =       f <\$> x)
_auto✝bind_map: autoParam
(∀ {α β : Type u} (f : m (α → β)) (x : m α),
(do
let x_1 ← f
x_1 <\$> x) =       Seq.seq f fun x_1 => x)
_auto✝map_pure: ∀ {α β : Type u} (g : α → β) (x : α), g <\$> pure x = pure (g x)α✝, β✝: Type ug✝: m (α✝ → β✝)x✝: α✝(Seq.seq g✝ fun x => pure x✝) = (fun h => h x✝) <\$> g✝ m: Type u → Type vinst✝: Monad mid_map: ∀ {α : Type u} (x : m α), id <\$> x = xpure_bind: ∀ {α β : Type u} (x : α) (f : α → m β), pure x >>= f = f xbind_assoc: ∀ {α β γ : Type u} (x : m α) (f : α → m β) (g : β → m γ), x >>= f >>= g = x >>= fun x => f x >>= gmap_const: autoParam (∀ {α β : Type u} (x : α) (y : m β), Functor.mapConst x y = Function.const β x <\$> y) _auto✝seqLeft_eq: autoParam
(∀ {α β : Type u} (x : m α) (y : m β),
(SeqLeft.seqLeft x fun x => y) = do
let a ← x
let _ ← y
pure a)
_auto✝seqRight_eq: autoParam
(∀ {α β : Type u} (x : m α) (y : m β),
(SeqRight.seqRight x fun x => y) = do
let _ ← x
y)
_auto✝bind_pure_comp: autoParam
(∀ {α β : Type u} (f : α → β) (x : m α),
(do
let y ← x
pure (f y)) =       f <\$> x)
_auto✝bind_map: autoParam
(∀ {α β : Type u} (f : m (α → β)) (x : m α),
(do
let x_1 ← f
x_1 <\$> x) =       Seq.seq f fun x_1 => x)
_auto✝map_pure: ∀ {α β : Type u} (g : α → β) (x : α), g <\$> pure x = pure (g x)∀ {α β : Type u} (g : m (α → β)) (x : α), (Seq.seq g fun x_1 => pure x) = (fun h => h x) <\$> grw [m: Type u → Type vinst✝: Monad mid_map: ∀ {α : Type u} (x : m α), id <\$> x = xpure_bind: ∀ {α β : Type u} (x : α) (f : α → m β), pure x >>= f = f xbind_assoc: ∀ {α β γ : Type u} (x : m α) (f : α → m β) (g : β → m γ), x >>= f >>= g = x >>= fun x => f x >>= gmap_const: autoParam (∀ {α β : Type u} (x : α) (y : m β), Functor.mapConst x y = Function.const β x <\$> y) _auto✝seqLeft_eq: autoParam
(∀ {α β : Type u} (x : m α) (y : m β),
(SeqLeft.seqLeft x fun x => y) = do
let a ← x
let _ ← y
pure a)
_auto✝seqRight_eq: autoParam
(∀ {α β : Type u} (x : m α) (y : m β),
(SeqRight.seqRight x fun x => y) = do
let _ ← x
y)
_auto✝bind_pure_comp: autoParam
(∀ {α β : Type u} (f : α → β) (x : m α),
(do
let y ← x
pure (f y)) =       f <\$> x)
_auto✝bind_map: autoParam
(∀ {α β : Type u} (f : m (α → β)) (x : m α),
(do
let x_1 ← f
x_1 <\$> x) =       Seq.seq f fun x_1 => x)
_auto✝map_pure: ∀ {α β : Type u} (g : α → β) (x : α), g <\$> pure x = pure (g x)α✝, β✝: Type ug✝: m (α✝ → β✝)x✝: α✝(Seq.seq g✝ fun x => pure x✝) = (fun h => h x✝) <\$> g✝← bind_map: autoParam
(∀ {α β : Type u} (f : m (α → β)) (x : m α),
(do
let x_1 ← f
x_1 <\$> x) =       Seq.seq f fun x_1 => x)
_auto✝bind_mapm: Type u → Type vinst✝: Monad mid_map: ∀ {α : Type u} (x : m α), id <\$> x = xpure_bind: ∀ {α β : Type u} (x : α) (f : α → m β), pure x >>= f = f xbind_assoc: ∀ {α β γ : Type u} (x : m α) (f : α → m β) (g : β → m γ), x >>= f >>= g = x >>= fun x => f x >>= gmap_const: autoParam (∀ {α β : Type u} (x : α) (y : m β), Functor.mapConst x y = Function.const β x <\$> y) _auto✝seqLeft_eq: autoParam
(∀ {α β : Type u} (x : m α) (y : m β),
(SeqLeft.seqLeft x fun x => y) = do
let a ← x
let _ ← y
pure a)
_auto✝seqRight_eq: autoParam
(∀ {α β : Type u} (x : m α) (y : m β),
(SeqRight.seqRight x fun x => y) = do
let _ ← x
y)
_auto✝bind_pure_comp: autoParam
(∀ {α β : Type u} (f : α → β) (x : m α),
(do
let y ← x
pure (f y)) =       f <\$> x)
_auto✝bind_map: autoParam
(∀ {α β : Type u} (f : m (α → β)) (x : m α),
(do
let x_1 ← f
x_1 <\$> x) =       Seq.seq f fun x_1 => x)
_auto✝map_pure: ∀ {α β : Type u} (g : α → β) (x : α), g <\$> pure x = pure (g x)α✝, β✝: Type ug✝: m (α✝ → β✝)x✝: α✝(do
let x ← g✝
x <\$> pure x✝) =   (fun h => h x✝) <\$> g✝]m: Type u → Type vinst✝: Monad mid_map: ∀ {α : Type u} (x : m α), id <\$> x = xpure_bind: ∀ {α β : Type u} (x : α) (f : α → m β), pure x >>= f = f xbind_assoc: ∀ {α β γ : Type u} (x : m α) (f : α → m β) (g : β → m γ), x >>= f >>= g = x >>= fun x => f x >>= gmap_const: autoParam (∀ {α β : Type u} (x : α) (y : m β), Functor.mapConst x y = Function.const β x <\$> y) _auto✝seqLeft_eq: autoParam
(∀ {α β : Type u} (x : m α) (y : m β),
(SeqLeft.seqLeft x fun x => y) = do
let a ← x
let _ ← y
pure a)
_auto✝seqRight_eq: autoParam
(∀ {α β : Type u} (x : m α) (y : m β),
(SeqRight.seqRight x fun x => y) = do
let _ ← x
y)
_auto✝bind_pure_comp: autoParam
(∀ {α β : Type u} (f : α → β) (x : m α),
(do
let y ← x
pure (f y)) =       f <\$> x)
_auto✝bind_map: autoParam
(∀ {α β : Type u} (f : m (α → β)) (x : m α),
(do
let x_1 ← f
x_1 <\$> x) =       Seq.seq f fun x_1 => x)
_auto✝map_pure: ∀ {α β : Type u} (g : α → β) (x : α), g <\$> pure x = pure (g x)α✝, β✝: Type ug✝: m (α✝ → β✝)x✝: α✝(do
let x ← g✝
x <\$> pure x✝) =   (fun h => h x✝) <\$> g✝;m: Type u → Type vinst✝: Monad mid_map: ∀ {α : Type u} (x : m α), id <\$> x = xpure_bind: ∀ {α β : Type u} (x : α) (f : α → m β), pure x >>= f = f xbind_assoc: ∀ {α β γ : Type u} (x : m α) (f : α → m β) (g : β → m γ), x >>= f >>= g = x >>= fun x => f x >>= gmap_const: autoParam (∀ {α β : Type u} (x : α) (y : m β), Functor.mapConst x y = Function.const β x <\$> y) _auto✝seqLeft_eq: autoParam
(∀ {α β : Type u} (x : m α) (y : m β),
(SeqLeft.seqLeft x fun x => y) = do
let a ← x
let _ ← y
pure a)
_auto✝seqRight_eq: autoParam
(∀ {α β : Type u} (x : m α) (y : m β),
(SeqRight.seqRight x fun x => y) = do
let _ ← x
y)
_auto✝bind_pure_comp: autoParam
(∀ {α β : Type u} (f : α → β) (x : m α),
(do
let y ← x
pure (f y)) =       f <\$> x)
_auto✝bind_map: autoParam
(∀ {α β : Type u} (f : m (α → β)) (x : m α),
(do
let x_1 ← f
x_1 <\$> x) =       Seq.seq f fun x_1 => x)
_auto✝map_pure: ∀ {α β : Type u} (g : α → β) (x : α), g <\$> pure x = pure (g x)α✝, β✝: Type ug✝: m (α✝ → β✝)x✝: α✝(do
let x ← g✝
x <\$> pure x✝) =   (fun h => h x✝) <\$> g✝ m: Type u → Type vinst✝: Monad mid_map: ∀ {α : Type u} (x : m α), id <\$> x = xpure_bind: ∀ {α β : Type u} (x : α) (f : α → m β), pure x >>= f = f xbind_assoc: ∀ {α β γ : Type u} (x : m α) (f : α → m β) (g : β → m γ), x >>= f >>= g = x >>= fun x => f x >>= gmap_const: autoParam (∀ {α β : Type u} (x : α) (y : m β), Functor.mapConst x y = Function.const β x <\$> y) _auto✝seqLeft_eq: autoParam
(∀ {α β : Type u} (x : m α) (y : m β),
(SeqLeft.seqLeft x fun x => y) = do
let a ← x
let _ ← y
pure a)
_auto✝seqRight_eq: autoParam
(∀ {α β : Type u} (x : m α) (y : m β),
(SeqRight.seqRight x fun x => y) = do
let _ ← x
y)
_auto✝bind_pure_comp: autoParam
(∀ {α β : Type u} (f : α → β) (x : m α),
(do
let y ← x
pure (f y)) =       f <\$> x)
_auto✝bind_map: autoParam
(∀ {α β : Type u} (f : m (α → β)) (x : m α),
(do
let x_1 ← f
x_1 <\$> x) =       Seq.seq f fun x_1 => x)
_auto✝map_pure: ∀ {α β : Type u} (g : α → β) (x : α), g <\$> pure x = pure (g x)∀ {α β : Type u} (g : m (α → β)) (x : α), (Seq.seq g fun x_1 => pure x) = (fun h => h x) <\$> gsimp [map_pure: ∀ {α β : Type u} (g : α → β) (x : α), g <\$> pure x = pure (g x)map_pure, bind_pure_comp: autoParam
(∀ {α β : Type u} (f : α → β) (x : m α),
(do
let y ← x
pure (f y)) =       f <\$> x)
_auto✝bind_pure_comp]Goals accomplished! 🐙
seq_assoc := byGoals accomplished! 🐙 m: Type u → Type vinst✝: Monad mid_map: ∀ {α : Type u} (x : m α), id <\$> x = xpure_bind: ∀ {α β : Type u} (x : α) (f : α → m β), pure x >>= f = f xbind_assoc: ∀ {α β γ : Type u} (x : m α) (f : α → m β) (g : β → m γ), x >>= f >>= g = x >>= fun x => f x >>= gmap_const: autoParam (∀ {α β : Type u} (x : α) (y : m β), Functor.mapConst x y = Function.const β x <\$> y) _auto✝seqLeft_eq: autoParam
(∀ {α β : Type u} (x : m α) (y : m β),
(SeqLeft.seqLeft x fun x => y) = do
let a ← x
let _ ← y
pure a)
_auto✝seqRight_eq: autoParam
(∀ {α β : Type u} (x : m α) (y : m β),
(SeqRight.seqRight x fun x => y) = do
let _ ← x
y)
_auto✝bind_pure_comp: autoParam
(∀ {α β : Type u} (f : α → β) (x : m α),
(do
let y ← x
pure (f y)) =       f <\$> x)
_auto✝bind_map: autoParam
(∀ {α β : Type u} (f : m (α → β)) (x : m α),
(do
let x_1 ← f
x_1 <\$> x) =       Seq.seq f fun x_1 => x)
_auto✝map_pure: ∀ {α β : Type u} (g : α → β) (x : α), g <\$> pure x = pure (g x)∀ {α β γ : Type u} (x : m α) (g : m (α → β)) (h : m (β → γ)),
(Seq.seq h fun x_1 => Seq.seq g fun x_2 => x) = Seq.seq (Seq.seq (Function.comp <\$> h) fun x => g) fun x_1 => xsimp [← bind_pure_comp: autoParam
(∀ {α β : Type u} (f : α → β) (x : m α),
(do
let y ← x
pure (f y)) =       f <\$> x)
_auto✝bind_pure_comp, ← bind_map: autoParam
(∀ {α β : Type u} (f : m (α → β)) (x : m α),
(do
let x_1 ← f
x_1 <\$> x) =       Seq.seq f fun x_1 => x)
_auto✝bind_map, bind_assoc: ∀ {α β γ : Type u} (x : m α) (f : α → m β) (g : β → m γ), x >>= f >>= g = x >>= fun x => f x >>= gbind_assoc, pure_bind: ∀ {α β : Type u} (x : α) (f : α → m β), pure x >>= f = f xpure_bind]Goals accomplished! 🐙
map_const := funext: ∀ {α : Sort ?u.1235} {β : α → Sort ?u.1234} {f g : (x : α) → β x}, (∀ (x : α), f x = g x) → f = gfunext fun x: ?m.1250x => funext: ∀ {α : Sort ?u.1253} {β : α → Sort ?u.1252} {f g : (x : α) → β x}, (∀ (x : α), f x = g x) → f = gfunext (map_const: autoParam (∀ {α β : Type u} (x : α) (y : m β), Functor.mapConst x y = Function.const β x <\$> y) _auto✝map_const x: ?m.1250x)
seqLeft_eq := byGoals accomplished! 🐙 m: Type u → Type vinst✝: Monad mid_map: ∀ {α : Type u} (x : m α), id <\$> x = xpure_bind: ∀ {α β : Type u} (x : α) (f : α → m β), pure x >>= f = f xbind_assoc: ∀ {α β γ : Type u} (x : m α) (f : α → m β) (g : β → m γ), x >>= f >>= g = x >>= fun x => f x >>= gmap_const: autoParam (∀ {α β : Type u} (x : α) (y : m β), Functor.mapConst x y = Function.const β x <\$> y) _auto✝seqLeft_eq: autoParam
(∀ {α β : Type u} (x : m α) (y : m β),
(SeqLeft.seqLeft x fun x => y) = do
let a ← x
let _ ← y
pure a)
_auto✝seqRight_eq: autoParam
(∀ {α β : Type u} (x : m α) (y : m β),
(SeqRight.seqRight x fun x => y) = do
let _ ← x
y)
_auto✝bind_pure_comp: autoParam
(∀ {α β : Type u} (f : α → β) (x : m α),
(do
let y ← x
pure (f y)) =       f <\$> x)
_auto✝bind_map: autoParam
(∀ {α β : Type u} (f : m (α → β)) (x : m α),
(do
let x_1 ← f
x_1 <\$> x) =       Seq.seq f fun x_1 => x)
_auto✝map_pure: ∀ {α β : Type u} (g : α → β) (x : α), g <\$> pure x = pure (g x)∀ {α β : Type u} (x : m α) (y : m β), (SeqLeft.seqLeft x fun x => y) = Seq.seq (Function.const β <\$> x) fun x => ysimp [seqLeft_eq: autoParam
(∀ {α β : Type u} (x : m α) (y : m β),
(SeqLeft.seqLeft x fun x => y) = do
let a ← x
let _ ← y
pure a)
_auto✝seqLeft_eq, ← bind_map: autoParam
(∀ {α β : Type u} (f : m (α → β)) (x : m α),
(do
let x_1 ← f
x_1 <\$> x) =       Seq.seq f fun x_1 => x)
_auto✝bind_map, ← bind_pure_comp: autoParam
(∀ {α β : Type u} (f : α → β) (x : m α),
(do
let y ← x
pure (f y)) =       f <\$> x)
_auto✝bind_pure_comp, pure_bind: ∀ {α β : Type u} (x : α) (f : α → m β), pure x >>= f = f xpure_bind, bind_assoc: ∀ {α β γ : Type u} (x : m α) (f : α → m β) (g : β → m γ), x >>= f >>= g = x >>= fun x => f x >>= gbind_assoc]Goals accomplished! 🐙
seqRight_eq := fun x: ?m.1291x y: ?m.1294y => byGoals accomplished! 🐙
m: Type u → Type vinst✝: Monad mid_map: ∀ {α : Type u} (x : m α), id <\$> x = xpure_bind: ∀ {α β : Type u} (x : α) (f : α → m β), pure x >>= f = f xbind_assoc: ∀ {α β γ : Type u} (x : m α) (f : α → m β) (g : β → m γ), x >>= f >>= g = x >>= fun x => f x >>= gmap_const: autoParam (∀ {α β : Type u} (x : α) (y : m β), Functor.mapConst x y = Function.const β x <\$> y) _auto✝seqLeft_eq: autoParam
(∀ {α β : Type u} (x : m α) (y : m β),
(SeqLeft.seqLeft x fun x => y) = do
let a ← x
let _ ← y
pure a)
_auto✝seqRight_eq: autoParam
(∀ {α β : Type u} (x : m α) (y : m β),
(SeqRight.seqRight x fun x => y) = do
let _ ← x
y)
_auto✝bind_pure_comp: autoParam
(∀ {α β : Type u} (f : α → β) (x : m α),
(do
let y ← x
pure (f y)) =       f <\$> x)
_auto✝bind_map: autoParam
(∀ {α β : Type u} (f : m (α → β)) (x : m α),
(do
let x_1 ← f
x_1 <\$> x) =       Seq.seq f fun x_1 => x)
_auto✝map_pure: ∀ {α β : Type u} (g : α → β) (x : α), g <\$> pure x = pure (g x)α✝, β✝: Type ux: m α✝y: m β✝(SeqRight.seqRight x fun x => y) = Seq.seq (Function.const α✝ id <\$> x) fun x => yrw [m: Type u → Type vinst✝: Monad mid_map: ∀ {α : Type u} (x : m α), id <\$> x = xpure_bind: ∀ {α β : Type u} (x : α) (f : α → m β), pure x >>= f = f xbind_assoc: ∀ {α β γ : Type u} (x : m α) (f : α → m β) (g : β → m γ), x >>= f >>= g = x >>= fun x => f x >>= gmap_const: autoParam (∀ {α β : Type u} (x : α) (y : m β), Functor.mapConst x y = Function.const β x <\$> y) _auto✝seqLeft_eq: autoParam
(∀ {α β : Type u} (x : m α) (y : m β),
(SeqLeft.seqLeft x fun x => y) = do
let a ← x
let _ ← y
pure a)
_auto✝seqRight_eq: autoParam
(∀ {α β : Type u} (x : m α) (y : m β),
(SeqRight.seqRight x fun x => y) = do
let _ ← x
y)
_auto✝bind_pure_comp: autoParam
(∀ {α β : Type u} (f : α → β) (x : m α),
(do
let y ← x
pure (f y)) =       f <\$> x)
_auto✝bind_map: autoParam
(∀ {α β : Type u} (f : m (α → β)) (x : m α),
(do
let x_1 ← f
x_1 <\$> x) =       Seq.seq f fun x_1 => x)
_auto✝map_pure: ∀ {α β : Type u} (g : α → β) (x : α), g <\$> pure x = pure (g x)α✝, β✝: Type ux: m α✝y: m β✝(SeqRight.seqRight x fun x => y) = Seq.seq (Function.const α✝ id <\$> x) fun x => yseqRight_eq: autoParam
(∀ {α β : Type u} (x : m α) (y : m β),
(SeqRight.seqRight x fun x => y) = do
let _ ← x
y)
_auto✝seqRight_eq,m: Type u → Type vinst✝: Monad mid_map: ∀ {α : Type u} (x : m α), id <\$> x = xpure_bind: ∀ {α β : Type u} (x : α) (f : α → m β), pure x >>= f = f xbind_assoc: ∀ {α β γ : Type u} (x : m α) (f : α → m β) (g : β → m γ), x >>= f >>= g = x >>= fun x => f x >>= gmap_const: autoParam (∀ {α β : Type u} (x : α) (y : m β), Functor.mapConst x y = Function.const β x <\$> y) _auto✝seqLeft_eq: autoParam
(∀ {α β : Type u} (x : m α) (y : m β),
(SeqLeft.seqLeft x fun x => y) = do
let a ← x
let _ ← y
pure a)
_auto✝seqRight_eq: autoParam
(∀ {α β : Type u} (x : m α) (y : m β),
(SeqRight.seqRight x fun x => y) = do
let _ ← x
y)
_auto✝bind_pure_comp: autoParam
(∀ {α β : Type u} (f : α → β) (x : m α),
(do
let y ← x
pure (f y)) =       f <\$> x)
_auto✝bind_map: autoParam
(∀ {α β : Type u} (f : m (α → β)) (x : m α),
(do
let x_1 ← f
x_1 <\$> x) =       Seq.seq f fun x_1 => x)
_auto✝map_pure: ∀ {α β : Type u} (g : α → β) (x : α), g <\$> pure x = pure (g x)α✝, β✝: Type ux: m α✝y: m β✝(do
let _ ← x
y) =   Seq.seq (Function.const α✝ id <\$> x) fun x => y m: Type u → Type vinst✝: Monad mid_map: ∀ {α : Type u} (x : m α), id <\$> x = xpure_bind: ∀ {α β : Type u} (x : α) (f : α → m β), pure x >>= f = f xbind_assoc: ∀ {α β γ : Type u} (x : m α) (f : α → m β) (g : β → m γ), x >>= f >>= g = x >>= fun x => f x >>= gmap_const: autoParam (∀ {α β : Type u} (x : α) (y : m β), Functor.mapConst x y = Function.const β x <\$> y) _auto✝seqLeft_eq: autoParam
(∀ {α β : Type u} (x : m α) (y : m β),
(SeqLeft.seqLeft x fun x => y) = do
let a ← x
let _ ← y
pure a)
_auto✝seqRight_eq: autoParam
(∀ {α β : Type u} (x : m α) (y : m β),
(SeqRight.seqRight x fun x => y) = do
let _ ← x
y)
_auto✝bind_pure_comp: autoParam
(∀ {α β : Type u} (f : α → β) (x : m α),
(do
let y ← x
pure (f y)) =       f <\$> x)
_auto✝bind_map: autoParam
(∀ {α β : Type u} (f : m (α → β)) (x : m α),
(do
let x_1 ← f
x_1 <\$> x) =       Seq.seq f fun x_1 => x)
_auto✝map_pure: ∀ {α β : Type u} (g : α → β) (x : α), g <\$> pure x = pure (g x)α✝, β✝: Type ux: m α✝y: m β✝(SeqRight.seqRight x fun x => y) = Seq.seq (Function.const α✝ id <\$> x) fun x => y← bind_map: autoParam
(∀ {α β : Type u} (f : m (α → β)) (x : m α),
(do
let x_1 ← f
x_1 <\$> x) =       Seq.seq f fun x_1 => x)
_auto✝bind_map,m: Type u → Type vinst✝: Monad mid_map: ∀ {α : Type u} (x : m α), id <\$> x = xpure_bind: ∀ {α β : Type u} (x : α) (f : α → m β), pure x >>= f = f xbind_assoc: ∀ {α β γ : Type u} (x : m α) (f : α → m β) (g : β → m γ), x >>= f >>= g = x >>= fun x => f x >>= gmap_const: autoParam (∀ {α β : Type u} (x : α) (y : m β), Functor.mapConst x y = Function.const β x <\$> y) _auto✝seqLeft_eq: autoParam
(∀ {α β : Type u} (x : m α) (y : m β),
(SeqLeft.seqLeft x fun x => y) = do
let a ← x
let _ ← y
pure a)
_auto✝seqRight_eq: autoParam
(∀ {α β : Type u} (x : m α) (y : m β),
(SeqRight.seqRight x fun x => y) = do
let _ ← x
y)
_auto✝bind_pure_comp: autoParam
(∀ {α β : Type u} (f : α → β) (x : m α),
(do
let y ← x
pure (f y)) =       f <\$> x)
_auto✝bind_map: autoParam
(∀ {α β : Type u} (f : m (α → β)) (x : m α),
(do
let x_1 ← f
x_1 <\$> x) =       Seq.seq f fun x_1 => x)
_auto✝map_pure: ∀ {α β : Type u} (g : α → β) (x : α), g <\$> pure x = pure (g x)α✝, β✝: Type ux: m α✝y: m β✝(do
let _ ← x
y) =   do
let x ← Function.const α✝ id <\$> x
x <\$> y m: Type u → Type vinst✝: Monad mid_map: ∀ {α : Type u} (x : m α), id <\$> x = xpure_bind: ∀ {α β : Type u} (x : α) (f : α → m β), pure x >>= f = f xbind_assoc: ∀ {α β γ : Type u} (x : m α) (f : α → m β) (g : β → m γ), x >>= f >>= g = x >>= fun x => f x >>= gmap_const: autoParam (∀ {α β : Type u} (x : α) (y : m β), Functor.mapConst x y = Function.const β x <\$> y) _auto✝seqLeft_eq: autoParam
(∀ {α β : Type u} (x : m α) (y : m β),
(SeqLeft.seqLeft x fun x => y) = do
let a ← x
let _ ← y
pure a)
_auto✝seqRight_eq: autoParam
(∀ {α β : Type u} (x : m α) (y : m β),
(SeqRight.seqRight x fun x => y) = do
let _ ← x
y)
_auto✝bind_pure_comp: autoParam
(∀ {α β : Type u} (f : α → β) (x : m α),
(do
let y ← x
pure (f y)) =       f <\$> x)
_auto✝bind_map: autoParam
(∀ {α β : Type u} (f : m (α → β)) (x : m α),
(do
let x_1 ← f
x_1 <\$> x) =       Seq.seq f fun x_1 => x)
_auto✝map_pure: ∀ {α β : Type u} (g : α → β) (x : α), g <\$> pure x = pure (g x)α✝, β✝: Type ux: m α✝y: m β✝(SeqRight.seqRight x fun x => y) = Seq.seq (Function.const α✝ id <\$> x) fun x => y← bind_pure_comp: autoParam
(∀ {α β : Type u} (f : α → β) (x : m α),
(do
let y ← x
pure (f y)) =       f <\$> x)
_auto✝bind_pure_comp,m: Type u → Type vinst✝: Monad mid_map: ∀ {α : Type u} (x : m α), id <\$> x = xpure_bind: ∀ {α β : Type u} (x : α) (f : α → m β), pure x >>= f = f xbind_assoc: ∀ {α β γ : Type u} (x : m α) (f : α → m β) (g : β → m γ), x >>= f >>= g = x >>= fun x => f x >>= gmap_const: autoParam (∀ {α β : Type u} (x : α) (y : m β), Functor.mapConst x y = Function.const β x <\$> y) _auto✝seqLeft_eq: autoParam
(∀ {α β : Type u} (x : m α) (y : m β),
(SeqLeft.seqLeft x fun x => y) = do
let a ← x
let _ ← y
pure a)
_auto✝seqRight_eq: autoParam
(∀ {α β : Type u} (x : m α) (y : m β),
(SeqRight.seqRight x fun x => y) = do
let _ ← x
y)
_auto✝bind_pure_comp: autoParam
(∀ {α β : Type u} (f : α → β) (x : m α),
(do
let y ← x
pure (f y)) =       f <\$> x)
_auto✝bind_map: autoParam
(∀ {α β : Type u} (f : m (α → β)) (x : m α),
(do
let x_1 ← f
x_1 <\$> x) =       Seq.seq f fun x_1 => x)
_auto✝map_pure: ∀ {α β : Type u} (g : α → β) (x : α), g <\$> pure x = pure (g x)α✝, β✝: Type ux: m α✝y: m β✝(do
let _ ← x
y) =   do
let x ←
do
let y ← x
pure (Function.const α✝ id y)
x <\$> y m: Type u → Type vinst✝: Monad mid_map: ∀ {α : Type u} (x : m α), id <\$> x = xpure_bind: ∀ {α β : Type u} (x : α) (f : α → m β), pure x >>= f = f xbind_assoc: ∀ {α β γ : Type u} (x : m α) (f : α → m β) (g : β → m γ), x >>= f >>= g = x >>= fun x => f x >>= gmap_const: autoParam (∀ {α β : Type u} (x : α) (y : m β), Functor.mapConst x y = Function.const β x <\$> y) _auto✝seqLeft_eq: autoParam
(∀ {α β : Type u} (x : m α) (y : m β),
(SeqLeft.seqLeft x fun x => y) = do
let a ← x
let _ ← y
pure a)
_auto✝seqRight_eq: autoParam
(∀ {α β : Type u} (x : m α) (y : m β),
(SeqRight.seqRight x fun x => y) = do
let _ ← x
y)
_auto✝bind_pure_comp: autoParam
(∀ {α β : Type u} (f : α → β) (x : m α),
(do
let y ← x
pure (f y)) =       f <\$> x)
_auto✝bind_map: autoParam
(∀ {α β : Type u} (f : m (α → β)) (x : m α),
(do
let x_1 ← f
x_1 <\$> x) =       Seq.seq f fun x_1 => x)
_auto✝map_pure: ∀ {α β : Type u} (g : α → β) (x : α), g <\$> pure x = pure (g x)α✝, β✝: Type ux: m α✝y: m β✝(SeqRight.seqRight x fun x => y) = Seq.seq (Function.const α✝ id <\$> x) fun x => ybind_assoc: ∀ {α β γ : Type u} (x : m α) (f : α → m β) (g : β → m γ), x >>= f >>= g = x >>= fun x => f x >>= gbind_assocm: Type u → Type vinst✝: Monad mid_map: ∀ {α : Type u} (x : m α), id <\$> x = xpure_bind: ∀ {α β : Type u} (x : α) (f : α → m β), pure x >>= f = f xbind_assoc: ∀ {α β γ : Type u} (x : m α) (f : α → m β) (g : β → m γ), x >>= f >>= g = x >>= fun x => f x >>= gmap_const: autoParam (∀ {α β : Type u} (x : α) (y : m β), Functor.mapConst x y = Function.const β x <\$> y) _auto✝seqLeft_eq: autoParam
(∀ {α β : Type u} (x : m α) (y : m β),
(SeqLeft.seqLeft x fun x => y) = do
let a ← x
let _ ← y
pure a)
_auto✝seqRight_eq: autoParam
(∀ {α β : Type u} (x : m α) (y : m β),
(SeqRight.seqRight x fun x => y) = do
let _ ← x
y)
_auto✝bind_pure_comp: autoParam
(∀ {α β : Type u} (f : α → β) (x : m α),
(do
let y ← x
pure (f y)) =       f <\$> x)
_auto✝bind_map: autoParam
(∀ {α β : Type u} (f : m (α → β)) (x : m α),
(do
let x_1 ← f
x_1 <\$> x) =       Seq.seq f fun x_1 => x)
_auto✝map_pure: ∀ {α β : Type u} (g : α → β) (x : α), g <\$> pure x = pure (g x)α✝, β✝: Type ux: m α✝y: m β✝(do
let _ ← x
y) =   do
let x ← x
let x ← pure (Function.const α✝ id x)
x <\$> y]m: Type u → Type vinst✝: Monad mid_map: ∀ {α : Type u} (x : m α), id <\$> x = xpure_bind: ∀ {α β : Type u} (x : α) (f : α → m β), pure x >>= f = f xbind_assoc: ∀ {α β γ : Type u} (x : m α) (f : α → m β) (g : β → m γ), x >>= f >>= g = x >>= fun x => f x >>= gmap_const: autoParam (∀ {α β : Type u} (x : α) (y : m β), Functor.mapConst x y = Function.const β x <\$> y) _auto✝seqLeft_eq: autoParam
(∀ {α β : Type u} (x : m α) (y : m β),
(SeqLeft.seqLeft x fun x => y) = do
let a ← x
let _ ← y
pure a)
_auto✝seqRight_eq: autoParam
(∀ {α β : Type u} (x : m α) (y : m β),
(SeqRight.seqRight x fun x => y) = do
let _ ← x
y)
_auto✝bind_pure_comp: autoParam
(∀ {α β : Type u} (f : α → β) (x : m α),
(do
let y ← x
pure (f y)) =       f <\$> x)
_auto✝bind_map: autoParam
(∀ {α β : Type u} (f : m (α → β)) (x : m α),
(do
let x_1 ← f
x_1 <\$> x) =       Seq.seq f fun x_1 => x)
_auto✝map_pure: ∀ {α β : Type u} (g : α → β) (x : α), g <\$> pure x = pure (g x)α✝, β✝: Type ux: m α✝y: m β✝(do
let _ ← x
y) =   do
let x ← x
let x ← pure (Function.const α✝ id x)
x <\$> y;m: Type u → Type vinst✝: Monad mid_map: ∀ {α : Type u} (x : m α), id <\$> x = xpure_bind: ∀ {α β : Type u} (x : α) (f : α → m β), pure x >>= f = f xbind_assoc: ∀ {α β γ : Type u} (x : m α) (f : α → m β) (g : β → m γ), x >>= f >>= g = x >>= fun x => f x >>= gmap_const: autoParam (∀ {α β : Type u} (x : α) (y : m β), Functor.mapConst x y = Function.const β x <\$> y) _auto✝seqLeft_eq: autoParam
(∀ {α β : Type u} (x : m α) (y : m β),
(SeqLeft.seqLeft x fun x => y) = do
let a ← x
let _ ← y
pure a)
_auto✝seqRight_eq: autoParam
(∀ {α β : Type u} (x : m α) (y : m β),
(SeqRight.seqRight x fun x => y) = do
let _ ← x
y)
_auto✝bind_pure_comp: autoParam
(∀ {α β : Type u} (f : α → β) (x : m α),
(do
let y ← x
pure (f y)) =       f <\$> x)
_auto✝bind_map: autoParam
(∀ {α β : Type u} (f : m (α → β)) (x : m α),
(do
let x_1 ← f
x_1 <\$> x) =       Seq.seq f fun x_1 => x)
_auto✝map_pure: ∀ {α β : Type u} (g : α → β) (x : α), g <\$> pure x = pure (g x)α✝, β✝: Type ux: m α✝y: m β✝(do
let _ ← x
y) =   do
let x ← x
let x ← pure (Function.const α✝ id x)
x <\$> y m: Type u → Type vinst✝: Monad mid_map: ∀ {α : Type u} (x : m α), id <\$> x = xpure_bind: ∀ {α β : Type u} (x : α) (f : α → m β), pure x >>= f = f xbind_assoc: ∀ {α β γ : Type u} (x : m α) (f : α → m β) (g : β → m γ), x >>= f >>= g = x >>= fun x => f x >>= gmap_const: autoParam (∀ {α β : Type u} (x : α) (y : m β), Functor.mapConst x y = Function.const β x <\$> y) _auto✝seqLeft_eq: autoParam
(∀ {α β : Type u} (x : m α) (y : m β),
(SeqLeft.seqLeft x fun x => y) = do
let a ← x
let _ ← y
pure a)
_auto✝seqRight_eq: autoParam
(∀ {α β : Type u} (x : m α) (y : m β),
(SeqRight.seqRight x fun x => y) = do
let _ ← x
y)
_auto✝bind_pure_comp: autoParam
(∀ {α β : Type u} (f : α → β) (x : m α),
(do
let y ← x
pure (f y)) =       f <\$> x)
_auto✝bind_map: autoParam
(∀ {α β : Type u} (f : m (α → β)) (x : m α),
(do
let x_1 ← f
x_1 <\$> x) =       Seq.seq f fun x_1 => x)
_auto✝map_pure: ∀ {α β : Type u} (g : α → β) (x : α), g <\$> pure x = pure (g x)α✝, β✝: Type ux: m α✝y: m β✝(SeqRight.seqRight x fun x => y) = Seq.seq (Function.const α✝ id <\$> x) fun x => ysimp [pure_bind: ∀ {α β : Type u} (x : α) (f : α → m β), pure x >>= f = f xpure_bind, id_map: ∀ {α : Type u} (x : m α), id <\$> x = xid_map]Goals accomplished! 🐙 }

instance: ∀ {ε : Type u_1}, LawfulMonad (Except ε)instance : LawfulMonad: (m : Type ?u.11294 → Type ?u.11293) → [inst : Monad m] → PropLawfulMonad (Except: Type ?u.11296 → Type ?u.11295 → Type (max?u.11296?u.11295)Except ε: ?m.11290ε) := LawfulMonad.mk': ∀ (m : Type ?u.11315 → Type ?u.11314) [inst : Monad m],
(∀ {α : Type ?u.11315} (x : m α), id <\$> x = x) →
(∀ {α β : Type ?u.11315} (x : α) (f : α → m β), pure x >>= f = f x) →
(∀ {α β γ : Type ?u.11315} (x : m α) (f : α → m β) (g : β → m γ), x >>= f >>= g = x >>= fun x => f x >>= g) →
autoParam (∀ {α β : Type ?u.11315} (x : α) (y : m β), Functor.mapConst x y = Function.const β x <\$> y) _auto✝ →
autoParam
(∀ {α β : Type ?u.11315} (x : m α) (y : m β),
(SeqLeft.seqLeft x fun x => y) = do
let a ← x
let _ ← y
pure a)
_auto✝¹ →
autoParam
(∀ {α β : Type ?u.11315} (x : m α) (y : m β),
(SeqRight.seqRight x fun x => y) = do
let _ ← x
y)
_auto✝² →
autoParam
(∀ {α β : Type ?u.11315} (f : α → β) (x : m α),
(do
let y ← x
pure (f y)) =                       f <\$> x)
_auto✝³ →
autoParam
(∀ {α β : Type ?u.11315} (f : m (α → β)) (x : m α),
(do
let x_1 ← f
x_1 <\$> x) =                         Seq.seq f fun x_1 => x)
_auto✝⁴ →
(id_map := fun x: ?m.11374x => byGoals accomplished! 🐙 ε: Type ?u.11296α✝: Type ?u.11295x: Except ε α✝id <\$> x = xcases x: Except ε α✝xε: Type ?u.11296α✝: Type ?u.11295a✝: εerrorid <\$> Except.error a✝ = Except.error a✝ε: Type ?u.11296α✝: Type ?u.11295a✝: α✝okid <\$> Except.ok a✝ = Except.ok a✝ ε: Type ?u.11296α✝: Type ?u.11295x: Except ε α✝id <\$> x = x<;>ε: Type ?u.11296α✝: Type ?u.11295a✝: εerrorid <\$> Except.error a✝ = Except.error a✝ε: Type ?u.11296α✝: Type ?u.11295a✝: α✝okid <\$> Except.ok a✝ = Except.ok a✝ ε: Type ?u.11296α✝: Type ?u.11295x: Except ε α✝id <\$> x = xrflGoals accomplished! 🐙)
(pure_bind := fun a: ?m.11391a f: ?m.11394f => rfl: ∀ {α : Sort ?u.11397} {a : α}, a = arfl)
(bind_assoc := fun a: ?m.11453a f: ?m.11456f g: ?m.11460g => byGoals accomplished! 🐙 ε: Type ?u.11296α✝, β✝, γ✝: Type ?u.11295a: Except ε α✝f: α✝ → Except ε β✝g: β✝ → Except ε γ✝a >>= f >>= g = a >>= fun x => f x >>= gcases a: Except ε α✝aε: Type ?u.11296α✝, β✝, γ✝: Type ?u.11295f: α✝ → Except ε β✝g: β✝ → Except ε γ✝a✝: εerrorExcept.error a✝ >>= f >>= g = Except.error a✝ >>= fun x => f x >>= gε: Type ?u.11296α✝, β✝, γ✝: Type ?u.11295f: α✝ → Except ε β✝g: β✝ → Except ε γ✝a✝: α✝okExcept.ok a✝ >>= f >>= g = Except.ok a✝ >>= fun x => f x >>= g ε: Type ?u.11296α✝, β✝, γ✝: Type ?u.11295a: Except ε α✝f: α✝ → Except ε β✝g: β✝ → Except ε γ✝a >>= f >>= g = a >>= fun x => f x >>= g<;>ε: Type ?u.11296α✝, β✝, γ✝: Type ?u.11295f: α✝ → Except ε β✝g: β✝ → Except ε γ✝a✝: εerrorExcept.error a✝ >>= f >>= g = Except.error a✝ >>= fun x => f x >>= gε: Type ?u.11296α✝, β✝, γ✝: Type ?u.11295f: α✝ → Except ε β✝g: β✝ → Except ε γ✝a✝: α✝okExcept.ok a✝ >>= f >>= g = Except.ok a✝ >>= fun x => f x >>= g ε: Type ?u.11296α✝, β✝, γ✝: Type ?u.11295a: Except ε α✝f: α✝ → Except ε β✝g: β✝ → Except ε γ✝a >>= f >>= g = a >>= fun x => f x >>= grflGoals accomplished! 🐙)

instance: ∀ {ε : Type u_1}, LawfulApplicative (Except ε)instance : LawfulApplicative: (f : Type ?u.11992 → Type ?u.11991) → [inst : Applicative f] → PropLawfulApplicative (Except: Type ?u.11994 → Type ?u.11993 → Type (max?u.11994?u.11993)Except ε: ?m.11988ε) := inferInstance: ∀ {α : Sort ?u.12027} [i : α], αinferInstance
instance: ∀ {ε : Type u_1}, LawfulFunctor (Except ε)instance : LawfulFunctor: (f : Type ?u.12078 → Type ?u.12077) → [inst : Functor f] → PropLawfulFunctor (Except: Type ?u.12080 → Type ?u.12079 → Type (max?u.12080?u.12079)Except ε: ?m.12074ε) := inferInstance: ∀ {α : Sort ?u.12123} [i : α], αinferInstance

instance: LawfulMonad Optioninstance : LawfulMonad: (m : Type ?u.12180 → Type ?u.12179) → [inst : Monad m] → PropLawfulMonad Option: Type ?u.12181 → Type ?u.12181Option := LawfulMonad.mk': ∀ (m : Type ?u.12194 → Type ?u.12193) [inst : Monad m],
(∀ {α : Type ?u.12194} (x : m α), id <\$> x = x) →
(∀ {α β : Type ?u.12194} (x : α) (f : α → m β), pure x >>= f = f x) →
(∀ {α β γ : Type ?u.12194} (x : m α) (f : α → m β) (g : β → m γ), x >>= f >>= g = x >>= fun x => f x >>= g) →
autoParam (∀ {α β : Type ?u.12194} (x : α) (y : m β), Functor.mapConst x y = Function.const β x <\$> y) _auto✝ →
autoParam
(∀ {α β : Type ?u.12194} (x : m α) (y : m β),
(SeqLeft.seqLeft x fun x => y) = do
let a ← x
let _ ← y
pure a)
_auto✝¹ →
autoParam
(∀ {α β : Type ?u.12194} (x : m α) (y : m β),
(SeqRight.seqRight x fun x => y) = do
let _ ← x
y)
_auto✝² →
autoParam
(∀ {α β : Type ?u.12194} (f : α → β) (x : m α),
(do
let y ← x
pure (f y)) =                       f <\$> x)
_auto✝³ →
autoParam
(∀ {α β : Type ?u.12194} (f : m (α → β)) (x : m α),
(do
let x_1 ← f
x_1 <\$> x) =                         Seq.seq f fun x_1 => x)
_auto✝⁴ →
(id_map := fun x: ?m.12253x => byGoals accomplished! 🐙 α✝: Type ?u.12181x: Option α✝id <\$> x = xcases x: Option α✝xα✝: Type ?u.12181noneid <\$> none = noneα✝: Type ?u.12181val✝: α✝someid <\$> some val✝ = some val✝ α✝: Type ?u.12181x: Option α✝id <\$> x = x<;>α✝: Type ?u.12181noneid <\$> none = noneα✝: Type ?u.12181val✝: α✝someid <\$> some val✝ = some val✝ α✝: Type ?u.12181x: Option α✝id <\$> x = xrflGoals accomplished! 🐙)
(pure_bind := fun x: ?m.12270x f: ?m.12273f => rfl: ∀ {α : Sort ?u.12276} {a : α}, a = arfl)
(bind_assoc := fun x: ?m.12333x f: ?m.12336f g: ?m.12340g => byGoals accomplished! 🐙 α✝, β✝, γ✝: Type ?u.12181x: Option α✝f: α✝ → Option β✝g: β✝ → Option γ✝x >>= f >>= g = x >>= fun x => f x >>= gcases x: Option α✝xα✝, β✝, γ✝: Type ?u.12181f: α✝ → Option β✝g: β✝ → Option γ✝nonenone >>= f >>= g = none >>= fun x => f x >>= gα✝, β✝, γ✝: Type ?u.12181f: α✝ → Option β✝g: β✝ → Option γ✝val✝: α✝somesome val✝ >>= f >>= g = some val✝ >>= fun x => f x >>= g α✝, β✝, γ✝: Type ?u.12181x: Option α✝f: α✝ → Option β✝g: β✝ → Option γ✝x >>= f >>= g = x >>= fun x => f x >>= g<;>α✝, β✝, γ✝: Type ?u.12181f: α✝ → Option β✝g: β✝ → Option γ✝nonenone >>= f >>= g = none >>= fun x => f x >>= gα✝, β✝, γ✝: Type ?u.12181f: α✝ → Option β✝g: β✝ → Option γ✝val✝: α✝somesome val✝ >>= f >>= g = some val✝ >>= fun x => f x >>= g α✝, β✝, γ✝: Type ?u.12181x: Option α✝f: α✝ → Option β✝g: β✝ → Option γ✝x >>= f >>= g = x >>= fun x => f x >>= grflGoals accomplished! 🐙)
(bind_pure_comp := fun f: ?m.12374f x: ?m.12378x => byGoals accomplished! 🐙 α✝, β✝: Type ?u.12181f: α✝ → β✝x: Option α✝(do
let y ← x
pure (f y)) =   f <\$> xcases x: Option α✝xα✝, β✝: Type ?u.12181f: α✝ → β✝none(do
let y ← none
pure (f y)) =   f <\$> noneα✝, β✝: Type ?u.12181f: α✝ → β✝val✝: α✝some(do
let y ← some val✝
pure (f y)) =   f <\$> some val✝ α✝, β✝: Type ?u.12181f: α✝ → β✝x: Option α✝(do
let y ← x
pure (f y)) =   f <\$> x<;>α✝, β✝: Type ?u.12181f: α✝ → β✝none(do
let y ← none
pure (f y)) =   f <\$> noneα✝, β✝: Type ?u.12181f: α✝ → β✝val✝: α✝some(do
let y ← some val✝
pure (f y)) =   f <\$> some val✝ α✝, β✝: Type ?u.12181f: α✝ → β✝x: Option α✝(do
let y ← x
pure (f y)) =   f <\$> xrflGoals accomplished! 🐙)

instance: LawfulApplicative Optioninstance : LawfulApplicative: (f : Type ?u.12934 → Type ?u.12933) → [inst : Applicative f] → PropLawfulApplicative Option: Type ?u.12935 → Type ?u.12935Option := inferInstance: ∀ {α : Sort ?u.12958} [i : α], αinferInstance
instance: LawfulFunctor Optioninstance : LawfulFunctor: (f : Type ?u.12992 → Type ?u.12991) → [inst : Functor f] → PropLawfulFunctor Option: Type ?u.12993 → Type ?u.12993Option := inferInstance: ∀ {α : Sort ?u.13007} [i : α], αinferInstance

/-!
## SatisfiesM

The `SatisfiesM` predicate works over an arbitrary (lawful) monad / applicative / functor,
and enables Hoare-like reasoning over monadic expressions. For example, given a monadic
function `f : α → m β`, to say that the return value of `f` satisfies `Q` whenever
the input satisfies `P`, we write `∀ a, P a → SatisfiesM Q (f a)`.
-/

/--
`SatisfiesM p (x : m α)` lifts propositions over a monad. It asserts that `x` may as well
have the type `x : m {a // p a}`, because there exists some `m {a // p a}` whose image is `x`.
So `p` is the postcondition of the monadic value.
-/
def SatisfiesM: {α : Type u} → {m : Type u → Type v} → [inst : Functor m] → (α → Prop) → m α → PropSatisfiesM {m: Type u → Type vm : Type u: Type (u+1)Type u → Type v: Type (v+1)Type v} [Functor: (Type ?u.13058 → Type ?u.13057) → Type (max(?u.13058+1)?u.13057)Functor m: Type u → Type vm] (p: α → Propp : α: ?m.13066α → Prop: TypeProp) (x: m αx : m: Type u → Type vm α: ?m.13066α) : Prop: TypeProp :=
∃ x': m { a // p a }x' : m: Type u → Type vm {a: ?m.13098a // p: α → Propp a: ?m.13098a}, Subtype.val: {α : Sort ?u.13110} → {p : α → Prop} → Subtype p → αSubtype.val <\$> x': m { a // p a }x' = x: m αx

namespace SatisfiesM

/-- If `p` is always true, then every `x` satisfies it. -/
theorem of_true: ∀ {m : Type u_1 → Type u_2} {α : Type u_1} {p : α → Prop} [inst : Applicative m] [inst_1 : LawfulApplicative m]
{x : m α}, (∀ (a : α), p a) → SatisfiesM p xof_true [Applicative: (Type ?u.13156 → Type ?u.13155) → Type (max(?u.13156+1)?u.13155)Applicative m: ?m.13152m] [LawfulApplicative: (f : Type ?u.13185 → Type ?u.13184) → [inst : Applicative f] → PropLawfulApplicative m: ?m.13152m] {x: m αx : m: ?m.13152m α: ?m.13176α}
(h: ∀ (a : ?m.13232), ?m.13236 ah : ∀ a: ?m.13232a, p: ?m.13206p a: ?m.13232a) : SatisfiesM: {α : Type ?u.13240} → {m : Type ?u.13240 → Type ?u.13239} → [inst : Functor m] → (α → Prop) → m α → PropSatisfiesM p: ?m.13206p x: m αx :=
⟨(fun a: ?m.13318a => ⟨a: ?m.13318a, h: ∀ (a : α), p ah a: ?m.13318a⟩) <\$> x: m αx, byGoals accomplished! 🐙 m: Type u_1 → Type u_2α: Type u_1p: α → Propinst✝¹: Applicative minst✝: LawfulApplicative mx: m αh: ∀ (a : α), p aSubtype.val <\$> (fun a => { val := a, property := (_ : p a) }) <\$> x = xsimp [← comp_map: ∀ {f : Type ?u.13355 → Type ?u.13354} [inst : Functor f] [self : LawfulFunctor f] {α β γ : Type ?u.13355} (g : α → β)
(h : β → γ) (x : f α), (h ∘ g) <\$> x = h <\$> g <\$> xcomp_map, Function.comp: {α : Sort ?u.13394} → {β : Sort ?u.13393} → {δ : Sort ?u.13392} → (β → δ) → (α → β) → α → δFunction.comp]Goals accomplished! 🐙⟩

/--
If `p` is always true, then every `x` satisfies it.
(This is the strongest postcondition version of `of_true`.)
-/
protected theorem trivial: ∀ {m : Type u_1 → Type u_2} {α : Type u_1} [inst : Applicative m] [inst_1 : LawfulApplicative m] {x : m α},
SatisfiesM (fun x => True) xtrivial [Applicative: (Type ?u.13890 → Type ?u.13889) → Type (max(?u.13890+1)?u.13889)Applicative m: ?m.13862m] [LawfulApplicative: (f : Type ?u.13895 → Type ?u.13894) → [inst : Applicative f] → PropLawfulApplicative m: ?m.13862m] {x: m αx : m: ?m.13862m α: ?m.13886α} :
SatisfiesM: {α : Type ?u.13912} → {m : Type ?u.13912 → Type ?u.13911} → [inst : Functor m] → (α → Prop) → m α → PropSatisfiesM (fun _: ?m.13926_ => True: PropTrue) x: m αx := of_true: ∀ {m : Type ?u.13957 → Type ?u.13958} {α : Type ?u.13957} {p : α → Prop} [inst : Applicative m]
[inst_1 : LawfulApplicative m] {x : m α}, (∀ (a : α), p a) → SatisfiesM p xof_true fun _: ?m.14001_ => trivial: Truetrivial

/-- The `SatisfiesM p x` predicate is monotonic in `p`. -/
theorem imp: ∀ {m : Type u_1 → Type u_2} {α : Type u_1} {p q : α → Prop} [inst : Functor m] [inst_1 : LawfulFunctor m] {x : m α},
SatisfiesM p x → (∀ {a : α}, p a → q a) → SatisfiesM q ximp [Functor: (Type ?u.14027 → Type ?u.14026) → Type (max(?u.14027+1)?u.14026)Functor m: ?m.14023m] [LawfulFunctor: (f : Type ?u.14145 → Type ?u.14144) → [inst : Functor f] → PropLawfulFunctor m: ?m.14023m] {x: m αx : m: ?m.14023m α: ?m.14045α}
(h: SatisfiesM p xh : SatisfiesM: {α : Type ?u.14160} → {m : Type ?u.14160 → Type ?u.14159} → [inst : Functor m] → (α → Prop) → m α → PropSatisfiesM p: ?m.14083p x: m αx) (H: ∀ {a : α}, p a → q aH : ∀ {a: ?m.14183a}, p: ?m.14083p a: ?m.14183a → q: ?m.14136q a: ?m.14183a) : SatisfiesM: {α : Type ?u.14193} → {m : Type ?u.14193 → Type ?u.14192} → [inst : Functor m] → (α → Prop) → m α → PropSatisfiesM q: ?m.14136q x: m αx :=
let ⟨x: m { a // p a }x, h: Subtype.val <\$> x = x✝h⟩ := h: SatisfiesM p xh; ⟨(fun ⟨a: αa, h: p ah⟩ => ⟨_: ?m.14344_, H: ∀ {a : α}, p a → q aH h: p ah⟩) <\$> x: m { a // p a }x, byGoals accomplished! 🐙 m: Type u_1 → Type u_2α: Type u_1p, q: α → Propinst✝¹: Functor minst✝: LawfulFunctor mx✝: m αh✝: SatisfiesM p x✝H: ∀ {a : α}, p a → q ax: m { a // p a }h: Subtype.val <\$> x = x✝Subtype.val <\$>     (fun x =>
match x with
| { val := a, property := h } => { val := a, property := (_ : q a) }) <\$>       x =   x✝rw [m: Type u_1 → Type u_2α: Type u_1p, q: α → Propinst✝¹: Functor minst✝: LawfulFunctor mx✝: m αh✝: SatisfiesM p x✝H: ∀ {a : α}, p a → q ax: m { a // p a }h: Subtype.val <\$> x = x✝Subtype.val <\$>     (fun x =>
match x with
| { val := a, property := h } => { val := a, property := (_ : q a) }) <\$>       x =   x✝← h: Subtype.val <\$> x = x✝h,m: Type u_1 → Type u_2α: Type u_1p, q: α → Propinst✝¹: Functor minst✝: LawfulFunctor mx✝: m αh✝: SatisfiesM p x✝H: ∀ {a : α}, p a → q ax: m { a // p a }h: Subtype.val <\$> x = x✝Subtype.val <\$>     (fun x =>
match x with
| { val := a, property := h } => { val := a, property := (_ : q a) }) <\$>       x =   Subtype.val <\$> x m: Type u_1 → Type u_2α: Type u_1p, q: α → Propinst✝¹: Functor minst✝: LawfulFunctor mx✝: m αh✝: SatisfiesM p x✝H: ∀ {a : α}, p a → q ax: m { a // p a }h: Subtype.val <\$> x = x✝Subtype.val <\$>     (fun x =>
match x with
| { val := a, property := h } => { val := a, property := (_ : q a) }) <\$>       x =   x✝← comp_map: ∀ {f : Type ?u.14512 → Type ?u.14511} [inst : Functor f] [self : LawfulFunctor f] {α β γ : Type ?u.14512} (g : α → β)
(h : β → γ) (x : f α), (h ∘ g) <\$> x = h <\$> g <\$> xcomp_mapm: Type u_1 → Type u_2α: Type u_1p, q: α → Propinst✝¹: Functor minst✝: LawfulFunctor mx✝: m αh✝: SatisfiesM p x✝H: ∀ {a : α}, p a → q ax: m { a // p a }h: Subtype.val <\$> x = x✝(Subtype.val ∘ fun x =>
match x with
| { val := a, property := h } => { val := a, property := (_ : q a) }) <\$>     x =   Subtype.val <\$> x]m: Type u_1 → Type u_2α: Type u_1p, q: α → Propinst✝¹: Functor minst✝: LawfulFunctor mx✝: m αh✝: SatisfiesM p x✝H: ∀ {a : α}, p a → q ax: m { a // p a }h: Subtype.val <\$> x = x✝(Subtype.val ∘ fun x =>
match x with
| { val := a, property := h } => { val := a, property := (_ : q a) }) <\$>     x =   Subtype.val <\$> x;m: Type u_1 → Type u_2α: Type u_1p, q: α → Propinst✝¹: Functor minst✝: LawfulFunctor mx✝: m αh✝: SatisfiesM p x✝H: ∀ {a : α}, p a → q ax: m { a // p a }h: Subtype.val <\$> x = x✝(Subtype.val ∘ fun x =>
match x with
| { val := a, property := h } => { val := a, property := (_ : q a) }) <\$>     x =   Subtype.val <\$> x m: Type u_1 → Type u_2α: Type u_1p, q: α → Propinst✝¹: Functor minst✝: LawfulFunctor mx✝: m αh✝: SatisfiesM p x✝H: ∀ {a : α}, p a → q ax: m { a // p a }h: Subtype.val <\$> x = x✝Subtype.val <\$>     (fun x =>
match x with
| { val := a, property := h } => { val := a, property := (_ : q a) }) <\$>       x =   x✝rflGoals accomplished! 🐙⟩

/-- `SatisfiesM` distributes over `<\$>`, general version. -/
protected theorem map: ∀ {m : Type u_1 → Type u_2} {α : Type u_1} {p : α → Prop} {α_1 : Type u_1} {q : α_1 → Prop} {f : α → α_1}
[inst : Functor m] [inst_1 : LawfulFunctor m] {x : m α},
SatisfiesM p x → (∀ {a : α}, p a → q (f a)) → SatisfiesM q (f <\$> x)map [Functor: (Type ?u.14764 → Type ?u.14763) → Type (max(?u.14764+1)?u.14763)Functor m: ?m.14647m] [LawfulFunctor: (f : Type ?u.14860 → Type ?u.14859) → [inst : Functor f] → PropLawfulFunctor m: ?m.14647m] {x: m αx : m: ?m.14647m α: ?m.14669α}
(hx: SatisfiesM p xhx : SatisfiesM: {α : Type ?u.14731} → {m : Type ?u.14731 → Type ?u.14730} → [inst : Functor m] → (α → Prop) → m α → PropSatisfiesM p: ?m.14707p x: m αx) (hf: ∀ {a : α}, p a → ?m.14904hf : ∀ {a: ?m.14898a}, p: ?m.14707p a: unknown metavariable '?_uniq.14807'a → q: ?m.14760q (f: ?m.14851f a: ?m.14898a)) : SatisfiesM: {α : Type ?u.14908} → {m : Type ?u.14908 → Type ?u.14907} → [inst : Functor m] → (α → Prop) → m α → PropSatisfiesM q: ?m.14760q (f: ?m.14851f <\$> x: m αx) := byGoals accomplished! 🐙
m: Type u_1 → Type u_2α: Type u_1p: α → Propα✝: Type u_1q: α✝ → Propf: α → α✝inst✝¹: Functor minst✝: LawfulFunctor mx: m αhx: SatisfiesM p xhf: ∀ {a : α}, p a → q (f a)SatisfiesM q (f <\$> x)let ⟨x': m { a // p a }x', hx: Subtype.val <\$> x' = xhx⟩ := hx: SatisfiesM p xhxm: Type u_1 → Type u_2α: Type u_1p: α → Propα✝: Type u_1q: α✝ → Propf: α → α✝inst✝¹: Functor minst✝: LawfulFunctor mx: m αhx✝: SatisfiesM p xhf: ∀ {a : α}, p a → q (f a)x': m { a // p a }hx: Subtype.val <\$> x' = xSatisfiesM q (f <\$> x)
m: Type u_1 → Type u_2α: Type u_1p: α → Propα✝: Type u_1q: α✝ → Propf: α → α✝inst✝¹: Functor minst✝: LawfulFunctor mx: m αhx: SatisfiesM p xhf: ∀ {a : α}, p a → q (f a)SatisfiesM q (f <\$> x)refine ⟨(fun ⟨a: αa, h: p ah⟩ => ⟨f: α → α✝f a: αa, hf: ∀ {a : α}, p a → q (f a)hf h: p ah⟩) <\$> x': m { a // p a }x', ?_: ?m.15081 ((fun x => ?m.15104 x) <\$> x')?_⟩m: Type u_1 → Type u_2α: Type u_1p: α → Propα✝: Type u_1q: α✝ → Propf: α → α✝inst✝¹: Functor minst✝: LawfulFunctor mx: m αhx✝: SatisfiesM p xhf: ∀ {a : α}, p a → q (f a)x': m { a // p a }hx: Subtype.val <\$> x' = xSubtype.val <\$>     (fun x =>
match x with
| { val := a, property := h } => { val := f a, property := (_ : q (f a)) }) <\$>       x' =   f <\$> x
m: Type u_1 → Type u_2α: Type u_1p: α → Propα✝: Type u_1q: α✝ → Propf: α → α✝inst✝¹: Functor minst✝: LawfulFunctor mx: m αhx: SatisfiesM p xhf: ∀ {a : α}, p a → q (f a)SatisfiesM q (f <\$> x)rw [m: Type u_1 → Type u_2α: Type u_1p: α → Propα✝: Type u_1q: α✝ → Propf: α → α✝inst✝¹: Functor minst✝: LawfulFunctor mx: m αhx✝: SatisfiesM p xhf: ∀ {a : α}, p a → q (f a)x': m { a // p a }hx: Subtype.val <\$> x' = xSubtype.val <\$>     (fun x =>
match x with
| { val := a, property := h } => { val := f a, property := (_ : q (f a)) }) <\$>       x' =   f <\$> x← hx: Subtype.val <\$> x' = xhxm: Type u_1 → Type u_2α: Type u_1p: α → Propα✝: Type u_1q: α✝ → Propf: α → α✝inst✝¹: Functor minst✝: LawfulFunctor mx: m αhx✝: SatisfiesM p xhf: ∀ {a : α}, p a → q (f a)x': m { a // p a }hx: Subtype.val <\$> x' = xSubtype.val <\$>     (fun x =>
match x with
| { val := a, property := h } => { val := f a, property := (_ : q (f a)) }) <\$>       x' =   f <\$> Subtype.val <\$> x']m: Type u_1 → Type u_2α: Type u_1p: α → Propα✝: Type u_1q: α✝ → Propf: α → α✝inst✝¹: Functor minst✝: LawfulFunctor mx: m αhx✝: SatisfiesM p xhf: ∀ {a : α}, p a → q (f a)x': m { a // p a }hx: Subtype.val <\$> x' = xSubtype.val <\$>     (fun x =>
match x with
| { val := a, property := h } => { val := f a, property := (_ : q (f a)) }) <\$>       x' =   f <\$> Subtype.val <\$> x';m: Type u_1 → Type u_2α: Type u_1p: α → Propα✝: Type u_1q: α✝ → Propf: α → α✝inst✝¹: Functor minst✝: LawfulFunctor mx: m αhx✝: SatisfiesM p xhf: ∀ {a : α}, p a → q (f a)x': m { a // p a }hx: Subtype.val <\$> x' = xSubtype.val <\$>     (fun x =>
match x with
| { val := a, property := h } => { val := f a, property := (_ : q (f a)) }) <\$>       x' =   f <\$> Subtype.val <\$> x' m: Type u_1 → Type u_2α: Type u_1p: α → Propα✝: Type u_1q: α✝ → Propf: α → α✝inst✝¹: Functor minst✝: LawfulFunctor mx: m αhx: SatisfiesM p xhf: ∀ {a : α}, p a → q (f a)SatisfiesM q (f <\$> x)simp [← comp_map: ∀ {f : Type ?u.15239 → Type ?u.15238} [inst : Functor f] [self : LawfulFunctor f] {α β γ : Type ?u.15239} (g : α → β)
(h : β → γ) (x : f α), (h ∘ g) <\$> x = h <\$> g <\$> xcomp_map, Function.comp: {α : Sort ?u.15278} → {β : Sort ?u.15277} → {δ : Sort ?u.15276} → (β → δ) → (α → β) → α → δFunction.comp]Goals accomplished! 🐙

/--
`SatisfiesM` distributes over `<\$>`, strongest postcondition version.
(Use this for reasoning forward from assumptions.)
-/
theorem map_post: ∀ {m : Type u_1 → Type u_2} {α : Type u_1} {p : α → Prop} {α_1 : Type u_1} {f : α → α_1} [inst : Functor m]
[inst_1 : LawfulFunctor m] {x : m α}, SatisfiesM p x → SatisfiesM (fun b => ∃ a, p a ∧ b = f a) (f <\$> x)map_post [Functor: (Type ?u.16250 → Type ?u.16249) → Type (max(?u.16250+1)?u.16249)Functor m: ?m.16246m] [LawfulFunctor: (f : Type ?u.16277 → Type ?u.16276) → [inst : Functor f] → PropLawfulFunctor m: ?m.16246m] {x: m αx : m: ?m.16246m α: ?m.16268α}
(hx: SatisfiesM p xhx : SatisfiesM: {α : Type ?u.16400} → {m : Type ?u.16400 → Type ?u.16399} → [inst : Functor m] → (α → Prop) → m α → PropSatisfiesM p: ?m.16306p x: m αx) : SatisfiesM: {α : Type ?u.16423} → {m : Type ?u.16423 → Type ?u.16422} → [inst : Functor m] → (α → Prop) → m α → PropSatisfiesM (fun b: ?m.16437b => ∃ a: ?m.16442a, p: ?m.16306p a: ?m.16442a ∧ b: ?m.16437b = f: ?m.16376f a: ?m.16442a) (f: ?m.16376f <\$> x: m αx) :=
hx: SatisfiesM p xhx.map: ∀ {m : Type ?u.16503 → Type ?u.16504} {α : Type ?u.16503} {p : α → Prop} {α_1 : Type ?u.16503} {q : α_1 → Prop}
{f : α → α_1} [inst : Functor m] [inst_1 : LawfulFunctor m] {x : m α},
SatisfiesM p x → (∀ {a : α}, p a → q (f a)) → SatisfiesM q (f <\$> x)map fun h: ?m.16558h => ⟨_: ?m.16565_, h: ?m.16558h, rfl: ∀ {α : Sort ?u.16582} {a : α}, a = arfl⟩

/--
`SatisfiesM` distributes over `<\$>`, weakest precondition version.
(Use this for reasoning backward from the goal.)
-/
theorem map_pre: ∀ {m : Type u_1 → Type u_2} {α α_1 : Type u_1} {p : α_1 → Prop} {f : α → α_1} [inst : Functor m]
[inst_1 : LawfulFunctor m] {x : m α}, SatisfiesM (fun a => p (f a)) x → SatisfiesM p (f <\$> x)map_pre [Functor: (Type ?u.16682 → Type ?u.16681) → Type (max(?u.16682+1)?u.16681)Functor m: ?m.16615m] [LawfulFunctor: (f : Type ?u.16687 → Type ?u.16686) → [inst : Functor f] → PropLawfulFunctor m: ?m.16615m] {x: m αx : m: ?m.16615m α: ?m.16637α}
(hx: SatisfiesM (fun a => ?m.16803 a) xhx : SatisfiesM: {α : Type ?u.16786} → {m : Type ?u.16786 → Type ?u.16785} → [inst : Functor m] → (α → Prop) → m α → PropSatisfiesM (fun a: ?m.16800a => p: ?m.16678p (f: ?m.16762f a: ?m.16800a)) x: m αx) : SatisfiesM: {α : Type ?u.16812} → {m : Type ?u.16812 → Type ?u.16811} → [inst : Functor m] → (α → Prop) → m α → PropSatisfiesM p: ?m.16678p (f: ?m.16762f <\$> x: m αx) :=
hx: SatisfiesM (fun a => p (f a)) xhx.map: ∀ {m : Type ?u.16874 → Type ?u.16875} {α : Type ?u.16874} {p : α → Prop} {α_1 : Type ?u.16874} {q : α_1 → Prop}
{f : α → α_1} [inst : Functor m] [inst_1 : LawfulFunctor m] {x : m α},
SatisfiesM p x → (∀ {a : α}, p a → q (f a)) → SatisfiesM q (f <\$> x)map fun h: ?m.16929h => h: ?m.16929h

/-- `SatisfiesM` distributes over `mapConst`, general version. -/
protected theorem mapConst: ∀ {m : Type u_1 → Type u_2} {α : Type u_1} {q : α → Prop} {α_1 : Type u_1} {p : α_1 → Prop} {a : α_1} [inst : Functor m]
[inst_1 : LawfulFunctor m] {x : m α}, SatisfiesM q x → (∀ {b : α}, q b → p a) → SatisfiesM p (Functor.mapConst a x)mapConst [Functor: (Type ?u.17073 → Type ?u.17072) → Type (max(?u.17073+1)?u.17072)Functor m: ?m.16956m] [LawfulFunctor: (f : Type ?u.17025 → Type ?u.17024) → [inst : Functor f] → PropLawfulFunctor m: ?m.16956m] {x: m αx : m: ?m.16956m α: ?m.16978α}
(hx: SatisfiesM q xhx : SatisfiesM: {α : Type ?u.17040} → {m : Type ?u.17040 → Type ?u.17039} → [inst : Functor m] → (α → Prop) → m α → PropSatisfiesM q: ?m.17016q x: m αx) (ha: ∀ {b : α}, q b → ?m.17213ha : ∀ {b: ?m.17207b}, q: ?m.17016q b: unknown metavariable '?_uniq.17116'b → p: ?m.17069p a: ?m.17160a) : SatisfiesM: {α : Type ?u.17217} → {m : Type ?u.17217 → Type ?u.17216} → [inst : Functor m] → (α → Prop) → m α → PropSatisfiesM p: ?m.17069p (Functor.mapConst: {f : Type ?u.17234 → Type ?u.17233} → [self : Functor f] → {α β : Type ?u.17234} → α → f β → f αFunctor.mapConst a: ?m.17160a x: m αx) :=
map_const: ∀ {f : Type ?u.17283 → Type ?u.17282} [inst : Functor f] [self : LawfulFunctor f] {α β : Type ?u.17283},
Functor.mapConst = Functor.map ∘ Function.const βmap_const (f := m: Type u_1 → Type u_2m) ▸ hx: SatisfiesM q xhx.map: ∀ {m : Type ?u.17309 → Type ?u.17310} {α : Type ?u.17309} {p : α → Prop} {α_1 : Type ?u.17309} {q : α_1 → Prop}
{f : α → α_1} [inst : Functor m] [inst_1 : LawfulFunctor m] {x : m α},
SatisfiesM p x → (∀ {a : α}, p a → q (f a)) → SatisfiesM q (f <\$> x)map ha: ∀ {b : α}, q b → p aha

/-- `SatisfiesM` distributes over `pure`, general version / weakest precondition version. -/
protected theorem pure: ∀ {m : Type u_1 → Type u_2} {α : Type u_1} {p : α → Prop} {a : α} [inst : Applicative m] [inst_1 : LawfulApplicative m],
p a → SatisfiesM p (pure a)pure [Applicative: (Type ?u.17498 → Type ?u.17497) → Type (max(?u.17498+1)?u.17497)Applicative m: ?m.17411m] [LawfulApplicative: (f : Type ?u.17420 → Type ?u.17419) → [inst : Applicative f] → PropLawfulApplicative m: ?m.17411m]
(h: unknown metavariable '?_uniq.17458'h : p: ?m.17435p a: ?m.17494a) : SatisfiesM: {α : Type ?u.17521} → {m : Type ?u.17521 → Type ?u.17520} → [inst : Functor m] → (α → Prop) → m α → PropSatisfiesM (m := m: ?m.17411m) p: ?m.17435p (pure: {f : Type ?u.17531 → Type ?u.17530} → [self : Pure f] → {α : Type ?u.17531} → α → f αpure a: ?m.17494a) := ⟨pure: {f : Type ?u.17615 → Type ?u.17614} → [self : Pure f] → {α : Type ?u.17615} → α → f αpure ⟨_: ?m.17641_, h: p ah⟩, byGoals accomplished! 🐙 m: Type u_1 → Type u_2α✝: Type u_1p: α✝ → Propa: α✝inst✝¹: Applicative minst✝: LawfulApplicative mh: p aSubtype.val <\$> pure { val := a, property := h } = pure asimpGoals accomplished! 🐙⟩

/-- `SatisfiesM` distributes over `<*>`, general version. -/
protected theorem seq: ∀ {m : Type u_1 → Type u_2} {α α_1 : Type u_1} {p₁ : (α → α_1) → Prop} {f : m (α → α_1)} {p₂ : α → Prop}
{q : α_1 → Prop} [inst : Applicative m] [inst_1 : LawfulApplicative m] {x : m α},
SatisfiesM p₁ f →
SatisfiesM p₂ x → (∀ {f : α → α_1} {a : α}, p₁ f → p₂ a → q (f a)) → SatisfiesM q (Seq.seq f fun x_1 => x)seq [Applicative: (Type ?u.18028 → Type ?u.18027) → Type (max(?u.18028+1)?u.18027)Applicative m: ?m.17917m] [LawfulApplicative: (f : Type ?u.17950 → Type ?u.17949) → [inst : Applicative f] → PropLawfulApplicative m: ?m.17917m] {x: m αx : m: ?m.17917m α: ?m.17941α}
(hf: SatisfiesM p₁ fhf : SatisfiesM: {α : Type ?u.18232} → {m : Type ?u.18232 → Type ?u.18231} → [inst : Functor m] → (α → Prop) → m α → PropSatisfiesM p₁: ?m.17981p₁ f: ?m.18024f) (hx: SatisfiesM p₂ xhx : SatisfiesM: {α : Type ?u.18266} → {m : Type ?u.18266 → Type ?u.18265} → [inst : Functor m] → (α → Prop) → m α → PropSatisfiesM p₂: ?m.18098p₂ x: m αx)
(H: ∀ {f : ?m.18309} {a : α}, p₁ f → p₂ a → ?m.18314H : ∀ {f: ?m.18302f a: ?m.18305a}, p₁: ?m.17981p₁ f: ?m.18302f → p₂: ?m.18098p₂ a: ?m.18305a → q: ?m.18206q (f: ?m.18302f a: ?m.18305a)) : SatisfiesM: {α : Type ?u.18318} → {m : Type ?u.18318 → Type ?u.18317} → [inst : Functor m] → (α → Prop) → m α → PropSatisfiesM q: ?m.18206q (f: ?m.18024f <*> x: m αx) := byGoals accomplished! 🐙
m: Type u_1 → Type u_2α, α✝: Type u_1p₁: (α → α✝) → Propf: m (α → α✝)p₂: α → Propq: α✝ → Propinst✝¹: Applicative minst✝: LawfulApplicative mx: m αhf: SatisfiesM p₁ fhx: SatisfiesM p₂ xH: ∀ {f : α → α✝} {a : α}, p₁ f → p₂ a → q (f a)SatisfiesM q (Seq.seq f fun x_1 => x)match f: m (α → α✝)f, x: m αx, hf: SatisfiesM p₁ fhf, hx: SatisfiesM p₂ xhx with | _, _, ⟨f: m { a // p₁ a }f, rfl: ∀ {α : Sort ?u.18428} {a : α}, a = arfl⟩, ⟨x: m { a // p₂ a }x, rfl: ∀ {α : Sort ?u.18432} {a : α}, a = arfl⟩ => ?_: SatisfiesM q (Seq.seq (Subtype.val <\$> f) fun x_1 => Subtype.val <\$> x)?_m: Type u_1 → Type u_2α, α✝: Type u_1p₁: (α → α✝) → Propf✝: m (α → α✝)p₂: α → Propq: α✝ → Propinst✝¹: Applicative minst✝: LawfulApplicative mx✝: m αhf: SatisfiesM p₁ f✝hx: SatisfiesM p₂ x✝H: ∀ {f : α → α✝} {a : α}, p₁ f → p₂ a → q (f a)f: m { a // p₁ a }x: m { a // p₂ a }SatisfiesM q (Seq.seq (Subtype.val <\$> f) fun x_1 => Subtype.val <\$> x)
m: Type u_1 → Type u_2α, α✝: Type u_1p₁: (α → α✝) → Propf: m (α → α✝)p₂: α → Propq: α✝ → Propinst✝¹: Applicative minst✝: LawfulApplicative mx: m αhf: SatisfiesM p₁ fhx: SatisfiesM p₂ xH: ∀ {f : α → α✝} {a : α}, p₁ f → p₂ a → q (f a)SatisfiesM q (Seq.seq f fun x_1 => x)refine ⟨(fun ⟨a: α → α✝a, h₁: p₁ ah₁⟩ ⟨b: αb, h₂: p₂ bh₂⟩ => ⟨a: α → α✝a b: αb, H: ∀ {f : α → α✝} {a : α}, p₁ f → p₂ a → q (f a)H h₁: p₁ ah₁ h₂: p₂ bh₂⟩) <\$> f: m { a // p₁ a }f <*> x: m { a // p₂ a }x, ?_: ?m.18906 (Seq.seq ((fun x x_1 => ?m.18959 x x_1) <\$> f) fun x_1 => x)?_⟩m: Type u_1 → Type u_2α, α✝: Type u_1p₁: (α → α✝) → Propf✝: m (α → α✝)p₂: α → Propq: α✝ → Propinst✝¹: Applicative minst✝: LawfulApplicative mx✝: m αhf: SatisfiesM p₁ f✝hx: SatisfiesM p₂ x✝H: ∀ {f : α → α✝} {a : α}, p₁ f → p₂ a → q (f a)f: m { a // p₁ a }x: m { a // p₂ a }(Subtype.val <\$>     Seq.seq
((fun x x_1 =>
match x with
| { val := a, property := h₁ } =>
match x_1 with
| { val := b, property := h₂ } => { val := a b, property := (_ : q (a b)) }) <\$>         f)
fun x_1 => x) =   Seq.seq (Subtype.val <\$> f) fun x_1 => Subtype.val <\$> x
m: Type u_1 → Type u_2α, α✝: Type u_1p₁: (α → α✝) → Propf: m (α → α✝)p₂: α → Propq: α✝ → Propinst✝¹: Applicative minst✝: LawfulApplicative mx: m αhf: SatisfiesM p₁ fhx: SatisfiesM p₂ xH: ∀ {f : α → α✝} {a : α}, p₁ f → p₂ a → q (f a)SatisfiesM q (Seq.seq f fun x_1 => x)simp only [← pure_seq: ∀ {f : Type ?u.19222 → Type ?u.19221} [inst : Applicative f] [self : LawfulApplicative f] {α β : Type ?u.19222}
(g : α → β) (x : f α), (Seq.seq (pure g) fun x_1 => x) = g <\$> xpure_seq]m: Type u_1 → Type u_2α, α✝: Type u_1p₁: (α → α✝) → Propf✝: m (α → α✝)p₂: α → Propq: α✝ → Propinst✝¹: Applicative minst✝: LawfulApplicative mx✝: m αhf: SatisfiesM p₁ f✝hx: SatisfiesM p₂ x✝H: ∀ {f : α → α✝} {a : α}, p₁ f → p₂ a → q (f a)f: m { a // p₁ a }x: m { a // p₂ a }(Seq.seq (pure Subtype.val) fun x_1 =>
Seq.seq
(Seq.seq (pure fun x x_2 => { val := Subtype.val x x_2.val, property := (_ : q (Subtype.val x x_2.val)) })
fun x => f)
fun x_2 => x) =   Seq.seq (Seq.seq (pure Subtype.val) fun x => f) fun x_1 => Seq.seq (pure Subtype.val) fun x_2 => x;m: Type u_1 → Type u_2α, α✝: Type u_1p₁: (α → α✝) → Propf✝: m (α → α✝)p₂: α → Propq: α✝ → Propinst✝¹: Applicative minst✝: LawfulApplicative mx✝: m αhf: SatisfiesM p₁ f✝hx: SatisfiesM p₂ x✝H: ∀ {f : α → α✝} {a : α}, p₁ f → p₂ a → q (f a)f: m { a // p₁ a }x: m { a // p₂ a }(Seq.seq (pure Subtype.val) fun x_1 =>
Seq.seq
(Seq.seq (pure fun x x_2 => { val := Subtype.val x x_2.val, property := (_ : q (Subtype.val x x_2.val)) })
fun x => f)
fun x_2 => x) =   Seq.seq (Seq.seq (pure Subtype.val) fun x => f) fun x_1 => Seq.seq (pure Subtype.val) fun x_2 => x m: Type u_1 → Type u_2α, α✝: Type u_1p₁: (α → α✝) → Propf: m (α → α✝)p₂: α → Propq: α✝ → Propinst✝¹: Applicative minst✝: LawfulApplicative mx: m αhf: SatisfiesM p₁ fhx: SatisfiesM p₂ xH: ∀ {f : α → α✝} {a : α}, p₁ f → p₂ a → q (f a)SatisfiesM q (Seq.seq f fun x_1 => x)simp [SatisfiesM: {α : Type ?u.19634} → {m : Type ?u.19634 → Type ?u.19633} → [inst : Functor m] → (α → Prop) → m α → PropSatisfiesM, seq_assoc: ∀ {f : Type ?u.19637 → Type ?u.19636} [inst : Applicative f] [self : LawfulApplicative f] {α β γ : Type ?u.19637}
(x : f α) (g : f (α → β)) (h : f (β → γ)),
(Seq.seq h fun x_1 => Seq.seq g fun x_2 => x) = Seq.seq (Seq.seq (Function.comp <\$> h) fun x => g) fun x_1 => xseq_assoc]m: Type u_1 → Type u_2α, α✝: Type u_1p₁: (α → α✝) → Propf✝: m (α → α✝)p₂: α → Propq: α✝ → Propinst✝¹: Applicative minst✝: LawfulApplicative mx✝: m αhf: SatisfiesM p₁ f✝hx: SatisfiesM p₂ x✝H: ∀ {f : α → α✝} {a : α}, p₁ f → p₂ a → q (f a)f: m { a // p₁ a }x: m { a // p₂ a }(Seq.seq
(Seq.seq
(pure
(Function.comp Subtype.val ∘ fun x x_1 =>
{ val := Subtype.val x x_1.val, property := (_ : q (Subtype.val x x_1.val)) }))
fun x => f)
fun x_1 => x) =   Seq.seq ((fun h => h Subtype.val) <\$> Function.comp <\$> Seq.seq (pure Subtype.val) fun x => f) fun x_1 => x
m: Type u_1 → Type u_2α, α✝: Type u_1p₁: (α → α✝) → Propf: m (α → α✝)p₂: α → Propq: α✝ → Propinst✝¹: Applicative minst✝: LawfulApplicative mx: m αhf: SatisfiesM p₁ fhx: SatisfiesM p₂ xH: ∀ {f : α → α✝} {a : α}, p₁ f → p₂ a → q (f a)SatisfiesM q (Seq.seq f fun x_1 => x)simp only [← pure_seq: ∀ {f : Type ?u.21890 → Type ?u.21889} [inst : Applicative f] [self : LawfulApplicative f] {α β : Type ?u.21890}
(g : α → β) (x : f α), (Seq.seq (pure g) fun x_1 => x) = g <\$> xpure_seq]m: Type u_1 → Type u_2α, α✝: Type u_1p₁: (α → α✝) → Propf✝: m (α → α✝)p₂: α → Propq: α✝ → Propinst✝¹: Applicative minst✝: LawfulApplicative mx✝: m αhf: SatisfiesM p₁ f✝hx: SatisfiesM p₂ x✝H: ∀ {f : α → α✝} {a : α}, p₁ f → p₂ a → q (f a)f: m { a // p₁ a }x: m { a // p₂ a }(Seq.seq
(Seq.seq
(pure
(Function.comp Subtype.val ∘ fun x x_1 =>
{ val := Subtype.val x x_1.val, property := (_ : q (Subtype.val x x_1.val)) }))
fun x => f)
fun x_1 => x) =   Seq.seq
(Seq.seq (pure fun h => h Subtype.val) fun x =>
Seq.seq (pure Function.comp) fun x => Seq.seq (pure Subtype.val) fun x => f)
fun x_1 => x;m: Type u_1 → Type u_2α, α✝: Type u_1p₁: (α → α✝) → Propf✝: m (α → α✝)p₂: α → Propq: α✝ → Propinst✝¹: Applicative minst✝: LawfulApplicative mx✝: m αhf: SatisfiesM p₁ f✝hx: SatisfiesM p₂ x✝H: ∀ {f : α → α✝} {a : α}, p₁ f → p₂ a → q (f a)f: m { a // p₁ a }x: m { a // p₂ a }(Seq.seq
(Seq.seq
(pure
(Function.comp Subtype.val ∘ fun x x_1 =>
{ val := Subtype.val x x_1.val, property := (_ : q (Subtype.val x x_1.val)) }))
fun x => f)
fun x_1 => x) =   Seq.seq
(Seq.seq (pure fun h => h Subtype.val) fun x =>
Seq.seq (pure Function.comp) fun x => Seq.seq (pure Subtype.val) fun x => f)
fun x_1 => x m: Type u_1 → Type u_2α, α✝: Type u_1p₁: (α → α✝) → Propf: m (α → α✝)p₂: α → Propq: α✝ → Propinst✝¹: Applicative minst✝: LawfulApplicative mx: m αhf: SatisfiesM p₁ fhx: SatisfiesM p₂ xH: ∀ {f : α → α✝} {a : α}, p₁ f → p₂ a → q (f a)SatisfiesM q (Seq.seq f fun x_1 => x)simp [seq_assoc: ∀ {f : Type ?u.22089 → Type ?u.22088} [inst : Applicative f] [self : LawfulApplicative f] {α β γ : Type ?u.22089}
(x : f α) (g : f (α → β)) (h : f (β → γ)),
(Seq.seq h fun x_1 => Seq.seq g fun x_2 => x) = Seq.seq (Seq.seq (Function.comp <\$> h) fun x => g) fun x_1 => xseq_assoc, Function.comp: {α : Sort ?u.22112} → {β : Sort ?u.22111} → {δ : Sort ?u.22110} → (β → δ) → (α → β) → α → δFunction.comp]Goals accomplished! 🐙

/-- `SatisfiesM` distributes over `<*>`, strongest postcondition version. -/
protected theorem seq_post: ∀ {m : Type u_1 → Type u_2} {α α_1 : Type u_1} {p₁ : (α → α_1) → Prop} {f : m (α → α_1)} {p₂ : α → Prop}
[inst : Applicative m] [inst_1 : LawfulApplicative m] {x : m α},
SatisfiesM p₁ f → SatisfiesM p₂ x → SatisfiesM (fun c => ∃ f a, p₁ f ∧ p₂ a ∧ c = f a) (Seq.seq f fun x_1 => x)seq_post [Applicative: (Type ?u.25708 → Type ?u.25707) → Type (max(?u.25708+1)?u.25707)Applicative m: ?m.25597m] [LawfulApplicative: (f : Type ?u.25670 → Type ?u.25669) → [inst : Applicative f] → PropLawfulApplicative m: ?m.25597m] {x: m αx : m: ?m.25597m α: ?m.25621α}
(hf: SatisfiesM p₁ fhf : SatisfiesM: {α : Type ?u.25730} → {m : Type ?u.25730 → Type ?u.25729} → [inst : Functor m] → (α → Prop) → m α → PropSatisfiesM p₁: ?m.25661p₁ f: ?m.25704f) (hx: SatisfiesM p₂ xhx : SatisfiesM: {α : Type ?u.25838} → {m : Type ?u.25838 → Type ?u.25837} → [inst : Functor m] → (α → Prop) → m α → PropSatisfiesM p₂: ?m.25778p₂ x: m αx) :
SatisfiesM: {α : Type ?u.25874} → {m : Type ?u.25874 → Type ?u.25873} → [inst : Functor m] → (α → Prop) → m α → PropSatisfiesM (fun c: ?m.25888c => ∃ f: ?m.25893f a: ?m.25898a, p₁: ?m.25661p₁ f: ?m.25893f ∧ p₂: ?m.25778p₂ a: ?m.25898a ∧ c: ?m.25888c = f: ?m.25893f a: ?m.25898a) (f: ?m.25704f <*> x: m αx) :=
hf: SatisfiesM p₁ fhf.seq: ∀ {m : Type ?u.25998 → Type ?u.25999} {α α_1 : Type ?u.25998} {p₁ : (α → α_1) → Prop} {f : m (α → α_1)} {p₂ : α → Prop}
{q : α_1 → Prop} [inst : Applicative m] [inst_1 : LawfulApplicative m] {x : m α},
SatisfiesM p₁ f →
SatisfiesM p₂ x → (∀ {f : α → α_1} {a : α}, p₁ f → p₂ a → q (f a)) → SatisfiesM q (Seq.seq f fun x_1 => x)seq hx: SatisfiesM p₂ xhx fun  hf: ?m.26060hf ha: ?m.26063ha => ⟨_: ?m.26070_, _: ?m.26084_, hf: ?m.26060hf, ha: ?m.26063ha, rfl: ∀ {α : Sort ?u.26107} {a : α}, a = arfl⟩

/--
`SatisfiesM` distributes over `<*>`, weakest precondition version 1.
(Use this when `x` and the goal are known and `f` is a subgoal.)
-/
protected theorem seq_pre: ∀ {m : Type u_1 → Type u_2} {α : Type u_1} {p₂ : α → Prop} {α_1 : Type u_1} {q : α_1 → Prop} {f : m (α → α_1)}
[inst : Applicative m] [inst_1 : LawfulApplicative m] {x : m α},
SatisfiesM (fun f => ∀ {a : α}, p₂ a → q (f a)) f → SatisfiesM p₂ x → SatisfiesM q (Seq.seq f fun x_1 => x)seq_pre [Applicative: (Type ?u.26159 → Type ?u.26158) → Type (max(?u.26159+1)?u.26158)Applicative m: ?m.26155m] [LawfulApplicative: (f : Type ?u.26348 → Type ?u.26347) → [inst : Applicative f] → PropLawfulApplicative m: ?m.26155m] {x: m αx : m: ?m.26155m α: ?m.26179α}
(hf: SatisfiesM (fun f => ∀ {a : ?m.26393 f}, ?m.26394 f → ?m.26395 f) fhf : SatisfiesM: {α : Type ?u.26365} → {m : Type ?u.26365 → Type ?u.26364} → [inst : Functor m] → (α → Prop) → m α → PropSatisfiesM (fun f: ?m.26379f => ∀ {a: ?m.26382a}, p₂: ?m.26227p₂ a: ?m.26382a → q: ?m.26277q (f: ?m.26379f a: ?m.26382a)) f: ?m.26339f) (hx: SatisfiesM p₂ xhx : SatisfiesM: {α : Type ?u.26419} → {m : Type ?u.26419 → Type ?u.26418} → [inst : Functor m] → (α → Prop) → m α → PropSatisfiesM p₂: ?m.26227p₂ x: m αx) :
SatisfiesM: {α : Type ?u.26455} → {m : Type ?u.26455 → Type ?u.26454} → [inst : Functor m] → (α → Prop) → m α → PropSatisfiesM q: ?m.26277q (f: ?m.26339f <*> x: m αx) :=
hf: SatisfiesM (fun f => ∀ {a : α}, p₂ a → q (f a)) fhf.seq: ∀ {m : Type ?u.26554 → Type ?u.26555} {α α_1 : Type ?u.26554} {p₁ : (α → α_1) → Prop} {f : m (α → α_1)} {p₂ : α → Prop}
{q : α_1 → Prop} [inst : Applicative m] [inst_1 : LawfulApplicative m] {x : m α},
SatisfiesM p₁ f →
SatisfiesM p₂ x → (∀ {f : α → α_1} {a : α}, p₁ f → p₂ a → q (f a)) → SatisfiesM q (Seq.seq f fun x_1 => x)seq hx: SatisfiesM p₂ xhx fun hf: ?m.26618hf ha: ?m.26623ha => hf: ?m.26618hf ha: ?m.26623ha

/--
`SatisfiesM` distributes over `<*>`, weakest precondition version 2.
(Use this when `f` and the goal are known and `x` is a subgoal.)
-/
protected theorem seq_pre': ∀ {m : Type u_1 → Type u_2} {α α_1 : Type u_1} {p₁ : (α → α_1) → Prop} {f : m (α → α_1)} {q : α_1 → Prop}
[inst : Applicative m] [inst_1 : LawfulApplicative m] {x : m α},
SatisfiesM p₁ f → SatisfiesM (fun a => ∀ {f : α → α_1}, p₁ f → q (f a)) x → SatisfiesM q (Seq.seq f fun x_1 => x)seq_pre' [Applicative: (Type ?u.26865 → Type ?u.26864) → Type (max(?u.26865+1)?u.26864)Applicative m: ?m.26670m] [LawfulApplicative: (f : Type ?u.26786 → Type ?u.26785) → [inst : Applicative f] → PropLawfulApplicative m: ?m.26670m] {x: m αx : m: ?m.26670m α: ?m.26694α}
(hf: SatisfiesM p₁ fhf : SatisfiesM: {α : Type ?u.26803} → {m : Type ?u.26803 → Type ?u.26802} → [inst : Functor m] → (α → Prop) → m α → PropSatisfiesM p₁: ?m.26734p₁ f: ?m.26777f) (hx: SatisfiesM (fun a => ∀ {f : ?m.26942}, p₁ f → ?m.26948 a) xhx : SatisfiesM: {α : Type ?u.26921} → {m : Type ?u.26921 → Type ?u.26920} → [inst : Functor m] → (α → Prop) → m α → PropSatisfiesM (fun a: ?m.26935a => ∀ {f: ?m.26938f}, ```