α β ε : 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
α β ε : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
x : ExceptT ε m α
y : ExceptT ε m β
⊢ (SeqLeft.seqLeft x fun x => y) = Seq.seq (const β <$> x) fun x => y
show (x >>= fun a => y >>= fun _ => pure a) = (const (α := α) β <$> x) >>= fun f => f <$> y
α β ε : 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
α β ε : 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
rw [← ExceptT.bind_pure_comp]
case h
α β ε : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
x : ExceptT ε m α
y : ExceptT ε m β
⊢ (run do
      let a ← x
      let _ ← y
      pure a) =
    run do
      let f ← x >>= pure ∘ const β
      f <$> y
α β ε : 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
apply ext
case h
α β ε : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
x : ExceptT ε m α
y : ExceptT ε m β
⊢ (do
      let x ← run x
      match x with
        | Except.ok x => do
          let x_1 ← run y
          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 ← run x
    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 <$> run y
      | Except.error e => pure (Except.error e)
case h
α β ε : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
x : ExceptT ε m α
y : ExceptT ε m β
⊢ (run do
      let a ← x
      let _ ← y
      pure a) =
    run do
      let f ← x >>= pure ∘ const β
      f <$> y
simp [run_bind]
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 ← run y
        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 <$> run y
        | Except.error e => pure (Except.error e)
case h
α β ε : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
x : ExceptT ε m α
y : ExceptT ε m β
⊢ (do
      let x ← run x
      match x with
        | Except.ok x => do
          let x_1 ← run y
          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 ← run x
    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 <$> run y
      | Except.error e => pure (Except.error e)
apply bind_congr
no goals
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 ← run y
        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 <$> run y
        | Except.error e => pure (Except.error e)
intro
| Except.error _ => simp
| Except.ok _ =>
  simp [map_eq_pure_bind]; apply bind_congr; intro b;
  cases b <;> simp [comp, Except.map, const]
no goals
α β ε : 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 ← run y
      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 <$> run y
      | Except.error e => pure (Except.error e)
simp
α β ε : 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 ← run y
      match x with
        | Except.ok x => pure (Except.ok a✝)
        | Except.error e => pure (Except.error e)) =
    do
    let a ← run y
    pure (Except.map (const β a✝) a)
α β ε : 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 ← run y
      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 <$> run y
      | Except.error e => pure (Except.error e)
simp [map_eq_pure_bind]
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)
α β ε : 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 ← run y
      match x with
        | Except.ok x => pure (Except.ok a✝)
        | Except.error e => pure (Except.error e)) =
    do
    let a ← run y
    pure (Except.map (const β a✝) a)
apply bind_congr
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)
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)
intro b
no goals
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)
cases b <;> simp [comp, Except.map, const]