Theorem: DijkstraMonad.Push.deq (Dijkstra/Control/Monad/Dijkstra.lean)

State before:
W₁ : Type u → Type v₁
inst✝¹ : Monad W₁
W₂ : Type u → Type v₂
inst✝ : Monad W₂
F : MonadHom W₁ W₂
M : (α : Type u) → W₁ α → Type w
α : Type u
wa₂ wa₂' : W₂ α
base : W₁ α
body✝ : M α base
hx : MonadHom.app F base = wa₂
hy : MonadHom.app F base = wa₂'
⊢ DEq (Push F M α) { base := base, body := body✝, underly := hx } { base := base, body := body✝, underly := hy }
Tactic:
cases (Eq.trans hy.symm hx)
State after:
case refl
W₁ : Type u → Type v₁
inst✝¹ : Monad W₁
W₂ : Type u → Type v₂
inst✝ : Monad W₂
F : MonadHom W₁ W₂
M : (α : Type u) → W₁ α → Type w
α : Type u
wa₂ : W₂ α
base : W₁ α
body✝ : M α base
hx hy : MonadHom.app F base = wa₂
⊢ DEq (Push F M α) { base := base, body := body✝, underly := hx } { base := base, body := body✝, underly := hy }

State before:
case refl
W₁ : Type u → Type v₁
inst✝¹ : Monad W₁
W₂ : Type u → Type v₂
inst✝ : Monad W₂
F : MonadHom W₁ W₂
M : (α : Type u) → W₁ α → Type w
α : Type u
wa₂ : W₂ α
base : W₁ α
body✝ : M α base
hx hy : MonadHom.app F base = wa₂
⊢ DEq (Push F M α) { base := base, body := body✝, underly := hx } { base := base, body := body✝, underly := hy }
Tactic:
exact DEq.refl _
State after:
no goals