Theorem: MonadHom.naturality (Dijkstra/Control/Monad/Hom.lean)

State before:
m : Type u → Type v
inst✝³ : Monad m
inst✝² : LawfulMonad m
n : Type u → Type w
inst✝¹ : Monad n
inst✝ : LawfulMonad n
F : MonadHom m n
α β : Type u
f : α → β
⊢ app F ∘ Functor.map f = Functor.map f ∘ app F
Tactic:
funext x
State after:
case h
m : Type u → Type v
inst✝³ : Monad m
inst✝² : LawfulMonad m
n : Type u → Type w
inst✝¹ : Monad n
inst✝ : LawfulMonad n
F : MonadHom m n
α β : Type u
f : α → β
x : m α
⊢ (app F ∘ Functor.map f) x = (Functor.map f ∘ app F) x

State before:
case h
m : Type u → Type v
inst✝³ : Monad m
inst✝² : LawfulMonad m
n : Type u → Type w
inst✝¹ : Monad n
inst✝ : LawfulMonad n
F : MonadHom m n
α β : Type u
f : α → β
x : m α
⊢ (app F ∘ Functor.map f) x = (Functor.map f ∘ app F) x
Tactic:
dsimp
State after:
case h
m : Type u → Type v
inst✝³ : Monad m
inst✝² : LawfulMonad m
n : Type u → Type w
inst✝¹ : Monad n
inst✝ : LawfulMonad n
F : MonadHom m n
α β : Type u
f : α → β
x : m α
⊢ app F (f <$> x) = f <$> app F x

State before:
case h
m : Type u → Type v
inst✝³ : Monad m
inst✝² : LawfulMonad m
n : Type u → Type w
inst✝¹ : Monad n
inst✝ : LawfulMonad n
F : MonadHom m n
α β : Type u
f : α → β
x : m α
⊢ app F (f <$> x) = f <$> app F x
Tactic:
conv =>
  lhs; rw [map_eq_pure_bind, F.app_bind]; rhs; ext a; dsimp; rw [F.app_pure]
State after:
case h
m : Type u → Type v
inst✝³ : Monad m
inst✝² : LawfulMonad m
n : Type u → Type w
inst✝¹ : Monad n
inst✝ : LawfulMonad n
F : MonadHom m n
α β : Type u
f : α → β
x : m α
⊢ (do
      let a ← app F x
      pure (f a)) =
    f <$> app F x

State before:
case h
m : Type u → Type v
inst✝³ : Monad m
inst✝² : LawfulMonad m
n : Type u → Type w
inst✝¹ : Monad n
inst✝ : LawfulMonad n
F : MonadHom m n
α β : Type u
f : α → β
x : m α
⊢ (do
      let a ← app F x
      pure (f a)) =
    f <$> app F x
Tactic:
rw [map_eq_pure_bind]
State after:
no goals