m : Type u_1 → Type u_2
ε α β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
x : ExceptT ε m α
y : ExceptT ε m β
⊢ (do
      let _ ← x
      y) =
    do
    let f ← const α id <$> x
    f <$> y
m : Type u_1 → Type u_2
ε α β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
x : ExceptT ε m α
y : ExceptT ε m β
⊢ (SeqRight.seqRight x fun x => y) = Seq.seq (const α id <$> x) fun x => y
show (x >>= fun _ => y) = (const α id <$> x) >>= fun f => f <$> y
m : Type u_1 → Type u_2
ε α β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
x : ExceptT ε m α
y : ExceptT ε m β
⊢ (do
      let _ ← x
      y) =
    do
    let f ← x >>= pure ∘ const α id
    f <$> y
m : Type u_1 → Type u_2
ε α β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
x : ExceptT ε m α
y : ExceptT ε m β
⊢ (do
      let _ ← x
      y) =
    do
    let f ← const α id <$> x
    f <$> y
rw [← ExceptT.bind_pure_comp]
case h
m : Type u_1 → Type u_2
ε α β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
x : ExceptT ε m α
y : ExceptT ε m β
⊢ (run do
      let _ ← x
      y) =
    run do
      let f ← x >>= pure ∘ const α id
      f <$> y
m : Type u_1 → Type u_2
ε α β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
x : ExceptT ε m α
y : ExceptT ε m β
⊢ (do
      let _ ← x
      y) =
    do
    let f ← x >>= pure ∘ const α id
    f <$> y
apply ext
case h
m : Type u_1 → Type u_2
ε α β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
x : ExceptT ε m α
y : ExceptT ε m β
⊢ (do
      let x ← run x
      match x with
        | Except.ok x => run y
        | Except.error e => pure (Except.error e)) =
    do
    let x ← run x
    let x ←
      match x with
        | Except.ok x => pure (Except.ok id)
        | Except.error e => pure (Except.error e)
    match x with
      | Except.ok x => Except.map x <$> run y
      | Except.error e => pure (Except.error e)
case h
m : Type u_1 → Type u_2
ε α β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
x : ExceptT ε m α
y : ExceptT ε m β
⊢ (run do
      let _ ← x
      y) =
    run do
      let f ← x >>= pure ∘ const α id
      f <$> y
simp [run_bind]
case h.h
m : Type u_1 → Type u_2
ε α β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
x : ExceptT ε m α
y : ExceptT ε m β
⊢ ∀ (a : Except ε α),
    (match a with
      | Except.ok x => run y
      | Except.error e => pure (Except.error e)) =
      do
      let x ←
        match a with
          | Except.ok x => pure (Except.ok id)
          | Except.error e => pure (Except.error e)
      match x with
        | Except.ok x => Except.map x <$> run y
        | Except.error e => pure (Except.error e)
case h
m : Type u_1 → Type u_2
ε α β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
x : ExceptT ε m α
y : ExceptT ε m β
⊢ (do
      let x ← run x
      match x with
        | Except.ok x => run y
        | Except.error e => pure (Except.error e)) =
    do
    let x ← run x
    let x ←
      match x with
        | Except.ok x => pure (Except.ok id)
        | Except.error e => pure (Except.error e)
    match x with
      | Except.ok x => Except.map x <$> run y
      | Except.error e => pure (Except.error e)
apply bind_congr
case h.h
m : Type u_1 → Type u_2
ε α β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
x : ExceptT ε m α
y : ExceptT ε m β
a : Except ε α
⊢ (match a with
    | Except.ok x => run y
    | Except.error e => pure (Except.error e)) =
    do
    let x ←
      match a with
        | Except.ok x => pure (Except.ok id)
        | Except.error e => pure (Except.error e)
    match x with
      | Except.ok x => Except.map x <$> run y
      | Except.error e => pure (Except.error e)
case h.h
m : Type u_1 → Type u_2
ε α β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
x : ExceptT ε m α
y : ExceptT ε m β
⊢ ∀ (a : Except ε α),
    (match a with
      | Except.ok x => run y
      | Except.error e => pure (Except.error e)) =
      do
      let x ←
        match a with
          | Except.ok x => pure (Except.ok id)
          | Except.error e => pure (Except.error e)
      match x with
        | Except.ok x => Except.map x <$> run y
        | Except.error e => pure (Except.error e)
intro a
no goals
case h.h
m : Type u_1 → Type u_2
ε α β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
x : ExceptT ε m α
y : ExceptT ε m β
a : Except ε α
⊢ (match a with
    | Except.ok x => run y
    | Except.error e => pure (Except.error e)) =
    do
    let x ←
      match a with
        | Except.ok x => pure (Except.ok id)
        | Except.error e => pure (Except.error e)
    match x with
      | Except.ok x => Except.map x <$> run y
      | Except.error e => pure (Except.error e)
cases a <;> simp