m : Type u_1 → Type u_2
α β ε : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β
x : ExceptT ε m α
⊢ run
      (mk do
        let a ← x
        match a with
          | Except.ok a => pure (Except.ok (f a))
          | Except.error e => pure (Except.error e)) =
    do
    let a ← run x
    pure (Except.map f a)
m : Type u_1 → Type u_2
α β ε : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β
x : ExceptT ε m α
⊢ run (f <$> x) = Except.map f <$> run x
simp [Functor.map, ExceptT.map, map_eq_pure_bind]
case h
m : Type u_1 → Type u_2
α β ε : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β
x : ExceptT ε m α
⊢ ∀ (a : Except ε α),
    (match a with
      | Except.ok a => pure (Except.ok (f a))
      | Except.error e => pure (Except.error e)) =
      pure (Except.map f a)
m : Type u_1 → Type u_2
α β ε : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β
x : ExceptT ε m α
⊢ run
      (mk do
        let a ← x
        match a with
          | Except.ok a => pure (Except.ok (f a))
          | Except.error e => pure (Except.error e)) =
    do
    let a ← run x
    pure (Except.map f a)
apply bind_congr
case h
m : Type u_1 → Type u_2
α β ε : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β
x : ExceptT ε m α
a : Except ε α
⊢ (match a with
    | Except.ok a => pure (Except.ok (f a))
    | Except.error e => pure (Except.error e)) =
    pure (Except.map f a)
case h
m : Type u_1 → Type u_2
α β ε : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β
x : ExceptT ε m α
⊢ ∀ (a : Except ε α),
    (match a with
      | Except.ok a => pure (Except.ok (f a))
      | Except.error e => pure (Except.error e)) =
      pure (Except.map f a)
intro a
no goals
case h
m : Type u_1 → Type u_2
α β ε : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β
x : ExceptT ε m α
a : Except ε α
⊢ (match a with
    | Except.ok a => pure (Except.ok (f a))
    | Except.error e => pure (Except.error e)) =
    pure (Except.map f a)
cases a <;> simp [Except.map]