/-
Copyright (c) 2022 Mario Carneiro. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
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 m
LawfulMonad.mk' (m: Type u → Type v
m : 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 v
m]
    (id_map: ∀ {α : Type u} (x : m α), id <$> x = x
id_map : ∀ {α: ?m.14
α} (x: m α
x : m: Type u → Type v
m α: ?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 x
pure_bind : ∀ {α: ?m.66
α β: ?m.69
β} (x: α
x : α: ?m.66
α) (f: α → m β
f : α: ?m.66
α → m: Type u → Type v
m β: ?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 >>= g
bind_assoc : ∀ {α: ?m.179
α β: ?m.182
β γ: ?m.185
γ} (x: m α
x : m: Type u → Type v
m α: ?m.179
α) (f: α → m β
f : α: ?m.179
α → m: Type u → Type v
m β: ?m.182
β) (g: β → m γ
g : β: ?m.182
β → m: Type u → Type v
m γ: ?m.185
γ),
      x: m α
x >>= f: α → m β
f >>= g: β → m γ
g = x: m α
x >>= fun x: ?m.255
x => f: α → m β
f x: ?m.255
x >>= 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 v
m β: ?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 v
m α: ?m.481
α) (y: m β
y : m: Type u → Type v
m β: ?m.484
β),
      x: m α
x <* y: m β
y = (x: m α
x >>= fun a: ?m.531
a => y: m β
y >>= fun _: ?m.568
_ => pure: {f : Type ?u.571 → Type ?u.570} → [self : Pure f] → {α : Type ?u.571} → α → f α
pure a: ?m.531
a) := 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 v
m α: ?m.675
α) (y: m β
y : m: Type u → Type v
m β: ?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 v
m α: ?m.805
α),
      x: m α
x >>= (fun y: ?m.826
y => pure: {f : Type ?u.829 → Type ?u.828} → [self : Pure f] → {α : Type ?u.829} → α → f α
pure (f: α → β
f y: ?m.826
y)) = 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 v
m (α: ?m.942
α → β: ?m.945
β)) (x: m α
x : m: Type u → Type v
m α: ?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] → Prop
LawfulMonad m: Type u → Type v
m :=
  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 v
m α: ?m.1071
α) = pure: {f : Type ?u.1153 → Type ?u.1152} → [self : Pure f] → {α : Type ?u.1153} → α → f α
pure (g: α → β
g x: α
x) := by
Goals accomplished! 🐙
    m: Type u → Type v

inst✝: Monad m

id_map: ∀ {α : Type u} (x : m α), id <$> x = x

pure_bind: ∀ {α β : Type u} (x : α) (f : α → m β), pure x >>= f = f x

bind_assoc: ∀ {α β γ : Type u} (x : m α) (f : α → m β) (g : β → m γ), x >>= f >>= g = x >>= fun x => f x >>= g

map_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 u

g: α → β

x: α

g <$> pure x = pure (g x)rw [m: Type u → Type v

inst✝: Monad m

id_map: ∀ {α : Type u} (x : m α), id <$> x = x

pure_bind: ∀ {α β : Type u} (x : α) (f : α → m β), pure x >>= f = f x

bind_assoc: ∀ {α β γ : Type u} (x : m α) (f : α → m β) (g : β → m γ), x >>= f >>= g = x >>= fun x => f x >>= g

map_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 u

g: α → β

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 v

inst✝: Monad m

id_map: ∀ {α : Type u} (x : m α), id <$> x = x

pure_bind: ∀ {α β : Type u} (x : α) (f : α → m β), pure x >>= f = f x

bind_assoc: ∀ {α β γ : Type u} (x : m α) (f : α → m β) (g : β → m γ), x >>= f >>= g = x >>= fun x => f x >>= g

map_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 u

g: α → β

x: α

(do
    let y ← pure x
    pure (g y)) =   pure (g x)]m: Type u → Type v

inst✝: Monad m

id_map: ∀ {α : Type u} (x : m α), id <$> x = x

pure_bind: ∀ {α β : Type u} (x : α) (f : α → m β), pure x >>= f = f x

bind_assoc: ∀ {α β γ : Type u} (x : m α) (f : α → m β) (g : β → m γ), x >>= f >>= g = x >>= fun x => f x >>= g

map_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 u

g: α → β

x: α

(do
    let y ← pure x
    pure (g y)) =   pure (g x);m: Type u → Type v

inst✝: Monad m

id_map: ∀ {α : Type u} (x : m α), id <$> x = x

pure_bind: ∀ {α β : Type u} (x : α) (f : α → m β), pure x >>= f = f x

bind_assoc: ∀ {α β γ : Type u} (x : m α) (f : α → m β) (g : β → m γ), x >>= f >>= g = x >>= fun x => f x >>= g

map_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 u

g: α → β

x: α

(do
    let y ← pure x
    pure (g y)) =   pure (g x) m: Type u → Type v

inst✝: Monad m

id_map: ∀ {α : Type u} (x : m α), id <$> x = x

pure_bind: ∀ {α β : Type u} (x : α) (f : α → m β), pure x >>= f = f x

bind_assoc: ∀ {α β γ : Type u} (x : m α) (f : α → m β) (g : β → m γ), x >>= f >>= g = x >>= fun x => f x >>= g

map_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 u

g: α → β

x: α

g <$> pure x = pure (g x)simp [pure_bind: ∀ {α β : Type u} (x : α) (f : α → m β), pure x >>= f = f x
pure_bind]
Goals accomplished! 🐙
  { id_map: ∀ {α : Type u} (x : m α), id <$> x = x
id_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 x
pure_bind, bind_assoc: ∀ {α β γ : Type u} (x : m α) (f : α → m β) (g : β → m γ), x >>= f >>= g = x >>= fun x => f x >>= g
bind_assoc, map_pure: ∀ {α β : Type u} (g : α → β) (x : α), g <$> pure x = pure (g x)
map_pure,
    comp_map := by
Goals accomplished! 🐙 m: Type u → Type v

inst✝: Monad m

id_map: ∀ {α : Type u} (x : m α), id <$> x = x

pure_bind: ∀ {α β : Type u} (x : α) (f : α → m β), pure x >>= f = f x

bind_assoc: ∀ {α β γ : Type u} (x : m α) (f : α → m β) (g : β → m γ), x >>= f >>= g = x >>= fun x => f x >>= g

map_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 >>= g
bind_assoc, pure_bind: ∀ {α β : Type u} (x : α) (f : α → m β), pure x >>= f = f x
pure_bind]
Goals accomplished! 🐙
    pure_seq := by
Goals accomplished! 🐙 m: Type u → Type v

inst✝: Monad m

id_map: ∀ {α : Type u} (x : m α), id <$> x = x

pure_bind: ∀ {α β : Type u} (x : α) (f : α → m β), pure x >>= f = f x

bind_assoc: ∀ {α β γ : Type u} (x : m α) (f : α → m β) (g : β → m γ), x >>= f >>= g = x >>= fun x => f x >>= g

map_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 v

inst✝: Monad m

id_map: ∀ {α : Type u} (x : m α), id <$> x = x

pure_bind: ∀ {α β : Type u} (x : α) (f : α → m β), pure x >>= f = f x

bind_assoc: ∀ {α β γ : Type u} (x : m α) (f : α → m β) (g : β → m γ), x >>= f >>= g = x >>= fun x => f x >>= g

