Theorem: ExceptT.map_eq_map_errorOrApply (Dijkstra/Control/Functor/Subreg.lean)

State before:
α β ε : Type u
m : Type u → Type v
inst✝² : Monad m
inst✝¹ : LawfulMonad m
inst✝ : SubregFunctor m
f : α → β
x : ExceptT ε m α
⊢ f <$> x = errorOrApply f <$> x
Tactic:
rw [Functor.map, Applicative.toFunctor, Monad.toApplicative]
State after:
α β ε : Type u
m : Type u → Type v
inst✝² : Monad m
inst✝¹ : LawfulMonad m
inst✝ : SubregFunctor m
f : α → β
x : ExceptT ε m α
⊢ instMonadExceptT.1.1.1 f x = errorOrApply f <$> x

State before:
α β ε : Type u
m : Type u → Type v
inst✝² : Monad m
inst✝¹ : LawfulMonad m
inst✝ : SubregFunctor m
f : α → β
x : ExceptT ε m α
⊢ instMonadExceptT.1.1.1 f x = errorOrApply f <$> x
Tactic:
unfold instMonadExceptT
State after:
α β ε : Type u
m : Type u → Type v
inst✝² : Monad m
inst✝¹ : LawfulMonad m
inst✝ : SubregFunctor m
f : α → β
x : ExceptT ε m α
⊢ Monad.mk.1.1.1 f x = errorOrApply f <$> x

State before:
α β ε : Type u
m : Type u → Type v
inst✝² : Monad m
inst✝¹ : LawfulMonad m
inst✝ : SubregFunctor m
f : α → β
x : ExceptT ε m α
⊢ Monad.mk.1.1.1 f x = errorOrApply f <$> x
Tactic:
simp
State after:
α β ε : Type u
m : Type u → Type v
inst✝² : Monad m
inst✝¹ : LawfulMonad m
inst✝ : SubregFunctor m
f : α → β
x : ExceptT ε m α
⊢ ExceptT.map f x = errorOrApply f <$> x

State before:
α β ε : Type u
m : Type u → Type v
inst✝² : Monad m
inst✝¹ : LawfulMonad m
inst✝ : SubregFunctor m
f : α → β
x : ExceptT ε m α
⊢ ExceptT.map f x = errorOrApply f <$> x
Tactic:
unfold ExceptT.map
State after:
α β ε : Type u
m : Type u → Type v
inst✝² : Monad m
inst✝¹ : LawfulMonad m
inst✝ : SubregFunctor m
f : α → β
x : ExceptT ε m α
⊢ (mk do
      let a ← x
      match a with
        | Except.ok a => pure (Except.ok (f a))
        | Except.error e => pure (Except.error e)) =
    errorOrApply f <$> x

State before:
α β ε : Type u
m : Type u → Type v
inst✝² : Monad m
inst✝¹ : LawfulMonad m
inst✝ : SubregFunctor m
f : α → β
x : ExceptT ε m α
⊢ (mk do
      let a ← x
      match a with
        | Except.ok a => pure (Except.ok (f a))
        | Except.error e => pure (Except.error e)) =
    errorOrApply f <$> x
Tactic:
rw [map_eq_pure_bind]
State after:
α β ε : Type u
m : Type u → Type v
inst✝² : Monad m
inst✝¹ : LawfulMonad m
inst✝ : SubregFunctor m
f : α → β
x : ExceptT ε m α
⊢ (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 ← x
    pure (errorOrApply f a)

State before:
α β ε : Type u
m : Type u → Type v
inst✝² : Monad m
inst✝¹ : LawfulMonad m
inst✝ : SubregFunctor m
f : α → β
x : ExceptT ε m α
⊢ (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 ← x
    pure (errorOrApply f a)
Tactic:
apply bind_congr
State after:
case h
α β ε : Type u
m : Type u → Type v
inst✝² : Monad m
inst✝¹ : LawfulMonad m
inst✝ : SubregFunctor 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 (errorOrApply f a)

State before:
case h
α β ε : Type u
m : Type u → Type v
inst✝² : Monad m
inst✝¹ : LawfulMonad m
inst✝ : SubregFunctor 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 (errorOrApply f a)
Tactic:
intro e
State after:
case h
α β ε : Type u
m : Type u → Type v
inst✝² : Monad m
inst✝¹ : LawfulMonad m
inst✝ : SubregFunctor m
f : α → β
x : ExceptT ε m α
e : Except ε α
⊢ (match e with
    | Except.ok a => pure (Except.ok (f a))
    | Except.error e => pure (Except.error e)) =
    pure (errorOrApply f e)

State before:
case h
α β ε : Type u
m : Type u → Type v
inst✝² : Monad m
inst✝¹ : LawfulMonad m
inst✝ : SubregFunctor m
f : α → β
x : ExceptT ε m α
e : Except ε α
⊢ (match e with
    | Except.ok a => pure (Except.ok (f a))
    | Except.error e => pure (Except.error e)) =
    pure (errorOrApply f e)
Tactic:
cases e <;> rfl
State after:
no goals