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 (SeqRight.seqRight x fun x => y) s = run (Seq.seq (const α id <$> 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 β
⊢ (SeqRight.seqRight x fun x => y) = Seq.seq (const α id <$> 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 (SeqRight.seqRight x fun x => y) s = run (Seq.seq (const α id <$> 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 (SeqRight.seqRight x fun x => y) s = run (Seq.seq (const α id <$> x) fun x => y) s
intro 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 : σ
⊢ (do
      let p ← run x s
      run y p.snd) =
    do
    let x ← run x s
    let a ← run y x.snd
    pure (a.fst, a.snd)
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 (SeqRight.seqRight x fun x => y) s = run (Seq.seq (const α id <$> x) fun x => y) s
simp [map_eq_pure_bind, const]
case h.h
m : Type u_1 → Type u_2
σ α β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
x : StateT σ m α
y : StateT σ m β
s : σ
⊢ ∀ (a : α × σ),
    run y a.snd = do
      let a ← run y a.snd
      pure (a.fst, a.snd)
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 : σ
⊢ (do
      let p ← run x s
      run y p.snd) =
    do
    let x ← run x s
    let a ← run y x.snd
    pure (a.fst, a.snd)
apply bind_congr
case h.h
m : Type u_1 → Type u_2
σ α β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
x : StateT σ m α
y : StateT σ m β
s : σ
p : α × σ
⊢ run y p.snd = do
    let a ← run y p.snd
    pure (a.fst, a.snd)
case h.h
m : Type u_1 → Type u_2
σ α β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
x : StateT σ m α
y : StateT σ m β
s : σ
⊢ ∀ (a : α × σ),
    run y a.snd = do
      let a ← run y a.snd
      pure (a.fst, a.snd)
intro p
case h.h.mk
m : Type u_1 → Type u_2
σ α β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
x : StateT σ m α
y : StateT σ m β
s : σ
fst✝ : α
snd✝ : σ
⊢ run y (fst✝, snd✝).snd = do
    let a ← run y (fst✝, snd✝).snd
    pure (a.fst, a.snd)
case h.h
m : Type u_1 → Type u_2
σ α β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
x : StateT σ m α
y : StateT σ m β
s : σ
p : α × σ
⊢ run y p.snd = do
    let a ← run y p.snd
    pure (a.fst, a.snd)
cases p
no goals
case h.h.mk
m : Type u_1 → Type u_2
σ α β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
x : StateT σ m α
y : StateT σ m β
s : σ
fst✝ : α
snd✝ : σ
⊢ run y (fst✝, snd✝).snd = do
    let a ← run y (fst✝, snd✝).snd
    pure (a.fst, a.snd)
simp [Prod.eta]