-- Mathlib/.lake/packages/lean4/src/lean/Init/Control/Lawful/Instances.lean
theorem seqRight_eq [Monad m] [LawfulMonad m] (x : StateT σ m α) (y : StateT σ m β) : x *> y = const α id <$> x <*> y

Proof state:
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 : σ), (x *> y).run s = (const α id <$> x <*> y).run s

Tactic:
intro s

Result:
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 : σ
⊢ (x *> y).run s = (const α id <$> x <*> y).run s

Proof state:
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 ← x.run s
      y.run p.snd) =
    do
    let x ← x.run s
    let a ← y.run x.snd
    pure (a.fst, a.snd)

Tactic:
apply bind_congr

Result:
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 : α × σ),
    y.run a.snd = do
      let a ← y.run a.snd
      pure (a.fst, a.snd)

Proof state:
m : Type u_1 → Type u_2
σ α β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
x : StateT σ m α
y : StateT σ m β
⊢ x *> y = const α id <$> x <*> y

Tactic:
apply ext

Result:
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 : σ), (x *> y).run s = (const α id <$> x <*> y).run s

Proof state:
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 : σ
⊢ (x *> y).run s = (const α id <$> x <*> y).run s

Tactic:
simp [←bind_pure_comp, const]

Result:
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 ← x.run s
      y.run p.snd) =
    do
    let x ← x.run s
    let a ← y.run x.snd
    pure (a.fst, a.snd)

Proof state:
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 : α × σ),
    y.run a.snd = do
      let a ← y.run a.snd
      pure (a.fst, a.snd)

Tactic:
intro p

Result:
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 : α × σ
⊢ y.run p.snd = do
    let a ← y.run p.snd
    pure (a.fst, a.snd)

Proof state:
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✝ : σ
⊢ y.run (fst✝, snd✝).snd = do
    let a ← y.run (fst✝, snd✝).snd
    pure (a.fst, a.snd)

Tactic:
simp [Prod.eta]

Result:
no goals

Proof state:
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 : α × σ
⊢ y.run p.snd = do
    let a ← y.run p.snd
    pure (a.fst, a.snd)

Tactic:
cases p

Result:
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✝ : σ
⊢ y.run (fst✝, snd✝).snd = do
    let a ← y.run (fst✝, snd✝).snd
    pure (a.fst, a.snd)