case h
m : Type u_1 → Type u_2
σ α β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
x : StateT σ m α
y : StateT σ m β
⊢ ∀ (s : σ), run (SeqLeft.seqLeft x fun x => y) s = run (Seq.seq (const β <$> x) fun x => y) s
m : Type u_1 → Type u_2
σ α β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
x : StateT σ m α
y : StateT σ m β
⊢ (SeqLeft.seqLeft x fun x => y) = Seq.seq (const β <$> x) fun x => y
apply ext
case h
m : Type u_1 → Type u_2
σ α β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
x : StateT σ m α
y : StateT σ m β
s : σ
⊢ run (SeqLeft.seqLeft x fun x => y) s = run (Seq.seq (const β <$> x) fun x => y) s
case h
m : Type u_1 → Type u_2
σ α β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
x : StateT σ m α
y : StateT σ m β
⊢ ∀ (s : σ), run (SeqLeft.seqLeft x fun x => y) s = run (Seq.seq (const β <$> x) fun x => y) s
intro s
no goals
case h
m : Type u_1 → Type u_2
σ α β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
x : StateT σ m α
y : StateT σ m β
s : σ
⊢ run (SeqLeft.seqLeft x fun x => y) s = run (Seq.seq (const β <$> x) fun x => y) s
simp [map_eq_pure_bind]