no goals
m : Type u → Type u_1
α β σ : Type u
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β
x : StateT σ m α
s : σ
⊢ run (f <$> x) s = (fun p => (f p.fst, p.snd)) <$> run x s
simp [Functor.map, StateT.map, run, map_eq_pure_bind]