-- Mathlib/.lake/packages/lean4/src/lean/Init/Control/Lawful/Instances.lean
theorem seqLeft_eq {α β ε : Type u} {m : Type u → Type v} [Monad m] [LawfulMonad m] (x : ExceptT ε m α) (y : ExceptT ε m β) : x <* y = const β <$> x <*> y

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

Tactic:
simp [run_bind]

Result:
case h
α β ε : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
x : ExceptT ε m α
y : ExceptT ε m β
⊢ (do
      let x ← x.run
      match x with
        | Except.ok x => do
          let x_1 ← y.run
          match x_1 with
            | Except.ok x_2 => pure (Except.ok x)
            | Except.error e => pure (Except.error e)
        | Except.error e => pure (Except.error e)) =
    do
    let x ← x.run
    let x ←
      match x with
        | Except.ok x => pure (Except.ok (const β x))
        | 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:
α β ε : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
x : ExceptT ε m α
y : ExceptT ε m β
x✝ : Except ε α
a✝ : α
⊢ (do
      let x ← y.run
      match x with
        | Except.ok x => pure (Except.ok a✝)
        | Except.error e => pure (Except.error e)) =
    do
    let a ← y.run
    pure (Except.map (const β a✝) a)

Tactic:
apply bind_congr

Result:
case h
α β ε : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
x : ExceptT ε m α
y : ExceptT ε m β
x✝ : Except ε α
a✝ : α
⊢ ∀ (a : Except ε β),
    (match a with
      | Except.ok x => pure (Except.ok a✝)
      | Except.error e => pure (Except.error e)) =
      pure (Except.map (const β a✝) a)

Proof state:
case h.h
α β ε : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
x : ExceptT ε m α
y : ExceptT ε m β
⊢ ∀ (a : Except ε α),
    (match a with
      | Except.ok x => do
        let x_1 ← y.run
        match x_1 with
          | Except.ok x_2 => pure (Except.ok x)
          | Except.error e => pure (Except.error e)
      | Except.error e => pure (Except.error e)) =
      do
      let x ←
        match a with
          | Except.ok x => pure (Except.ok (const β x))
          | 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
| Except.error _ => simp
| Except.ok _ =>
  simp [←bind_pure_comp]; apply bind_congr; intro b;
  cases b <;> simp [comp, Except.map, const]

Result:
no goals

Proof state:
case h
α β ε : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
x : ExceptT ε m α
y : ExceptT ε m β
⊢ (do
      let x ← x.run
      match x with
        | Except.ok x => do
          let x_1 ← y.run
          match x_1 with
            | Except.ok x_2 => pure (Except.ok x)
            | Except.error e => pure (Except.error e)
        | Except.error e => pure (Except.error e)) =
    do
    let x ← x.run
    let x ←
      match x with
        | Except.ok x => pure (Except.ok (const β x))
        | 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
α β ε : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
x : ExceptT ε m α
y : ExceptT ε m β
⊢ ∀ (a : Except ε α),
    (match a with
      | Except.ok x => do
        let x_1 ← y.run
        match x_1 with
          | Except.ok x_2 => pure (Except.ok x)
          | Except.error e => pure (Except.error e)
      | Except.error e => pure (Except.error e)) =
      do
      let x ←
        match a with
          | Except.ok x => pure (Except.ok (const β x))
          | 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:
α β ε : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
x : ExceptT ε m α
y : ExceptT ε m β
⊢ (do
      let a ← x
      let _ ← y
      pure a) =
    do
    let f ← const β <$> x
    f <$> y

Tactic:
rw [← ExceptT.bind_pure_comp]

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

Proof state:
α β ε : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
x : ExceptT ε m α
y : ExceptT ε m β
x✝ : Except ε α
a✝ : ε
⊢ (match Except.error a✝ with
    | Except.ok x => do
      let x_1 ← y.run
      match x_1 with
        | Except.ok x_2 => pure (Except.ok x)
        | Except.error e => pure (Except.error e)
    | Except.error e => pure (Except.error e)) =
    do
    let x ←
      match Except.error a✝ with
        | Except.ok x => pure (Except.ok (const β x))
        | 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:
simp

Result:
no goals

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

Tactic:
apply ext

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

Proof state:
α β ε : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
x : ExceptT ε m α
y : ExceptT ε m β
x✝ : Except ε α
a✝ : α
⊢ (match Except.ok a✝ with
    | Except.ok x => do
      let x_1 ← y.run
      match x_1 with
        | Except.ok x_2 => pure (Except.ok x)
        | Except.error e => pure (Except.error e)
    | Except.error e => pure (Except.error e)) =
    do
    let x ←
      match Except.ok a✝ with
        | Except.ok x => pure (Except.ok (const β x))
        | 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:
simp [←bind_pure_comp]

Result:
α β ε : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
x : ExceptT ε m α
y : ExceptT ε m β
x✝ : Except ε α
a✝ : α
⊢ (do
      let x ← y.run
      match x with
        | Except.ok x => pure (Except.ok a✝)
        | Except.error e => pure (Except.error e)) =
    do
    let a ← y.run
    pure (Except.map (const β a✝) a)

Proof state:
case h
α β ε : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
x : ExceptT ε m α
y : ExceptT ε m β
x✝ : Except ε α
a✝ : α
⊢ ∀ (a : Except ε β),
    (match a with
      | Except.ok x => pure (Except.ok a✝)
      | Except.error e => pure (Except.error e)) =
      pure (Except.map (const β a✝) a)

Tactic:
intro b

Result:
case h
α β ε : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
x : ExceptT ε m α
y : ExceptT ε m β
x✝ : Except ε α
a✝ : α
b : Except ε β
⊢ (match b with
    | Except.ok x => pure (Except.ok a✝)
    | Except.error e => pure (Except.error e)) =
    pure (Except.map (const β a✝) b)

Proof state:
case h
α β ε : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
x : ExceptT ε m α
y : ExceptT ε m β
x✝ : Except ε α
a✝ : α
b : Except ε β
⊢ (match b with
    | Except.ok x => pure (Except.ok a✝)
    | Except.error e => pure (Except.error e)) =
    pure (Except.map (const β a✝) b)

Tactic:
cases b <;> simp [comp, Except.map, const]

Result:
no goals