Theorem: DijkstraMonad.dbind_congr (Dijkstra/Control/Monad/Dijkstra.lean)

State before:
W : Type u → Type v
inst✝¹ : Monad W
M : (α : Type u) → W α → Type w
inst✝ : DijkstraMonad W M
α β : Type u
a✝ : W α
wf₁ wf₂ : α → W β
x✝ : M α a✝
f₁ : (a : α) → M β (wf₁ a)
f₂ : (a : α) → M β (wf₂ a)
hf : ∀ (a : α), DEq (M β) (f₁ a) (f₂ a)
⊢ DEq (M β) (dbind x✝ f₁) (dbind x✝ f₂)
Tactic:
have : wf₁ = wf₂ := by
  funext a
  exact (hf a).eq_param
State after:
W : Type u → Type v
inst✝¹ : Monad W
M : (α : Type u) → W α → Type w
inst✝ : DijkstraMonad W M
α β : Type u
a✝ : W α
wf₁ wf₂ : α → W β
x✝ : M α a✝
f₁ : (a : α) → M β (wf₁ a)
f₂ : (a : α) → M β (wf₂ a)
hf : ∀ (a : α), DEq (M β) (f₁ a) (f₂ a)
this : wf₁ = wf₂
⊢ DEq (M β) (dbind x✝ f₁) (dbind x✝ f₂)

State before:
W : Type u → Type v
inst✝¹ : Monad W
M : (α : Type u) → W α → Type w
inst✝ : DijkstraMonad W M
α β : Type u
a✝ : W α
wf₁ wf₂ : α → W β
x✝ : M α a✝
f₁ : (a : α) → M β (wf₁ a)
f₂ : (a : α) → M β (wf₂ a)
hf : ∀ (a : α), DEq (M β) (f₁ a) (f₂ a)
this : wf₁ = wf₂
⊢ DEq (M β) (dbind x✝ f₁) (dbind x✝ f₂)
Tactic:
cases this
State after:
case refl
W : Type u → Type v
inst✝¹ : Monad W
M : (α : Type u) → W α → Type w
inst✝ : DijkstraMonad W M
α β : Type u
a✝ : W α
wf₁ : α → W β
x✝ : M α a✝
f₁ f₂ : (a : α) → M β (wf₁ a)
hf : ∀ (a : α), DEq (M β) (f₁ a) (f₂ a)
⊢ DEq (M β) (dbind x✝ f₁) (dbind x✝ f₂)

State before:
case refl
W : Type u → Type v
inst✝¹ : Monad W
M : (α : Type u) → W α → Type w
inst✝ : DijkstraMonad W M
α β : Type u
a✝ : W α
wf₁ : α → W β
x✝ : M α a✝
f₁ f₂ : (a : α) → M β (wf₁ a)
hf : ∀ (a : α), DEq (M β) (f₁ a) (f₂ a)
⊢ DEq (M β) (dbind x✝ f₁) (dbind x✝ f₂)
Tactic:
have : f₁ = f₂ := by
  funext a
  exact (hf a).eq_of_deq
State after:
case refl
W : Type u → Type v
inst✝¹ : Monad W
M : (α : Type u) → W α → Type w
inst✝ : DijkstraMonad W M
α β : Type u
a✝ : W α
wf₁ : α → W β
x✝ : M α a✝
f₁ f₂ : (a : α) → M β (wf₁ a)
hf : ∀ (a : α), DEq (M β) (f₁ a) (f₂ a)
this : f₁ = f₂
⊢ DEq (M β) (dbind x✝ f₁) (dbind x✝ f₂)

State before:
case refl
W : Type u → Type v
inst✝¹ : Monad W
M : (α : Type u) → W α → Type w
inst✝ : DijkstraMonad W M
α β : Type u
a✝ : W α
wf₁ : α → W β
x✝ : M α a✝
f₁ f₂ : (a : α) → M β (wf₁ a)
hf : ∀ (a : α), DEq (M β) (f₁ a) (f₂ a)
this : f₁ = f₂
⊢ DEq (M β) (dbind x✝ f₁) (dbind x✝ f₂)
Tactic:
cases this
State after:
case refl.refl
W : Type u → Type v
inst✝¹ : Monad W
M : (α : Type u) → W α → Type w
inst✝ : DijkstraMonad W M
α β : Type u
a✝ : W α
wf₁ : α → W β
x✝ : M α a✝
f₁ : (a : α) → M β (wf₁ a)
hf : ∀ (a : α), DEq (M β) (f₁ a) (f₁ a)
⊢ DEq (M β) (dbind x✝ f₁) (dbind x✝ f₁)

