Theorem: map_bind (Dijkstra/Control/Lawful.lean)

State before:
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α β γ : Type u
f : α → β
x : m α
g : β → m γ
⊢ f <$> x >>= g = x >>= g ∘ f
Tactic:
rw [map_eq_pure_bind, bind_assoc]
State after:
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α β γ : Type u
f : α → β
x : m α
g : β → m γ
⊢ (x >>= fun x => pure (f x) >>= g) = x >>= g ∘ f

State before:
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α β γ : Type u
f : α → β
x : m α
g : β → m γ
⊢ (x >>= fun x => pure (f x) >>= g) = x >>= g ∘ f
Tactic:
apply bind_congr
State after:
case h
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α β γ : Type u
f : α → β
x : m α
g : β → m γ
⊢ ∀ (a : α), pure (f a) >>= g = (g ∘ f) a

State before:
case h
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α β γ : Type u
f : α → β
x : m α
g : β → m γ
⊢ ∀ (a : α), pure (f a) >>= g = (g ∘ f) a
Tactic:
intro a
State after:
case h
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α β γ : Type u
f : α → β
x : m α
g : β → m γ
a : α
⊢ pure (f a) >>= g = (g ∘ f) a

State before:
case h
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α β γ : Type u
f : α → β
x : m α
g : β → m γ
a : α
⊢ pure (f a) >>= g = (g ∘ f) a
Tactic:
rw [pure_bind]
State after:
case h
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α β γ : Type u
f : α → β
x : m α
g : β → m γ
a : α
⊢ g (f a) = (g ∘ f) a

State before:
case h
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α β γ : Type u
f : α → β
x : m α
g : β → m γ
a : α
⊢ g (f a) = (g ∘ f) a
Tactic:
rfl
State after:
no goals