map_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 => x✝) = g✝ <$> x✝;m: Type u → Type v

inst✝: Monad m

id_map: ∀ {α : Type u} (x : m α), id <$> x = x

pure_bind: ∀ {α β : Type u} (x : α) (f : α → m β), pure x >>= f = f x

bind_assoc: ∀ {α β γ : Type u} (x : m α) (f : α → m β) (g : β → m γ), x >>= f >>= g = x >>= fun x => f x >>= g

map_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 => x✝) = g✝ <$> x✝ m: Type u → Type v

inst✝: Monad m

id_map: ∀ {α : Type u} (x : m α), id <$> x = x

pure_bind: ∀ {α β : Type u} (x : α) (f : α → m β), pure x >>= f = f x

bind_assoc: ∀ {α β γ : Type u} (x : m α) (f : α → m β) (g : β → m γ), x >>= f >>= g = x >>= fun x => f x >>= g

map_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 v

inst✝: Monad m

id_map: ∀ {α : Type u} (x : m α), id <$> x = x

pure_bind: ∀ {α β : Type u} (x : α) (f : α → m β), pure x >>= f = f x

bind_assoc: ∀ {α β γ : Type u} (x : m α) (f : α → m β) (g : β → m γ), x >>= f >>= g = x >>= fun x => f x >>= g

map_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 => 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 v

inst✝: Monad m

id_map: ∀ {α : Type u} (x : m α), id <$> x = x

pure_bind: ∀ {α β : Type u} (x : α) (f : α → m β), pure x >>= f = f x

bind_assoc: ∀ {α β γ : Type u} (x : m α) (f : α → m β) (g : β → m γ), x >>= f >>= g = x >>= fun x => f x >>= g

map_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 α✝

(do
    let x ← pure g✝
    x <$> x✝) =   g✝ <$> x✝]m: Type u → Type v

inst✝: Monad m

id_map: ∀ {α : Type u} (x : m α), id <$> x = x

pure_bind: ∀ {α β : Type u} (x : α) (f : α → m β), pure x >>= f = f x

bind_assoc: ∀ {α β γ : Type u} (x : m α) (f : α → m β) (g : β → m γ), x >>= f >>= g = x >>= fun x => f x >>= g

map_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 α✝

(do
    let x ← pure g✝
    x <$> x✝) =   g✝ <$> x✝;m: Type u → Type v

inst✝: Monad m

id_map: ∀ {α : Type u} (x : m α), id <$> x = x

pure_bind: ∀ {α β : Type u} (x : α) (f : α → m β), pure x >>= f = f x

bind_assoc: ∀ {α β γ : Type u} (x : m α) (f : α → m β) (g : β → m γ), x >>= f >>= g = x >>= fun x => f x >>= g

map_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 α✝

(do
    let x ← pure g✝
    x <$> x✝) =   g✝ <$> x✝ m: Type u → Type v

inst✝: Monad m

id_map: ∀ {α : Type u} (x : m α), id <$> x = x

pure_bind: ∀ {α β : Type u} (x : α) (f : α → m β), pure x >>= f = f x

bind_assoc: ∀ {α β γ : Type u} (x : m α) (f : α → m β) (g : β → m γ), x >>= f >>= g = x >>= fun x => f x >>= g

map_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 x
pure_bind]
Goals accomplished! 🐙
    seq_pure := by
Goals accomplished! 🐙 m: Type u → Type v

inst✝: Monad m

id_map: ∀ {α : Type u} (x : m α), id <$> x = x

pure_bind: ∀ {α β : Type u} (x : α) (f : α → m β), pure x >>= f = f x

bind_assoc: ∀ {α β γ : Type u} (x : m α) (f : α → m β) (g : β → m γ), x >>= f >>= g = x >>= fun x => f x >>= g

map_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 v

inst✝: Monad m

id_map: ∀ {α : Type u} (x : m α), id <$> x = x

pure_bind: ∀ {α β : Type u} (x : α) (f : α → m β), pure x >>= f = f x

bind_assoc: ∀ {α β γ : Type u} (x : m α) (f : α → m β) (g : β → m γ), x >>= f >>= g = x >>= fun x => f x >>= g

map_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 => pure x✝) = (fun h => h x✝) <$> g✝;m: Type u → Type v

inst✝: Monad m

id_map: ∀ {α : Type u} (x : m α), id <$> x = x

pure_bind: ∀ {α β : Type u} (x : α) (f : α → m β), pure x >>= f = f x

bind_assoc: ∀ {α β γ : Type u} (x : m α) (f : α → m β) (g : β → m γ), x >>= f >>= g = x >>= fun x => f x >>= g

map_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 => pure x✝) = (fun h => h x✝) <$> g✝ m: Type u → Type v

inst✝: Monad m

id_map: ∀ {α : Type u} (x : m α), id <$> x = x

pure_bind: ∀ {α β : Type u} (x : α) (f : α → m β), pure x >>= f = f x

bind_assoc: ∀ {α β γ : Type u} (x : m α) (f : α → m β) (g : β → m γ), x >>= f >>= g = x >>= fun x => f x >>= g

map_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 v

inst✝: Monad m

id_map: ∀ {α : Type u} (x : m α), id <$> x = x

pure_bind: ∀ {α β : Type u} (x : α) (f : α → m β), pure x >>= f = f x

bind_assoc: ∀ {α β γ : Type u} (x : m α) (f : α → m β) (g : β → m γ), x >>= f >>= g = x >>= fun x => f x >>= g

map_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 => 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 v

inst✝: Monad m

id_map: ∀ {α : Type u} (x : m α), id <$> x = x

pure_bind: ∀ {α β : Type u} (x : α) (f : α → m β), pure x >>= f = f x

bind_assoc: ∀ {α β γ : Type u} (x : m α) (f : α → m β) (g : β → m γ), x >>= f >>= g = x >>= fun x => f x >>= g

map_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✝: α✝

(do
    let x ← g✝
    x <$> pure x✝) =   (fun h => h x✝) <$> g✝]m: Type u → Type v

inst✝: Monad m

id_map: ∀ {α : Type u} (x : m α), id <$> x = x

pure_bind: ∀ {α β : Type u} (x : α) (f : α → m β), pure x >>= f = f x

bind_assoc: ∀ {α β γ : Type u} (x : m α) (f : α → m β) (g : β → m γ), x >>= f >>= g = x >>= fun x => f x >>= g

map_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✝: α✝

(do
    let x ← g✝
    x <$> pure x✝) =   (fun h => h x✝) <$> g✝;m: Type u → Type v

inst✝: Monad m

id_map: ∀ {α : Type u} (x : m α), id <$> x = x

pure_bind: ∀ {α β : Type u} (x : α) (f : α → m β), pure x >>= f = f x

bind_assoc: ∀ {α β γ : Type u} (x : m α) (f : α → m β) (g : β → m γ), x >>= f >>= g = x >>= fun x => f x >>= g

map_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✝: α✝

(do
    let x ← g✝
    x <$> pure x✝) =   (fun h => h x✝) <$> g✝ m: Type u → Type v

inst✝: Monad m

id_map: ∀ {α : Type u} (x : m α), id <$> x = x

pure_bind: ∀ {α β : Type u} (x : α) (f : α → m β), pure x >>= f = f x

