m : Type u → Type u_1
α β σ : Type u
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : StateT σ m (α → β)
x : StateT σ m α
s : σ
⊢ run
      (do
        let g ← f
        g <$> x)
      s =
    do
    let fs ← run f s
    (fun p => (Prod.fst fs p.fst, p.snd)) <$> run x fs.snd
m : Type u → Type u_1
α β σ : Type u
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : StateT σ m (α → β)
x : StateT σ m α
s : σ
⊢ run (Seq.seq f fun x_1 => x) s = do
    let fs ← run f s
    (fun p => (Prod.fst fs p.fst, p.snd)) <$> run x fs.snd
show (f >>= fun g => g <$> x).run s = _
no goals
m : Type u → Type u_1
α β σ : Type u
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : StateT σ m (α → β)
x : StateT σ m α
s : σ
⊢ run
      (do
        let g ← f
        g <$> x)
      s =
    do
    let fs ← run f s
    (fun p => (Prod.fst fs p.fst, p.snd)) <$> run x fs.snd
simp