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

State before:
m : Type u → Type v
inst✝¹ : Monad m
n : Type u → Type w
inst✝ : Monad n
F G : MonadHom m n
h : ∀ {α : Type u} (x : m α), app F x = app G x
⊢ F = G
Tactic:
apply MonadHom.eq (m:=m)
State after:
m : Type u → Type v
inst✝¹ : Monad m
n : Type u → Type w
inst✝ : Monad n
F G : MonadHom m n
h : ∀ {α : Type u} (x : m α), app F x = app G x
⊢ F.app = G.app

State before:
m : Type u → Type v
inst✝¹ : Monad m
n : Type u → Type w
inst✝ : Monad n
F G : MonadHom m n
h : ∀ {α : Type u} (x : m α), app F x = app G x
⊢ F.app = G.app
Tactic:
funext _ x
State after:
case h.h
m : Type u → Type v
inst✝¹ : Monad m
n : Type u → Type w
inst✝ : Monad n
F G : MonadHom m n
h : ∀ {α : Type u} (x : m α), app F x = app G x
x✝ : Type u
x : m x✝
⊢ app F x = app G x

State before:
case h.h
m : Type u → Type v
inst✝¹ : Monad m
n : Type u → Type w
inst✝ : Monad n
F G : MonadHom m n
h : ∀ {α : Type u} (x : m α), app F x = app G x
x✝ : Type u
x : m x✝
⊢ app F x = app G x
Tactic:
exact h x
State after:
no goals