bind_assoc: ∀ {α β γ : Type u} (x : m α) (f : α → m β) (g : β → m γ), x >>= f >>= g = x >>= fun x => f x >>= g

map_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 := by
Goals accomplished! 🐙 m: Type u → Type v

inst✝: Monad m

id_map: ∀ {α : Type u} (x : m α), id <$> x = x

pure_bind: ∀ {α β : Type u} (x : α) (f : α → m β), pure x >>= f = f x

bind_assoc: ∀ {α β γ : Type u} (x : m α) (f : α → m β) (g : β → m γ), x >>= f >>= g = x >>= fun x => f x >>= g

map_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 >>= g
bind_assoc, pure_bind: ∀ {α β : Type u} (x : α) (f : α → m β), pure x >>= f = f x
pure_bind]
Goals accomplished! 🐙
    map_const := funext: ∀ {α : Sort ?u.1235} {β : α → Sort ?u.1234} {f g : (x : α) → β x}, (∀ (x : α), f x = g x) → f = g
funext fun x: ?m.1250
x => funext: ∀ {α : Sort ?u.1253} {β : α → Sort ?u.1252} {f g : (x : α) → β x}, (∀ (x : α), f x = g x) → f = g
funext (map_const: autoParam (∀ {α β : Type u} (x : α) (y : m β), Functor.mapConst x y = Function.const β x <$> y) _auto✝
map_const x: ?m.1250
x)
    seqLeft_eq := by
Goals accomplished! 🐙 m: Type u → Type v

inst✝: Monad m

id_map: ∀ {α : Type u} (x : m α), id <$> x = x

pure_bind: ∀ {α β : Type u} (x : α) (f : α → m β), pure x >>= f = f x

bind_assoc: ∀ {α β γ : Type u} (x : m α) (f : α → m β) (g : β → m γ), x >>= f >>= g = x >>= fun x => f x >>= g

map_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 x
pure_bind, bind_assoc: ∀ {α β γ : Type u} (x : m α) (f : α → m β) (g : β → m γ), x >>= f >>= g = x >>= fun x => f x >>= g
bind_assoc]
Goals accomplished! 🐙
    seqRight_eq := fun x: ?m.1291
x y: ?m.1294
y => by
Goals accomplished! 🐙
      m: Type u → Type v

inst✝: Monad m

id_map: ∀ {α : Type u} (x : m α), id <$> x = x

pure_bind: ∀ {α β : Type u} (x : α) (f : α → m β), pure x >>= f = f x

bind_assoc: ∀ {α β γ : Type u} (x : m α) (f : α → m β) (g : β → m γ), x >>= f >>= g = x >>= fun x => f x >>= g

map_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 β✝

