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

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

Tactic:
show (x >>= fun _ => y) = (const α id <$> x) >>= fun f => f <$> y

Result:
m : Type u_1 → Type u_2
ε α β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
x : ExceptT ε m α
y : ExceptT ε m β
⊢ (do
      let _ ← x
      y) =
    do
    let f ← const α id <$> x
    f <$> y

Proof state:
m : Type u_1 → Type u_2
ε α β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
x : ExceptT ε m α
y : ExceptT ε m β
⊢ (do
      let _ ← x
      y) =
    do
    let f ← x >>= pure ∘ const α id
    f <$> y

Tactic:
apply ext

Result:
case h
m : Type u_1 → Type u_2
ε α β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
x : ExceptT ε m α
y : ExceptT ε m β
⊢ (do
        let _ ← x
        y).run =
    (do
        let f ← x >>= pure ∘ const α id
        f <$> y).run

Proof state:
case h.h
m : Type u_1 → Type u_2
ε α β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
x : ExceptT ε m α
y : ExceptT ε m β
⊢ ∀ (a : Except ε α),
    (match a with
      | Except.ok x => y.run
      | Except.error e => pure (Except.error e)) =
      do
      let x ←
        match a with
          | Except.ok x => pure (Except.ok id)
          | Except.error e => pure (Except.error e)
      match x with
        | Except.ok x => Except.map x <$> y.run
        | Except.error e => pure (Except.error e)

Tactic:
intro a

Result:
case h.h
m : Type u_1 → Type u_2
ε α β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
x : ExceptT ε m α
y : ExceptT ε m β
a : Except ε α
⊢ (match a with
    | Except.ok x => y.run
    | Except.error e => pure (Except.error e)) =
    do
    let x ←
      match a with
        | Except.ok x => pure (Except.ok id)
        | Except.error e => pure (Except.error e)
    match x with
      | Except.ok x => Except.map x <$> y.run
      | Except.error e => pure (Except.error e)

Proof state:
case h
m : Type u_1 → Type u_2
ε α β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
x : ExceptT ε m α
y : ExceptT ε m β
⊢ (do
      let x ← x.run
      match x with
        | Except.ok x => y.run
        | Except.error e => pure (Except.error e)) =
    do
    let x ← x.run
    let x ←
      match x with
        | Except.ok x => pure (Except.ok id)
        | Except.error e => pure (Except.error e)
    match x with
      | Except.ok x => Except.map x <$> y.run
      | Except.error e => pure (Except.error e)

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 : ExceptT ε m α
y : ExceptT ε m β
⊢ ∀ (a : Except ε α),
    (match a with
      | Except.ok x => y.run
      | Except.error e => pure (Except.error e)) =
      do
      let x ←
        match a with
          | Except.ok x => pure (Except.ok id)
          | Except.error e => pure (Except.error e)
      match x with
        | Except.ok x => Except.map x <$> y.run
        | Except.error e => pure (Except.error e)

Proof state:
m : Type u_1 → Type u_2
ε α β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
x : ExceptT ε m α
y : ExceptT ε m β
⊢ (do
      let _ ← x
      y) =
    do
    let f ← const α id <$> x
    f <$> y

Tactic:
rw [← ExceptT.bind_pure_comp]

Result:
m : Type u_1 → Type u_2
ε α β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
x : ExceptT ε m α
y : ExceptT ε m β
⊢ (do
      let _ ← x
      y) =
    do
    let f ← x >>= pure ∘ const α id
    f <$> y

Proof state:
case h
m : Type u_1 → Type u_2
ε α β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
x : ExceptT ε m α
y : ExceptT ε m β
⊢ (do
        let _ ← x
        y).run =
    (do
        let f ← x >>= pure ∘ const α id
        f <$> y).run

Tactic:
simp [run_bind]

Result:
case h
m : Type u_1 → Type u_2
ε α β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
x : ExceptT ε m α
y : ExceptT ε m β
⊢ (do
      let x ← x.run
      match x with
        | Except.ok x => y.run
        | Except.error e => pure (Except.error e)) =
    do
    let x ← x.run
    let x ←
      match x with
        | Except.ok x => pure (Except.ok id)
        | Except.error e => pure (Except.error e)
    match x with
      | Except.ok x => Except.map x <$> y.run
      | Except.error e => pure (Except.error e)

Proof state:
case h.h
m : Type u_1 → Type u_2
ε α β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
x : ExceptT ε m α
y : ExceptT ε m β
a : Except ε α
⊢ (match a with
    | Except.ok x => y.run
    | Except.error e => pure (Except.error e)) =
    do
    let x ←
      match a with
        | Except.ok x => pure (Except.ok id)
        | Except.error e => pure (Except.error e)
    match x with
      | Except.ok x => Except.map x <$> y.run
      | Except.error e => pure (Except.error e)

Tactic:
cases a <;> simp

Result:
no goals