no goals
α β γ : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
x : m α
g : α → m β
f : β → γ
⊢ f <$> (x >>= g) = do
    let a ← x
    f <$> g a
rw [← bind_pure_comp, bind_assoc] <;> simp [bind_pure_comp]