(SeqRight.seqRight x fun x => y) = Seq.seq (Function.const α✝ id <$> x) fun x => yrw [m: Type u → Type v

inst✝: Monad m

id_map: ∀ {α : Type u} (x : m α), id <$> x = x

pure_bind: ∀ {α β : Type u} (x : α) (f : α → m β), pure x >>= f = f x

bind_assoc: ∀ {α β γ : Type u} (x : m α) (f : α → m β) (g : β → m γ), x >>= f >>= g = x >>= fun x => f x >>= g

map_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 β✝

(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 v

inst✝: Monad m

id_map: ∀ {α : Type u} (x : m α), id <$> x = x

pure_bind: ∀ {α β : Type u} (x : α) (f : α → m β), pure x >>= f = f x

bind_assoc: ∀ {α β γ : Type u} (x : m α) (f : α → m β) (g : β → m γ), x >>= f >>= g = x >>= fun x => f x >>= g

map_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 β✝

(do
    let _ ← x
    y) =   Seq.seq (Function.const α✝ id <$> x) fun x => y m: Type u → Type v

inst✝: Monad m

id_map: ∀ {α : Type u} (x : m α), id <$> x = x

pure_bind: ∀ {α β : Type u} (x : α) (f : α → m β), pure x >>= f = f x

bind_assoc: ∀ {α β γ : Type u} (x : m α) (f : α → m β) (g : β → m γ), x >>= f >>= g = x >>= fun x => f x >>= g

map_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 β✝

(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 v

inst✝: Monad m

id_map: ∀ {α : Type u} (x : m α), id <$> x = x

pure_bind: ∀ {α β : Type u} (x : α) (f : α → m β), pure x >>= f = f x

bind_assoc: ∀ {α β γ : Type u} (x : m α) (f : α → m β) (g : β → m γ), x >>= f >>= g = x >>= fun x => f x >>= g

map_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 β✝

(do
    let _ ← x
    y) =   do
  let x ← Function.const α✝ id <$> x
  x <$> y m: Type u → Type v

inst✝: Monad m

id_map: ∀ {α : Type u} (x : m α), id <$> x = x

pure_bind: ∀ {α β : Type u} (x : α) (f : α → m β), pure x >>= f = f x

bind_assoc: ∀ {α β γ : Type u} (x : m α) (f : α → m β) (g : β → m γ), x >>= f >>= g = x >>= fun x => f x >>= g

map_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 β✝

(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 v

inst✝: Monad m

id_map: ∀ {α : Type u} (x : m α), id <$> x = x

pure_bind: ∀ {α β : Type u} (x : α) (f : α → m β), pure x >>= f = f x

bind_assoc: ∀ {α β γ : Type u} (x : m α) (f : α → m β) (g : β → m γ), x >>= f >>= g = x >>= fun x => f x >>= g

map_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 β✝

(do
    let _ ← x
    y) =   do
  let x ←
    do
      let y ← x
      pure (Function.const α✝ id y)
  x <$> y m: Type u → Type v

inst✝: Monad m

id_map: ∀ {α : Type u} (x : m α), id <$> x = x

pure_bind: ∀ {α β : Type u} (x : α) (f : α → m β), pure x >>= f = f x

bind_assoc: ∀ {α β γ : Type u} (x : m α) (f : α → m β) (g : β → m γ), x >>= f >>= g = x >>= fun x => f x >>= g

map_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 β✝

(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 >>= g
bind_assocm: Type u → Type v

inst✝: Monad m

id_map: ∀ {α : Type u} (x : m α), id <$> x = x

pure_bind: ∀ {α β : Type u} (x : α) (f : α → m β), pure x >>= f = f x

bind_assoc: ∀ {α β γ : Type u} (x : m α) (f : α → m β) (g : β → m γ), x >>= f >>= g = x >>= fun x => f x >>= g

map_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 β✝

(do
    let _ ← x
    y) =   do
  let x ← x
  let x ← pure (Function.const α✝ id x)
  x <$> y]m: Type u → Type v

inst✝: Monad m

id_map: ∀ {α : Type u} (x : m α), id <$> x = x

pure_bind: ∀ {α β : Type u} (x : α) (f : α → m β), pure x >>= f = f x

bind_assoc: ∀ {α β γ : Type u} (x : m α) (f : α → m β) (g : β → m γ), x >>= f >>= g = x >>= fun x => f x >>= g

map_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 β✝

(do
    let _ ← x
    y) =   do
  let x ← x
  let x ← pure (Function.const α✝ id x)
  x <$> y;m: Type u → Type v

inst✝: Monad m

id_map: ∀ {α : Type u} (x : m α), id <$> x = x

pure_bind: ∀ {α β : Type u} (x : α) (f : α → m β), pure x >>= f = f x

bind_assoc: ∀ {α β γ : Type u} (x : m α) (f : α → m β) (g : β → m γ), x >>= f >>= g = x >>= fun x => f x >>= g

map_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 β✝

(do
    let _ ← x
    y) =   do
  let x ← x
  let x ← pure (Function.const α✝ id x)
  x <$> y m: Type u → Type v

inst✝: Monad m

id_map: ∀ {α : Type u} (x : m α), id <$> x = x

pure_bind: ∀ {α β : Type u} (x : α) (f : α → m β), pure x >>= f = f x

bind_assoc: ∀ {α β γ : Type u} (x : m α) (f : α → m β) (g : β → m γ), x >>= f >>= g = x >>= fun x => f x >>= g

map_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 β✝

(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 x
pure_bind, id_map: ∀ {α : Type u} (x : m α), id <$> x = x
id_map]
Goals accomplished! 🐙 }

instance: ∀ {ε : Type u_1}, LawfulMonad (Except ε)
instance : LawfulMonad: (m : Type ?u.11294 → Type ?u.11293) → [inst : Monad m] → Prop
LawfulMonad (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✝⁴ →
                  LawfulMonad m
LawfulMonad.mk'
  (id_map := fun x: ?m.11374
x => by
Goals accomplished! 🐙 ε: Type ?u.11296

α✝: Type ?u.11295

x: Except ε α✝

id <$> x = xcases x: Except ε α✝
xε: Type ?u.11296

α✝: Type ?u.11295

a✝: ε

errorid <$> Except.error a✝ = Except.error a✝
ε: Type ?u.11296

α✝: Type ?u.11295

a✝: α✝

okid <$> Except.ok a✝ = Except.ok a✝ ε: Type ?u.11296

α✝: Type ?u.11295

x: Except ε α✝

id <$> x = x<;>ε: Type ?u.11296

α✝: Type ?u.11295

a✝: ε

errorid <$> Except.error a✝ = Except.error a✝
ε: Type ?u.11296

α✝: Type ?u.11295

a✝: α✝

okid <$> Except.ok a✝ = Except.ok a✝ ε: Type ?u.11296

α✝: Type ?u.11295

x: Except ε α✝

id <$> x = xrfl
Goals accomplished! 🐙)
  (pure_bind := fun a: ?m.11391
a f: ?m.11394
f => rfl: ∀ {α : Sort ?u.11397} {a : α}, a = a
rfl)
  (bind_assoc := fun a: ?m.11453
a f: ?m.11456
f g: ?m.11460
g => by
Goals accomplished! 🐙 ε: Type ?u.11296

α✝, β✝, γ✝: Type ?u.11295

a: Except ε α✝

f: α✝ → Except ε β✝

g: β✝ → Except ε γ✝

a >>= f >>= g = a >>= fun x => f x >>= gcases a: Except ε α✝
aε: Type ?u.11296

α✝, β✝, γ✝: Type ?u.11295

f: α✝ → Except ε β✝

g: β✝ → Except ε γ✝

a✝: ε

errorExcept.error a✝ >>= f >>= g = Except.error a✝ >>= fun x => f x >>= g
ε: Type ?u.11296

α✝, β✝, γ✝: Type ?u.11295

f: α✝ → Except ε β✝

g: β✝ → Except ε γ✝

a✝: α✝

okExcept.ok a✝ >>= f >>= g = Except.ok a✝ >>= fun x => f x >>= g ε: Type ?u.11296

α✝, β✝, γ✝: Type ?u.11295

a: Except ε α✝

f: α✝ → Except ε β✝

g: β✝ → Except ε γ✝

a >>= f >>= g = a >>= fun x => f x >>= g<;>ε: Type ?u.11296

α✝, β✝, γ✝: Type ?u.11295

f: α✝ → Except ε β✝

g: β✝ → Except ε γ✝

a✝: ε

errorExcept.error a✝ >>= f >>= g = Except.error a✝ >>= fun x => f x >>= g
ε: Type ?u.11296

α✝, β✝, γ✝: Type ?u.11295

f: α✝ → Except ε β✝

g: β✝ → Except ε γ✝

a✝: α✝

okExcept.ok a✝ >>= f >>= g = Except.ok a✝ >>= fun x => f x >>= g ε: Type ?u.11296

α✝, β✝, γ✝: Type ?u.11295

a: Except ε α✝

f: α✝ → Except ε β✝

g: β✝ → Except ε γ✝

a >>= f >>= g = a >>= fun x => f x >>= grfl
Goals accomplished! 🐙)

instance: ∀ {ε : Type u_1}, LawfulApplicative (Except ε)
instance : LawfulApplicative: (f : Type ?u.11992 → Type ?u.11991) → [inst : Applicative f] → Prop
LawfulApplicative (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] → Prop
LawfulFunctor (Except: Type ?u.12080 → Type ?u.12079 → Type (max?u.12080?u.12079)
Except ε: ?m.12074
ε) := inferInstance: ∀ {α : Sort ?u.12123} [i : α], α
inferInstance

instance: LawfulMonad Option
instance : LawfulMonad: (m : Type ?u.12180 → Type ?u.12179) → [inst : Monad m] → Prop
LawfulMonad Option: Type ?u.12181 → Type ?u.12181
Option := 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✝⁴ →
                  LawfulMonad m
LawfulMonad.mk'
  (id_map := fun x: ?m.12253
x => by
Goals accomplished! 🐙 α✝: Type ?u.12181

x: Option α✝

id <$> x = xcases x: Option α✝
xα✝: Type ?u.12181

noneid <$> none = none
α✝: Type ?u.12181

val✝: α✝

someid <$> some val✝ = some val✝ α✝: Type ?u.12181

x: Option α✝

id <$> x = x<;>α✝: Type ?u.12181

noneid <$> none = none
α✝: Type ?u.12181

val✝: α✝

someid <$> some val✝ = some val✝ α✝: Type ?u.12181

x: Option α✝

id <$> x = xrfl
Goals accomplished! 🐙)
  (pure_bind := fun x: ?m.12270
x f: ?m.12273
f => rfl: ∀ {α : Sort ?u.12276} {a : α}, a = a
rfl)
  (bind_assoc := fun x: ?m.12333
x f: ?m.12336
f g: ?m.12340
g => by
Goals accomplished! 🐙 α✝, β✝, γ✝: Type ?u.12181

x: Option α✝

f: α✝ → Option β✝

g: β✝ → Option γ✝

x >>= f >>= g = x >>= fun x => f x >>= gcases x: Option α✝
xα✝, β✝, γ✝: Type ?u.12181

f: α✝ → Option β✝

g: β✝ → Option γ✝

nonenone >>= f >>= g = none >>= fun x => f x >>= g
α✝, β✝, γ✝: Type ?u.12181

f: α✝ → Option β✝

g: β✝ → Option γ✝

val✝: α✝

somesome val✝ >>= f >>= g = some val✝ >>= fun x => f x >>= g α✝, β✝, γ✝: Type ?u.12181

x: Option α✝

f: α✝ → Option β✝

g: β✝ → Option γ✝

x >>= f >>= g = x >>= fun x => f x >>= g<;>α✝, β✝, γ✝: Type ?u.12181

f: α✝ → Option β✝

g: β✝ → Option γ✝

nonenone >>= f >>= g = none >>= fun x => f x >>= g
α✝, β✝, γ✝: Type ?u.12181

f: α✝ → Option β✝

g: β✝ → Option γ✝

val✝: α✝

somesome val✝ >>= f >>= g = some val✝ >>= fun x => f x >>= g α✝, β✝, γ✝: Type ?u.12181

x: Option α✝

f: α✝ → Option β✝

g: β✝ → Option γ✝

x >>= f >>= g = x >>= fun x => f x >>= grfl
Goals accomplished! 🐙)
  (bind_pure_comp := fun f: ?m.12374
f x: ?m.12378
x => by
Goals accomplished! 🐙 α✝, β✝: Type ?u.12181

f: α✝ → β✝

x: Option α✝

(do
    let y ← x
    pure (f y)) =   f <$> xcases x: Option α✝
xα✝, β✝: Type ?u.12181

f: α✝ → β✝

none(do
    let y ← none
    pure (f y)) =   f <$> none
α✝, β✝: Type ?u.12181

f: α✝ → β✝

val✝: α✝

some(do
    let y ← some val✝
    pure (f y)) =   f <$> some val✝ α✝, β✝: Type ?u.12181

f: α✝ → β✝

x: Option α✝

(do
    let y ← x
    pure (f y)) =   f <$> x<;>α✝, β✝: Type ?u.12181

f: α✝ → β✝

none(do
    let y ← none
    pure (f y)) =   f <$> none
α✝, β✝: Type ?u.12181

f: α✝ → β✝

val✝: α✝

some(do
    let y ← some val✝
    pure (f y)) =   f <$> some val✝ α✝, β✝: Type ?u.12181

f: α✝ → β✝

x: Option α✝

(do
    let y ← x
    pure (f y)) =   f <$> xrfl
Goals accomplished! 🐙)

instance: LawfulApplicative Option
instance : LawfulApplicative: (f : Type ?u.12934 → Type ?u.12933) → [inst : Applicative f] → Prop
LawfulApplicative Option: Type ?u.12935 → Type ?u.12935
Option := inferInstance: ∀ {α : Sort ?u.12958} [i : α], α
inferInstance
instance: LawfulFunctor Option
instance : LawfulFunctor: (f : Type ?u.12992 → Type ?u.12991) → [inst : Functor f] → Prop
LawfulFunctor Option: Type ?u.12993 → Type ?u.12993
Option := 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 α → Prop
SatisfiesM {m: Type u → Type v
m : 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 v
m] (p: α → Prop
p : α: ?m.13066
α → Prop: Type
Prop) (x: m α
x : m: Type u → Type v
m α: ?m.13066
α) : Prop: Type
Prop :=
  ∃ x': m { a // p a }
x' : m: Type u → Type v
m {a: ?m.13098
a // p: α → Prop
p a: ?m.13098
a}, 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 x
of_true [Applicative: (Type ?u.13156 → Type ?u.13155) → Type (max(?u.13156+1)?u.13155)
Applicative m: ?m.13152
m] [LawfulApplicative: (f : Type ?u.13185 → Type ?u.13184) → [inst : Applicative f] → Prop
LawfulApplicative m: ?m.13152
m] {x: m α
x : m: ?m.13152
m α: ?m.13176
α}
    (h: ∀ (a : ?m.13232), ?m.13236 a
h : ∀ a: ?m.13232
a, p: ?m.13206
p a: ?m.13232
a) : SatisfiesM: {α : Type ?u.13240} → {m : Type ?u.13240 → Type ?u.13239} → [inst : Functor m] → (α → Prop) → m α → Prop
SatisfiesM p: ?m.13206
p x: m α
x :=
  ⟨(fun a: ?m.13318
a => ⟨a: ?m.13318
a, h: ∀ (a : α), p a
h a: ?m.13318
a⟩) <$> x: m α
x, by
Goals accomplished! 🐙 m: Type u_1 → Type u_2

α: Type u_1

p: α → Prop

inst✝¹: Applicative m

inst✝: LawfulApplicative m

x: m α

h: ∀ (a : α), p a

Subtype.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 <$> x
comp_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) x
trivial [Applicative: (Type ?u.13890 → Type ?u.13889) → Type (max(?u.13890+1)?u.13889)
Applicative m: ?m.13862
m] [LawfulApplicative: (f : Type ?u.13895 → Type ?u.13894) → [inst : Applicative f] → Prop
LawfulApplicative m: ?m.13862
m] {x: m α
x : m: ?m.13862
m α: ?m.13886
α} :
  SatisfiesM: {α : Type ?u.13912} → {m : Type ?u.13912 → Type ?u.13911} → [inst : Functor m] → (α → Prop) → m α → Prop
SatisfiesM (fun _: ?m.13926
_ => True: Prop
True) 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 x
of_true fun _: ?m.14001
_ => trivial: True
trivial

/-- 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 x
imp [Functor: (Type ?u.14027 → Type ?u.14026) → Type (max(?u.14027+1)?u.14026)
Functor m: ?m.14023
m] [LawfulFunctor: (f : Type ?u.14145 → Type ?u.14144) → [inst : Functor f] → Prop
LawfulFunctor m: ?m.14023
m] {x: m α
x : m: ?m.14023
m α: ?m.14045
α}
    (h: SatisfiesM p x
h : SatisfiesM: {α : Type ?u.14160} → {m : Type ?u.14160 → Type ?u.14159} → [inst : Functor m] → (α → Prop) → m α → Prop
SatisfiesM p: ?m.14083
p x: m α
x) (H: ∀ {a : α}, p a → q a
H : ∀ {a: ?m.14183
a}, p: ?m.14083
p a: ?m.14183
a → q: ?m.14136
q a: ?m.14183
a) : SatisfiesM: {α : Type ?u.14193} → {m : Type ?u.14193 → Type ?u.14192} → [inst : Functor m] → (α → Prop) → m α → Prop
SatisfiesM q: ?m.14136
q x: m α
x :=
  let ⟨x: m { a // p a }
x, h: Subtype.val <$> x = x✝
h⟩ := h: SatisfiesM p x
h; ⟨(fun ⟨a: α
a, h: p a
h⟩ => ⟨_: ?m.14344
_, H: ∀ {a : α}, p a → q a
H h: p a
h⟩) <$> x: m { a // p a }
x, by
Goals accomplished! 🐙 m: Type u_1 → Type u_2

α: Type u_1

p, q: α → Prop

inst✝¹: Functor m

inst✝: LawfulFunctor m

x✝: m α

h✝: SatisfiesM p x✝

H: ∀ {a : α}, p a → q a

x: 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_1

p, q: α → Prop

inst✝¹: Functor m

inst✝: LawfulFunctor m

x✝: m α

h✝: SatisfiesM p x✝

H: ∀ {a : α}, p a → q a

x: 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_1

p, q: α → Prop

inst✝¹: Functor m

inst✝: LawfulFunctor m

x✝: m α

h✝: SatisfiesM p x✝

H: ∀ {a : α}, p a → q a

x: 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_1

p, q: α → Prop

inst✝¹: Functor m

inst✝: LawfulFunctor m

x✝: m α

h✝: SatisfiesM p x✝

H: ∀ {a : α}, p a → q a

x: 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 <$> x
comp_mapm: Type u_1 → Type u_2

α: Type u_1

p, q: α → Prop

inst✝¹: Functor m

inst✝: LawfulFunctor m

x✝: m α

h✝: SatisfiesM p x✝

H: ∀ {a : α}, p a → q a

x: 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_1

p, q: α → Prop

inst✝¹: Functor m

inst✝: LawfulFunctor m

x✝: m α

h✝: SatisfiesM p x✝

H: ∀ {a : α}, p a → q a

x: 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_1

p, q: α → Prop

inst✝¹: Functor m

inst✝: LawfulFunctor m

x✝: m α

h✝: SatisfiesM p x✝

H: ∀ {a : α}, p a → q a

x: 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_1

p, q: α → Prop

inst✝¹: Functor m

inst✝: LawfulFunctor m

x✝: m α

h✝: SatisfiesM p x✝

H: ∀ {a : α}, p a → q a

x: 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✝rfl
Goals 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.14647
m] [LawfulFunctor: (f : Type ?u.14860 → Type ?u.14859) → [inst : Functor f] → Prop
LawfulFunctor m: ?m.14647
m] {x: m α
x : m: ?m.14647
m α: ?m.14669
α}
    (hx: SatisfiesM p x
hx : SatisfiesM: {α : Type ?u.14731} → {m : Type ?u.14731 → Type ?u.14730} → [inst : Functor m] → (α → Prop) → m α → Prop
SatisfiesM p: ?m.14707
p x: m α
x) (hf: ∀ {a : α}, p a → ?m.14904
hf : ∀ {a: ?m.14898
a}, p: ?m.14707
p a: unknown metavariable '?_uniq.14807'
a → q: ?m.14760
q (f: ?m.14851
f a: ?m.14898
a)) : SatisfiesM: {α : Type ?u.14908} → {m : Type ?u.14908 → Type ?u.14907} → [inst : Functor m] → (α → Prop) → m α → Prop
SatisfiesM q: ?m.14760
q (f: ?m.14851
f <$> x: m α
x) := by
Goals accomplished! 🐙
  m: Type u_1 → Type u_2

α: Type u_1

p: α → Prop

α✝: Type u_1

q: α✝ → Prop

f: α → α✝

inst✝¹: Functor m

inst✝: LawfulFunctor m

x: m α

hx: SatisfiesM p x

hf: ∀ {a : α}, p a → q (f a)

SatisfiesM q (f <$> x)let ⟨x': m { a // p a }
x', hx: Subtype.val <$> x' = x
hx⟩ := hx: SatisfiesM p x
hxm: Type u_1 → Type u_2

α: Type u_1

p: α → Prop

α✝: Type u_1

q: α✝ → Prop

f: α → α✝

inst✝¹: Functor m

inst✝: LawfulFunctor m

x: m α

hx✝: SatisfiesM p x

hf: ∀ {a : α}, p a → q (f a)

x': m { a // p a }

hx: Subtype.val <$> x' = x

SatisfiesM q (f <$> x)
  m: Type u_1 → Type u_2

α: Type u_1

p: α → Prop

α✝: Type u_1

q: α✝ → Prop

f: α → α✝

inst✝¹: Functor m

inst✝: LawfulFunctor m

x: m α

hx: SatisfiesM p x

hf: ∀ {a : α}, p a → q (f a)

SatisfiesM q (f <$> x)refine ⟨(fun ⟨a: α
a, h: p a
h⟩ => ⟨f: α → α✝
f a: α
a, hf: ∀ {a : α}, p a → q (f a)
hf h: p a
h⟩) <$> x': m { a // p a }
x', ?_: ?m.15081 ((fun x => ?m.15104 x) <$> x')
?_⟩m: Type u_1 → Type u_2

α: Type u_1

p: α → Prop

α✝: Type u_1

q: α✝ → Prop

f: α → α✝

inst✝¹: Functor m

inst✝: LawfulFunctor m

x: m α

hx✝: SatisfiesM p x

hf: ∀ {a : α}, p a → q (f a)

x': m { a // p a }

hx: Subtype.val <$> x' = x

Subtype.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_1

p: α → Prop

α✝: Type u_1

q: α✝ → Prop

f: α → α✝

inst✝¹: Functor m

inst✝: LawfulFunctor m

x: m α

hx: SatisfiesM p x

hf: ∀ {a : α}, p a → q (f a)

SatisfiesM q (f <$> x)rw [m: Type u_1 → Type u_2

α: Type u_1

p: α → Prop

α✝: Type u_1

q: α✝ → Prop

f: α → α✝

inst✝¹: Functor m

inst✝: LawfulFunctor m

x: m α

hx✝: SatisfiesM p x

hf: ∀ {a : α}, p a → q (f a)

x': m { a // p a }

hx: Subtype.val <$> x' = x

Subtype.val <$>     (fun x =>
        match x with
        | { val := a, property := h } => { val := f a, property := (_ : q (f a)) }) <$>       x' =   f <$> x← hx: Subtype.val <$> x' = x
hxm: Type u_1 → Type u_2

α: Type u_1

p: α → Prop

α✝: Type u_1

q: α✝ → Prop

f: α → α✝

inst✝¹: Functor m

inst✝: LawfulFunctor m

x: m α

hx✝: SatisfiesM p x

hf: ∀ {a : α}, p a → q (f a)

x': m { a // p a }

hx: Subtype.val <$> x' = x

Subtype.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_1

p: α → Prop

α✝: Type u_1

q: α✝ → Prop

f: α → α✝

inst✝¹: Functor m

inst✝: LawfulFunctor m

x: m α

hx✝: SatisfiesM p x

hf: ∀ {a : α}, p a → q (f a)

x': m { a // p a }

hx: Subtype.val <$> x' = x

Subtype.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_1

p: α → Prop

α✝: Type u_1

q: α✝ → Prop

f: α → α✝

inst✝¹: Functor m

inst✝: LawfulFunctor m

x: m α

hx✝: SatisfiesM p x

hf: ∀ {a : α}, p a → q (f a)

x': m { a // p a }

hx: Subtype.val <$> x' = x

Subtype.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_1

p: α → Prop

α✝: Type u_1

q: α✝ → Prop

f: α → α✝

inst✝¹: Functor m

inst✝: LawfulFunctor m

x: m α

hx: SatisfiesM p x

hf: ∀ {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 <$> x
comp_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.16246
m] [LawfulFunctor: (f : Type ?u.16277 → Type ?u.16276) → [inst : Functor f] → Prop
LawfulFunctor m: ?m.16246
m] {x: m α
x : m: ?m.16246
m α: ?m.16268
α}
    (hx: SatisfiesM p x
hx : SatisfiesM: {α : Type ?u.16400} → {m : Type ?u.16400 → Type ?u.16399} → [inst : Functor m] → (α → Prop) → m α → Prop
SatisfiesM p: ?m.16306
p x: m α
x) : SatisfiesM: {α : Type ?u.16423} → {m : Type ?u.16423 → Type ?u.16422} → [inst : Functor m] → (α → Prop) → m α → Prop
SatisfiesM (fun b: ?m.16437
b => ∃ a: ?m.16442
a, p: ?m.16306
p a: ?m.16442
a ∧ b: ?m.16437
b = f: ?m.16376
f a: ?m.16442
a) (f: ?m.16376
f <$> x: m α
x) :=
  hx: SatisfiesM p x
hx.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.16558
h => ⟨_: ?m.16565
_, h: ?m.16558
h, rfl: ∀ {α : Sort ?u.16582} {a : α}, a = a
rfl⟩

/--
`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.16615
m] [LawfulFunctor: (f : Type ?u.16687 → Type ?u.16686) → [inst : Functor f] → Prop
LawfulFunctor m: ?m.16615
m] {x: m α
x : m: ?m.16615
m α: ?m.16637
α}
    (hx: SatisfiesM (fun a => ?m.16803 a) x
hx : SatisfiesM: {α : Type ?u.16786} → {m : Type ?u.16786 → Type ?u.16785} → [inst : Functor m] → (α → Prop) → m α → Prop
SatisfiesM (fun a: ?m.16800
a => p: ?m.16678
p (f: ?m.16762
f a: ?m.16800
a)) x: m α
x) : SatisfiesM: {α : Type ?u.16812} → {m : Type ?u.16812 → Type ?u.16811} → [inst : Functor m] → (α → Prop) → m α → Prop
SatisfiesM p: ?m.16678
p (f: ?m.16762
f <$> x: m α
x) :=
  hx: SatisfiesM (fun a => p (f a)) x
hx.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.16929
h => h: ?m.16929
h

/-- `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.16956
m] [LawfulFunctor: (f : Type ?u.17025 → Type ?u.17024) → [inst : Functor f] → Prop
LawfulFunctor m: ?m.16956
m] {x: m α
x : m: ?m.16956
m α: ?m.16978
α}
    (hx: SatisfiesM q x
hx : SatisfiesM: {α : Type ?u.17040} → {m : Type ?u.17040 → Type ?u.17039} → [inst : Functor m] → (α → Prop) → m α → Prop
SatisfiesM q: ?m.17016
q x: m α
x) (ha: ∀ {b : α}, q b → ?m.17213
ha : ∀ {b: ?m.17207
b}, q: ?m.17016
q b: unknown metavariable '?_uniq.17116'
b → p: ?m.17069
p a: ?m.17160
a) : SatisfiesM: {α : Type ?u.17217} → {m : Type ?u.17217 → Type ?u.17216} → [inst : Functor m] → (α → Prop) → m α → Prop
SatisfiesM p: ?m.17069
p (Functor.mapConst: {f : Type ?u.17234 → Type ?u.17233} → [self : Functor f] → {α β : Type ?u.17234} → α → f β → f α
Functor.mapConst a: ?m.17160
a 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_2
m) ▸ hx: SatisfiesM q x
hx.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 a
ha

/-- `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.17411
m] [LawfulApplicative: (f : Type ?u.17420 → Type ?u.17419) → [inst : Applicative f] → Prop
LawfulApplicative m: ?m.17411
m]
    (h: unknown metavariable '?_uniq.17458'
h : p: ?m.17435
p a: ?m.17494
a) : SatisfiesM: {α : Type ?u.17521} → {m : Type ?u.17521 → Type ?u.17520} → [inst : Functor m] → (α → Prop) → m α → Prop
SatisfiesM (m := m: ?m.17411
m) p: ?m.17435
p (pure: {f : Type ?u.17531 → Type ?u.17530} → [self : Pure f] → {α : Type ?u.17531} → α → f α
pure a: ?m.17494
a) := ⟨pure: {f : Type ?u.17615 → Type ?u.17614} → [self : Pure f] → {α : Type ?u.17615} → α → f α
pure ⟨_: ?m.17641
_, h: p a
h⟩, by
Goals accomplished! 🐙 m: Type u_1 → Type u_2

α✝: Type u_1

p: α✝ → Prop

a: α✝

inst✝¹: Applicative m

inst✝: LawfulApplicative m

h: p a

Subtype.val <$> pure { val := a, property := h } = pure asimp
Goals 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.17917
m] [LawfulApplicative: (f : Type ?u.17950 → Type ?u.17949) → [inst : Applicative f] → Prop
LawfulApplicative m: ?m.17917
m] {x: m α
x : m: ?m.17917
m α: ?m.17941
α}
    (hf: SatisfiesM p₁ f
hf : SatisfiesM: {α : Type ?u.18232} → {m : Type ?u.18232 → Type ?u.18231} → [inst : Functor m] → (α → Prop) → m α → Prop
SatisfiesM p₁: ?m.17981
p₁ f: ?m.18024
f) (hx: SatisfiesM p₂ x
hx : SatisfiesM: {α : Type ?u.18266} → {m : Type ?u.18266 → Type ?u.18265} → [inst : Functor m] → (α → Prop) → m α → Prop
SatisfiesM p₂: ?m.18098
p₂ x: m α
x)
    (H: ∀ {f : ?m.18309} {a : α}, p₁ f → p₂ a → ?m.18314
H : ∀ {f: ?m.18302
f a: ?m.18305
a}, p₁: ?m.17981
p₁ f: ?m.18302
f → p₂: ?m.18098
p₂ a: ?m.18305
a → q: ?m.18206
q (f: ?m.18302
f a: ?m.18305
a)) : SatisfiesM: {α : Type ?u.18318} → {m : Type ?u.18318 → Type ?u.18317} → [inst : Functor m] → (α → Prop) → m α → Prop
SatisfiesM q: ?m.18206
q (f: ?m.18024
f <*> x: m α
x) := by
Goals accomplished! 🐙
  m: Type u_1 → Type u_2

α, α✝: Type u_1

p₁: (α → α✝) → Prop

f: m (α → α✝)

p₂: α → Prop

q: α✝ → Prop

inst✝¹: Applicative m

inst✝: LawfulApplicative m

x: m α

hf: SatisfiesM p₁ f

hx: SatisfiesM p₂ x

H: ∀ {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₁ f
hf, hx: SatisfiesM p₂ x
hx with | _, _, ⟨f: m { a // p₁ a }
f, rfl: ∀ {α : Sort ?u.18428} {a : α}, a = a
rfl⟩, ⟨x: m { a // p₂ a }
x, rfl: ∀ {α : Sort ?u.18432} {a : α}, a = a
rfl⟩ => ?_: SatisfiesM q (Seq.seq (Subtype.val <$> f) fun x_1 => Subtype.val <$> x)
?_m: Type u_1 → Type u_2

α, α✝: Type u_1

p₁: (α → α✝) → Prop

f✝: m (α → α✝)

p₂: α → Prop

q: α✝ → Prop

inst✝¹: Applicative m

inst✝: LawfulApplicative m

x✝: 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_1

p₁: (α → α✝) → Prop

f: m (α → α✝)

p₂: α → Prop

q: α✝ → Prop

inst✝¹: Applicative m

inst✝: LawfulApplicative m

x: m α

hf: SatisfiesM p₁ f

hx: SatisfiesM p₂ x

H: ∀ {f : α → α✝} {a : α}, p₁ f → p₂ a → q (f a)

SatisfiesM q (Seq.seq f fun x_1 => x)refine ⟨(fun ⟨a: α → α✝
a, h₁: p₁ a
h₁⟩ ⟨b: α
b, h₂: p₂ b
h₂⟩ => ⟨a: α → α✝
a b: α
b, H: ∀ {f : α → α✝} {a : α}, p₁ f → p₂ a → q (f a)
H h₁: p₁ a
h₁ h₂: p₂ b
h₂⟩) <$> 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_1

p₁: (α → α✝) → Prop

f✝: m (α → α✝)

p₂: α → Prop

q: α✝ → Prop

inst✝¹: Applicative m

inst✝: LawfulApplicative m

x✝: 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_1

p₁: (α → α✝) → Prop

f: m (α → α✝)

p₂: α → Prop

q: α✝ → Prop

inst✝¹: Applicative m

inst✝: LawfulApplicative m

x: m α

hf: SatisfiesM p₁ f

hx: SatisfiesM p₂ x

H: ∀ {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 <$> x
pure_seq]m: Type u_1 → Type u_2

α, α✝: Type u_1

p₁: (α → α✝) → Prop

f✝: m (α → α✝)

p₂: α → Prop

q: α✝ → Prop

inst✝¹: Applicative m

inst✝: LawfulApplicative m

x✝: 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_1

p₁: (α → α✝) → Prop

f✝: m (α → α✝)

p₂: α → Prop

q: α✝ → Prop

inst✝¹: Applicative m

inst✝: LawfulApplicative m

x✝: 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_1

p₁: (α → α✝) → Prop

f: m (α → α✝)

p₂: α → Prop

q: α✝ → Prop

inst✝¹: Applicative m

inst✝: LawfulApplicative m

x: m α

hf: SatisfiesM p₁ f

hx: SatisfiesM p₂ x

H: ∀ {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 α → Prop
SatisfiesM, 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 => x
seq_assoc]m: Type u_1 → Type u_2

α, α✝: Type u_1

p₁: (α → α✝) → Prop

f✝: m (α → α✝)

p₂: α → Prop

q: α✝ → Prop

inst✝¹: Applicative m

inst✝: LawfulApplicative m

x✝: 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_1

p₁: (α → α✝) → Prop

f: m (α → α✝)

p₂: α → Prop

q: α✝ → Prop

inst✝¹: Applicative m

inst✝: LawfulApplicative m

x: m α

hf: SatisfiesM p₁ f

hx: SatisfiesM p₂ x

H: ∀ {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 <$> x
pure_seq]m: Type u_1 → Type u_2

α, α✝: Type u_1

p₁: (α → α✝) → Prop

f✝: m (α → α✝)

p₂: α → Prop

q: α✝ → Prop

inst✝¹: Applicative m

inst✝: LawfulApplicative m

x✝: 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_1

p₁: (α → α✝) → Prop

f✝: m (α → α✝)

p₂: α → Prop

q: α✝ → Prop

inst✝¹: Applicative m

inst✝: LawfulApplicative m

x✝: 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_1

p₁: (α → α✝) → Prop

f: m (α → α✝)

p₂: α → Prop

q: α✝ → Prop

inst✝¹: Applicative m

inst✝: LawfulApplicative m

x: m α

hf: SatisfiesM p₁ f

hx: SatisfiesM p₂ x

H: ∀ {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 => x
seq_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.25597
m] [LawfulApplicative: (f : Type ?u.25670 → Type ?u.25669) → [inst : Applicative f] → Prop
LawfulApplicative m: ?m.25597
m] {x: m α
x : m: ?m.25597
m α: ?m.25621
α}
    (hf: SatisfiesM p₁ f
hf : SatisfiesM: {α : Type ?u.25730} → {m : Type ?u.25730 → Type ?u.25729} → [inst : Functor m] → (α → Prop) → m α → Prop
SatisfiesM p₁: ?m.25661
p₁ f: ?m.25704
f) (hx: SatisfiesM p₂ x
hx : SatisfiesM: {α : Type ?u.25838} → {m : Type ?u.25838 → Type ?u.25837} → [inst : Functor m] → (α → Prop) → m α → Prop
SatisfiesM p₂: ?m.25778
p₂ x: m α
x) :
    SatisfiesM: {α : Type ?u.25874} → {m : Type ?u.25874 → Type ?u.25873} → [inst : Functor m] → (α → Prop) → m α → Prop
SatisfiesM (fun c: ?m.25888
c => ∃ f: ?m.25893
f a: ?m.25898
a, p₁: ?m.25661
p₁ f: ?m.25893
f ∧ p₂: ?m.25778
p₂ a: ?m.25898
a ∧ c: ?m.25888
c = f: ?m.25893
f a: ?m.25898
a) (f: ?m.25704
f <*> x: m α
x) :=
  hf: SatisfiesM p₁ f
hf.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₂ x
hx fun  hf: ?m.26060
hf ha: ?m.26063
ha => ⟨_: ?m.26070
_, _: ?m.26084
_, hf: ?m.26060
hf, ha: ?m.26063
ha, rfl: ∀ {α : Sort ?u.26107} {a : α}, a = a
rfl⟩

/--
`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.26155
m] [LawfulApplicative: (f : Type ?u.26348 → Type ?u.26347) → [inst : Applicative f] → Prop
LawfulApplicative m: ?m.26155
m] {x: m α
x : m: ?m.26155
m α: ?m.26179
α}
    (hf: SatisfiesM (fun f => ∀ {a : ?m.26393 f}, ?m.26394 f → ?m.26395 f) f
hf : SatisfiesM: {α : Type ?u.26365} → {m : Type ?u.26365 → Type ?u.26364} → [inst : Functor m] → (α → Prop) → m α → Prop
SatisfiesM (fun f: ?m.26379
f => ∀ {a: ?m.26382
a}, p₂: ?m.26227
p₂ a: ?m.26382
a → q: ?m.26277
q (f: ?m.26379
f a: ?m.26382
a)) f: ?m.26339
f) (hx: SatisfiesM p₂ x
hx : SatisfiesM: {α : Type ?u.26419} → {m : Type ?u.26419 → Type ?u.26418} → [inst : Functor m] → (α → Prop) → m α → Prop
SatisfiesM p₂: ?m.26227
p₂ x: m α
x) :
    SatisfiesM: {α : Type ?u.26455} → {m : Type ?u.26455 → Type ?u.26454} → [inst : Functor m] → (α → Prop) → m α → Prop
SatisfiesM q: ?m.26277
q (f: ?m.26339
f <*> x: m α
x) :=
  hf: SatisfiesM (fun f => ∀ {a : α}, p₂ a → q (f a)) f
hf.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₂ x
hx fun hf: ?m.26618
hf ha: ?m.26623
ha => hf: ?m.26618
hf ha: ?m.26623
ha

/--
`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.26670
m] [LawfulApplicative: (f : Type ?u.26786 → Type ?u.26785) → [inst : Applicative f] → Prop
LawfulApplicative m: ?m.26670
m] {x: m α
x : m: ?m.26670
m α: ?m.26694
α}
    (hf: SatisfiesM p₁ f
hf : SatisfiesM: {α : Type ?u.26803} → {m : Type ?u.26803 → Type ?u.26802} → [inst : Functor m] → (α → Prop) → m α → Prop
SatisfiesM p₁: ?m.26734
p₁ f: ?m.26777
f) (hx: SatisfiesM (fun a => ∀ {f : ?m.26942}, p₁ f → ?m.26948 a) x
hx : SatisfiesM: {α : Type ?u.26921} → {m : Type ?u.26921 → Type ?u.26920} → [inst : Functor m] → (α → Prop) → m α → Prop
SatisfiesM (fun a: ?m.26935
a => ∀ {f: ?m.26938
f},