State before:
case refl.refl
W : Type u → Type v
inst✝¹ : Monad W
M : (α : Type u) → W α → Type w
inst✝ : DijkstraMonad W M
α β : Type u
a✝ : W α
wf₁ : α → W β
x✝ : M α a✝
f₁ : (a : α) → M β (wf₁ a)
hf : ∀ (a : α), DEq (M β) (f₁ a) (f₁ a)
⊢ DEq (M β) (dbind x✝ f₁) (dbind x✝ f₁)
Tactic:
exact DEq.refl _
State after:
no goals

State before:
W : Type u → Type v
inst✝¹ : Monad W
M : (α : Type u) → W α → Type w
inst✝ : DijkstraMonad W M
α β : Type u
a✝ : W α
wf₁ wf₂ : α → W β
x✝ : M α a✝
f₁ : (a : α) → M β (wf₁ a)
f₂ : (a : α) → M β (wf₂ a)
hf : ∀ (a : α), DEq (M β) (f₁ a) (f₂ a)
⊢ wf₁ = wf₂
Tactic:
funext a
State after:
case h
W : Type u → Type v
inst✝¹ : Monad W
M : (α : Type u) → W α → Type w
inst✝ : DijkstraMonad W M
α β : Type u
a✝ : W α
wf₁ wf₂ : α → W β
x✝ : M α a✝
f₁ : (a : α) → M β (wf₁ a)
f₂ : (a : α) → M β (wf₂ a)
hf : ∀ (a : α), DEq (M β) (f₁ a) (f₂ a)
a : α
⊢ wf₁ a = wf₂ a

State before:
case h
W : Type u → Type v
inst✝¹ : Monad W
M : (α : Type u) → W α → Type w
inst✝ : DijkstraMonad W M
α β : Type u
a✝ : W α
wf₁ wf₂ : α → W β
x✝ : M α a✝
f₁ : (a : α) → M β (wf₁ a)
f₂ : (a : α) → M β (wf₂ a)
hf : ∀ (a : α), DEq (M β) (f₁ a) (f₂ a)
a : α
⊢ wf₁ a = wf₂ a
Tactic:
exact (hf a).eq_param
State after:
no goals

State before:
W : Type u → Type v
inst✝¹ : Monad W
M : (α : Type u) → W α → Type w
inst✝ : DijkstraMonad W M
α β : Type u
a✝ : W α
wf₁ : α → W β
x✝ : M α a✝
f₁ f₂ : (a : α) → M β (wf₁ a)
hf : ∀ (a : α), DEq (M β) (f₁ a) (f₂ a)
⊢ f₁ = f₂
Tactic:
funext a
State after:
case h
W : Type u → Type v
inst✝¹ : Monad W
M : (α : Type u) → W α → Type w
inst✝ : DijkstraMonad W M
α β : Type u
a✝ : W α
wf₁ : α → W β
x✝ : M α a✝
f₁ f₂ : (a : α) → M β (wf₁ a)
hf : ∀ (a : α), DEq (M β) (f₁ a) (f₂ a)
a : α
⊢ f₁ a = f₂ a

State before:
case h
W : Type u → Type v
inst✝¹ : Monad W
M : (α : Type u) → W α → Type w
inst✝ : DijkstraMonad W M
α β : Type u
a✝ : W α
wf₁ : α → W β
x✝ : M α a✝
f₁ f₂ : (a : α) → M β (wf₁ a)
hf : ∀ (a : α), DEq (M β) (f₁ a) (f₂ a)
a : α
⊢ f₁ a = f₂ a
Tactic:
exact (hf a).eq_of_deq
State after:
no goals