internlm/Lean-Github huggingface dataset:
Theorem: interpUB_bind
Proof state before:
case Vis
T R : Type
k : T → Fitree UBE R
T✝ : Type
e✝ : UBE T✝
k✝ : T✝ → Fitree UBE T
ih :
  ∀ (a : T✝),
    interpUB (Fitree.bind (k✝ a) k) =
      Fitree.bind (interpUB (k✝ a)) fun x =>
        match x with
        | Except.error ε => Fitree.ret (Except.error ε)
        | Except.ok x => interpUB (k x)
⊢ interpUB (Fitree.bind (Fitree.Vis e✝ k✝) k) =
    Fitree.bind (interpUB (Fitree.Vis e✝ k✝)) fun x =>
      match x with
      | Except.error ε => Fitree.ret (Except.error ε)
      | Except.ok x => interpUB (k x)
Tactic:
simp [interpUB, Fitree.interpExcept] at *
Proof state after:
case Vis
T R : Type
k : T → Fitree UBE R
T✝ : Type
e✝ : UBE T✝
k✝ : T✝ → Fitree UBE T
ih :
  ∀ (a : T✝),
    Fitree.interp UBE.handle (Fitree.bind (k✝ a) k) =
      Fitree.bind (Fitree.interp UBE.handle (k✝ a)) fun x =>
        match x with
        | Except.error ε => Fitree.ret (Except.error ε)
        | Except.ok x => Fitree.interp UBE.handle (k x)
⊢ Fitree.interp UBE.handle (Fitree.bind (Fitree.Vis e✝ k✝) k) =
    Fitree.bind (Fitree.interp UBE.handle (Fitree.Vis e✝ k✝)) fun x =>
      match x with
      | Except.error ε => Fitree.ret (Except.error ε)
      | Except.ok x => Fitree.interp UBE.handle (k x)
Theorem: interpUB_bind
Proof state before:
case Vis
T R : Type
k : T → Fitree UBE R
T✝ : Type
e✝ : UBE T✝
k✝ : T✝ → Fitree UBE T
ih :
  ∀ (a : T✝),
    Fitree.interp UBE.handle (Fitree.bind (k✝ a) k) =
      Fitree.bind (Fitree.interp UBE.handle (k✝ a)) fun x =>
        match x with
        | Except.error ε => Fitree.ret (Except.error ε)
        | Except.ok x => Fitree.interp UBE.handle (k x)
⊢ Fitree.interp UBE.handle (Fitree.bind (Fitree.Vis e✝ k✝) k) =
    Fitree.bind (Fitree.interp UBE.handle (Fitree.Vis e✝ k✝)) fun x =>
      match x with
      | Except.error ε => Fitree.ret (Except.error ε)
      | Except.ok x => Fitree.interp UBE.handle (k x)
Tactic:
simp [Fitree.interp, Fitree.bind, Bind.bind]
Proof state after:
case Vis
T R : Type
k : T → Fitree UBE R
T✝ : Type
e✝ : UBE T✝
k✝ : T✝ → Fitree UBE T
ih :
  ∀ (a : T✝),
    Fitree.interp UBE.handle (Fitree.bind (k✝ a) k) =
      Fitree.bind (Fitree.interp UBE.handle (k✝ a)) fun x =>
        match x with
        | Except.error ε => Fitree.ret (Except.error ε)
        | Except.ok x => Fitree.interp UBE.handle (k x)
⊢ Fitree.bind (UBE.handle T✝ e✝) (ExceptT.bindCont fun t => Fitree.interp UBE.handle (Fitree.bind (k✝ t) k)) =
    Fitree.bind (UBE.handle T✝ e✝) fun x =>
      Fitree.bind (ExceptT.bindCont (fun t => Fitree.interp UBE.handle (k✝ t)) x) fun x =>
        match x with
        | Except.error ε => Fitree.ret (Except.error ε)
        | Except.ok x => Fitree.interp UBE.handle (k x)
Theorem: interpUB_bind
Proof state before:
case Vis
T R : Type
k : T → Fitree UBE R
T✝ : Type
e✝ : UBE T✝
k✝ : T✝ → Fitree UBE T
ih :
  ∀ (a : T✝),
    Fitree.interp UBE.handle (Fitree.bind (k✝ a) k) =
      Fitree.bind (Fitree.interp UBE.handle (k✝ a)) fun x =>
        match x with
        | Except.error ε => Fitree.ret (Except.error ε)
        | Except.ok x => Fitree.interp UBE.handle (k x)
⊢ Fitree.bind (UBE.handle T✝ e✝) (ExceptT.bindCont fun t => Fitree.interp UBE.handle (Fitree.bind (k✝ t) k)) =
    Fitree.bind (UBE.handle T✝ e✝) fun x =>
      Fitree.bind (ExceptT.bindCont (fun t => Fitree.interp UBE.handle (k✝ t)) x) fun x =>
        match x with
        | Except.error ε => Fitree.ret (Except.error ε)
        | Except.ok x => Fitree.interp UBE.handle (k x)
Tactic:
simp [ExceptT.bind, ExceptT.mk, ExceptT.bindCont]
Proof state after:
case Vis
T R : Type
k : T → Fitree UBE R
T✝ : Type
e✝ : UBE T✝
k✝ : T✝ → Fitree UBE T
ih :
  ∀ (a : T✝),
    Fitree.interp UBE.handle (Fitree.bind (k✝ a) k) =
      Fitree.bind (Fitree.interp UBE.handle (k✝ a)) fun x =>
        match x with
        | Except.error ε => Fitree.ret (Except.error ε)
        | Except.ok x => Fitree.interp UBE.handle (k x)
⊢ (Fitree.bind (UBE.handle T✝ e✝) fun x =>
      match x with
      | Except.ok a => Fitree.interp UBE.handle (Fitree.bind (k✝ a) k)
      | Except.error e => Fitree.ret (Except.error e)) =
    Fitree.bind (UBE.handle T✝ e✝) fun x =>
      Fitree.bind
        (match x with
        | Except.ok a => Fitree.interp UBE.handle (k✝ a)
        | Except.error e => Fitree.ret (Except.error e))
        fun x =>
        match x with
        | Except.error e => Fitree.ret (Except.error e)
        | Except.ok x => Fitree.interp UBE.handle (k x)
Theorem: interpUB_bind
Proof state before:
case Vis
T R : Type
k : T → Fitree UBE R
T✝ : Type
e✝ : UBE T✝
k✝ : T✝ → Fitree UBE T
ih :
  ∀ (a : T✝),
    Fitree.interp UBE.handle (Fitree.bind (k✝ a) k) =
      Fitree.bind (Fitree.interp UBE.handle (k✝ a)) fun x =>
        match x with
        | Except.error ε => Fitree.ret (Except.error ε)
        | Except.ok x => Fitree.interp UBE.handle (k x)
⊢ (Fitree.bind (UBE.handle T✝ e✝) fun x =>
      match x with
      | Except.ok a => Fitree.interp UBE.handle (Fitree.bind (k✝ a) k)
      | Except.error e => Fitree.ret (Except.error e)) =
    Fitree.bind (UBE.handle T✝ e✝) fun x =>
      Fitree.bind
        (match x with
        | Except.ok a => Fitree.interp UBE.handle (k✝ a)
        | Except.error e => Fitree.ret (Except.error e))
        fun x =>
        match x with
        | Except.error e => Fitree.ret (Except.error e)
        | Except.ok x => Fitree.interp UBE.handle (k x)
Tactic:
have fequal2 α β (f g: α → β) x y: f = g → x = y → f x = g y :=
  fun h₁ h₂ => by simp [h₁, h₂]
Proof state after:
case Vis
T R : Type
k : T → Fitree UBE R
T✝ : Type
e✝ : UBE T✝
k✝ : T✝ → Fitree UBE T
ih :
  ∀ (a : T✝),
    Fitree.interp UBE.handle (Fitree.bind (k✝ a) k) =
      Fitree.bind (Fitree.interp UBE.handle (k✝ a)) fun x =>
        match x with
        | Except.error ε => Fitree.ret (Except.error ε)
        | Except.ok x => Fitree.interp UBE.handle (k x)
fequal2 : ∀ (α : Sort ?u.7562) (β : Sort ?u.7563) (f g : α → β) (x y : α), f = g → x = y → f x = g y
⊢ (Fitree.bind (UBE.handle T✝ e✝) fun x =>
      match x with
      | Except.ok a => Fitree.interp UBE.handle (Fitree.bind (k✝ a) k)
      | Except.error e => Fitree.ret (Except.error e)) =
    Fitree.bind (UBE.handle T✝ e✝) fun x =>
      Fitree.bind
        (match x with
        | Except.ok a => Fitree.interp UBE.handle (k✝ a)
        | Except.error e => Fitree.ret (Except.error e))
        fun x =>
        match x with
        | Except.error e => Fitree.ret (Except.error e)
        | Except.ok x => Fitree.interp UBE.handle (k x)
Theorem: interpUB_bind
Proof state before:
case Vis
T R : Type
k : T → Fitree UBE R
T✝ : Type
e✝ : UBE T✝
k✝ : T✝ → Fitree UBE T
ih :
  ∀ (a : T✝),
    Fitree.interp UBE.handle (Fitree.bind (k✝ a) k) =
      Fitree.bind (Fitree.interp UBE.handle (k✝ a)) fun x =>
        match x with
        | Except.error ε => Fitree.ret (Except.error ε)
        | Except.ok x => Fitree.interp UBE.handle (k x)
fequal2 : ∀ (α : Sort ?u.7562) (β : Sort ?u.7563) (f g : α → β) (x y : α), f = g → x = y → f x = g y
⊢ (Fitree.bind (UBE.handle T✝ e✝) fun x =>
      match x with
      | Except.ok a => Fitree.interp UBE.handle (Fitree.bind (k✝ a) k)
      | Except.error e => Fitree.ret (Except.error e)) =
    Fitree.bind (UBE.handle T✝ e✝) fun x =>
      Fitree.bind
        (match x with
        | Except.ok a => Fitree.interp UBE.handle (k✝ a)
        | Except.error e => Fitree.ret (Except.error e))
        fun x =>
        match x with
        | Except.error e => Fitree.ret (Except.error e)
        | Except.ok x => Fitree.interp UBE.handle (k x)
Tactic:
apply fequal2
Proof state after:
case Vis.a
T R : Type
k : T → Fitree UBE R
T✝ : Type
e✝ : UBE T✝
k✝ : T✝ → Fitree UBE T
ih :
  ∀ (a : T✝),
    Fitree.interp UBE.handle (Fitree.bind (k✝ a) k) =
      Fitree.bind (Fitree.interp UBE.handle (k✝ a)) fun x =>
        match x with
        | Except.error ε => Fitree.ret (Except.error ε)
        | Except.ok x => Fitree.interp UBE.handle (k x)
fequal2 : ∀ (α β : Type 1) (f g : α → β) (x y : α), f = g → x = y → f x = g y
⊢ Fitree.bind (UBE.handle T✝ e✝) = Fitree.bind (UBE.handle T✝ e✝)

case Vis.a
T R : Type
k : T → Fitree UBE R
T✝ : Type
e✝ : UBE T✝
k✝ : T✝ → Fitree UBE T
ih :
  ∀ (a : T✝),
    Fitree.interp UBE.handle (Fitree.bind (k✝ a) k) =
      Fitree.bind (Fitree.interp UBE.handle (k✝ a)) fun x =>
        match x with
        | Except.error ε => Fitree.ret (Except.error ε)
        | Except.ok x => Fitree.interp UBE.handle (k x)
fequal2 : ∀ (α β : Type 1) (f g : α → β) (x y : α), f = g → x = y → f x = g y
⊢ (fun x =>
      match x with
      | Except.ok a => Fitree.interp UBE.handle (Fitree.bind (k✝ a) k)
      | Except.error e => Fitree.ret (Except.error e)) =
    fun x =>
    Fitree.bind
      (match x with
      | Except.ok a => Fitree.interp UBE.handle (k✝ a)
      | Except.error e => Fitree.ret (Except.error e))
      fun x =>
      match x with
      | Except.error e => Fitree.ret (Except.error e)
      | Except.ok x => Fitree.interp UBE.handle (k x)
Theorem: interpUB_bind
Proof state before:
case Vis.a
T R : Type
k : T → Fitree UBE R
T✝ : Type
e✝ : UBE T✝
k✝ : T✝ → Fitree UBE T
ih :
  ∀ (a : T✝),
    Fitree.interp UBE.handle (Fitree.bind (k✝ a) k) =
      Fitree.bind (Fitree.interp UBE.handle (k✝ a)) fun x =>
        match x with
        | Except.error ε => Fitree.ret (Except.error ε)
        | Except.ok x => Fitree.interp UBE.handle (k x)
fequal2 : ∀ (α β : Type 1) (f g : α → β) (x y : α), f = g → x = y → f x = g y
⊢ Fitree.bind (UBE.handle T✝ e✝) = Fitree.bind (UBE.handle T✝ e✝)

case Vis.a
T R : Type
k : T → Fitree UBE R
T✝ : Type
e✝ : UBE T✝
k✝ : T✝ → Fitree UBE T
ih :
  ∀ (a : T✝),
    Fitree.interp UBE.handle (Fitree.bind (k✝ a) k) =
      Fitree.bind (Fitree.interp UBE.handle (k✝ a)) fun x =>
        match x with
        | Except.error ε => Fitree.ret (Except.error ε)
        | Except.ok x => Fitree.interp UBE.handle (k x)
fequal2 : ∀ (α β : Type 1) (f g : α → β) (x y : α), f = g → x = y → f x = g y
⊢ (fun x =>
      match x with
      | Except.ok a => Fitree.interp UBE.handle (Fitree.bind (k✝ a) k)
      | Except.error e => Fitree.ret (Except.error e)) =
    fun x =>
    Fitree.bind
      (match x with
      | Except.ok a => Fitree.interp UBE.handle (k✝ a)
      | Except.error e => Fitree.ret (Except.error e))
      fun x =>
      match x with
      | Except.error e => Fitree.ret (Except.error e)
      | Except.ok x => Fitree.interp UBE.handle (k x)
Tactic:
rfl
Proof state after:
case Vis.a
T R : Type
k : T → Fitree UBE R
T✝ : Type
e✝ : UBE T✝
k✝ : T✝ → Fitree UBE T
ih :
  ∀ (a : T✝),
    Fitree.interp UBE.handle (Fitree.bind (k✝ a) k) =
      Fitree.bind (Fitree.interp UBE.handle (k✝ a)) fun x =>
        match x with
        | Except.error ε => Fitree.ret (Except.error ε)
        | Except.ok x => Fitree.interp UBE.handle (k x)
fequal2 : ∀ (α β : Type 1) (f g : α → β) (x y : α), f = g → x = y → f x = g y
⊢ (fun x =>
      match x with
      | Except.ok a => Fitree.interp UBE.handle (Fitree.bind (k✝ a) k)
      | Except.error e => Fitree.ret (Except.error e)) =
    fun x =>
    Fitree.bind
      (match x with
      | Except.ok a => Fitree.interp UBE.handle (k✝ a)
      | Except.error e => Fitree.ret (Except.error e))
      fun x =>
      match x with
      | Except.error e => Fitree.ret (Except.error e)
      | Except.ok x => Fitree.interp UBE.handle (k x)
Theorem: interpUB_bind
Proof state before:
case Vis.a
T R : Type
k : T → Fitree UBE R
T✝ : Type
e✝ : UBE T✝
k✝ : T✝ → Fitree UBE T
ih :
  ∀ (a : T✝),
    Fitree.interp UBE.handle (Fitree.bind (k✝ a) k) =
      Fitree.bind (Fitree.interp UBE.handle (k✝ a)) fun x =>
        match x with
        | Except.error ε => Fitree.ret (Except.error ε)
        | Except.ok x => Fitree.interp UBE.handle (k x)
fequal2 : ∀ (α β : Type 1) (f g : α → β) (x y : α), f = g → x = y → f x = g y
⊢ (fun x =>
      match x with
      | Except.ok a => Fitree.interp UBE.handle (Fitree.bind (k✝ a) k)
      | Except.error e => Fitree.ret (Except.error e)) =
    fun x =>
    Fitree.bind
      (match x with
      | Except.ok a => Fitree.interp UBE.handle (k✝ a)
      | Except.error e => Fitree.ret (Except.error e))
      fun x =>
      match x with
      | Except.error e => Fitree.ret (Except.error e)
      | Except.ok x => Fitree.interp UBE.handle (k x)
Tactic:
funext x
Proof state after:
case Vis.a.h
T R : Type
k : T → Fitree UBE R
T✝ : Type
e✝ : UBE T✝
k✝ : T✝ → Fitree UBE T
ih :
  ∀ (a : T✝),
    Fitree.interp UBE.handle (Fitree.bind (k✝ a) k) =
      Fitree.bind (Fitree.interp UBE.handle (k✝ a)) fun x =>
        match x with
        | Except.error ε => Fitree.ret (Except.error ε)
        | Except.ok x => Fitree.interp UBE.handle (k x)
fequal2 : ∀ (α β : Type 1) (f g : α → β) (x y : α), f = g → x = y → f x = g y
x : Except String T✝
⊢ (match x with
    | Except.ok a => Fitree.interp UBE.handle (Fitree.bind (k✝ a) k)
    | Except.error e => Fitree.ret (Except.error e)) =
    Fitree.bind
      (match x with
      | Except.ok a => Fitree.interp UBE.handle (k✝ a)
      | Except.error e => Fitree.ret (Except.error e))
      fun x =>
      match x with
      | Except.error e => Fitree.ret (Except.error e)
      | Except.ok x => Fitree.interp UBE.handle (k x)
Theorem: interpUB_bind
Proof state before:
case Vis.a.h
T R : Type
k : T → Fitree UBE R
T✝ : Type
e✝ : UBE T✝
k✝ : T✝ → Fitree UBE T
ih :
  ∀ (a : T✝),
    Fitree.interp UBE.handle (Fitree.bind (k✝ a) k) =
      Fitree.bind (Fitree.interp UBE.handle (k✝ a)) fun x =>
        match x with
        | Except.error ε => Fitree.ret (Except.error ε)
        | Except.ok x => Fitree.interp UBE.handle (k x)
fequal2 : ∀ (α β : Type 1) (f g : α → β) (x y : α), f = g → x = y → f x = g y
x : Except String T✝
⊢ (match x with
    | Except.ok a => Fitree.interp UBE.handle (Fitree.bind (k✝ a) k)
    | Except.error e => Fitree.ret (Except.error e)) =
    Fitree.bind
      (match x with
      | Except.ok a => Fitree.interp UBE.handle (k✝ a)
      | Except.error e => Fitree.ret (Except.error e))
      fun x =>
      match x with
      | Except.error e => Fitree.ret (Except.error e)
      | Except.ok x => Fitree.interp UBE.handle (k x)
Tactic:
cases x <;> simp [ih]
Proof state after:
no goals
Theorem: interpUB_bind
Proof state before:
T R : Type
k : T → Fitree UBE R
T✝ : Type
e✝ : UBE T✝
k✝ : T✝ → Fitree UBE T
ih :
  ∀ (a : T✝),
    Fitree.interp UBE.handle (Fitree.bind (k✝ a) k) =
      Fitree.bind (Fitree.interp UBE.handle (k✝ a)) fun x =>
        match x with
        | Except.error ε => Fitree.ret (Except.error ε)
        | Except.ok x => Fitree.interp UBE.handle (k x)
α : Sort ?u.7562
β : Sort ?u.7563
f g : α → β
x y : α
h₁ : f = g
h₂ : x = y
⊢ f x = g y
Tactic:
simp [h₁, h₂]
Proof state after:
no goals
Theorem: interpUB'_bind
Proof state before:
T : Type
E : Type → Type
R : Type
t : Fitree (UBE +' E) T
k : T → Fitree (UBE +' E) R
⊢ interpUB' (Fitree.bind t k) =
    Fitree.bind (interpUB' t) fun x =>
      match x with
      | Except.error ε => Fitree.ret (Except.error ε)
      | Except.ok x => interpUB' (k x)
Tactic:
induction t with
| Ret _ => rfl
| Vis _ _ ih =>
    simp [interpUB', Fitree.interpExcept] at *
    simp [Fitree.interp, Fitree.bind, Bind.bind]
    simp [ExceptT.bind, ExceptT.mk, ExceptT.bindCont]
    have fequal2 α β (f g: α → β) x y: f = g → x = y → f x = g y :=
      fun h₁ h₂ => by simp [h₁, h₂]
    apply fequal2; rfl; funext x
    cases x <;> simp [ih]
Proof state after:
no goals
Theorem: interpUB'_bind
Proof state before:
case Ret
T : Type
E : Type → Type
R : Type
k : T → Fitree (UBE +' E) R
r✝ : T
⊢ interpUB' (Fitree.bind (Fitree.Ret r✝) k) =
    Fitree.bind (interpUB' (Fitree.Ret r✝)) fun x =>
      match x with
      | Except.error ε => Fitree.ret (Except.error ε)
      | Except.ok x => interpUB' (k x)
Tactic:
rfl
Proof state after:
no goals
Theorem: interpUB'_bind
Proof state before:
case Vis
T : Type
E : Type → Type
R : Type
k : T → Fitree (UBE +' E) R
T✝ : Type
e✝ : sum1 UBE E T✝
k✝ : T✝ → Fitree (UBE +' E) T
ih :
  ∀ (a : T✝),
    interpUB' (Fitree.bind (k✝ a) k) =
      Fitree.bind (interpUB' (k✝ a)) fun x =>
        match x with
        | Except.error ε => Fitree.ret (Except.error ε)
        | Except.ok x => interpUB' (k x)
⊢ interpUB' (Fitree.bind (Fitree.Vis e✝ k✝) k) =
    Fitree.bind (interpUB' (Fitree.Vis e✝ k✝)) fun x =>
      match x with
      | Except.error ε => Fitree.ret (Except.error ε)
      | Except.ok x => interpUB' (k x)
Tactic:
simp [interpUB', Fitree.interpExcept] at *
Proof state after:
case Vis
T : Type
E : Type → Type
R : Type
k : T → Fitree (UBE +' E) R
T✝ : Type
e✝ : sum1 UBE E T✝
k✝ : T✝ → Fitree (UBE +' E) T
ih :
  ∀ (a : T✝),
    Fitree.interp (Fitree.case UBE.handle Fitree.liftHandler) (Fitree.bind (k✝ a) k) =
      Fitree.bind (Fitree.interp (Fitree.case UBE.handle Fitree.liftHandler) (k✝ a)) fun x =>
        match x with
        | Except.error ε => Fitree.ret (Except.error ε)
        | Except.ok x => Fitree.interp (Fitree.case UBE.handle Fitree.liftHandler) (k x)
⊢ Fitree.interp (Fitree.case UBE.handle Fitree.liftHandler) (Fitree.bind (Fitree.Vis e✝ k✝) k) =
    Fitree.bind (Fitree.interp (Fitree.case UBE.handle Fitree.liftHandler) (Fitree.Vis e✝ k✝)) fun x =>
      match x with
      | Except.error ε => Fitree.ret (Except.error ε)
      | Except.ok x => Fitree.interp (Fitree.case UBE.handle Fitree.liftHandler) (k x)
Theorem: interpUB'_bind
Proof state before:
case Vis
T : Type
E : Type → Type
R : Type
k : T → Fitree (UBE +' E) R
T✝ : Type
e✝ : sum1 UBE E T✝
k✝ : T✝ → Fitree (UBE +' E) T
ih :
  ∀ (a : T✝),
    Fitree.interp (Fitree.case UBE.handle Fitree.liftHandler) (Fitree.bind (k✝ a) k) =
      Fitree.bind (Fitree.interp (Fitree.case UBE.handle Fitree.liftHandler) (k✝ a)) fun x =>
        match x with
        | Except.error ε => Fitree.ret (Except.error ε)
        | Except.ok x => Fitree.interp (Fitree.case UBE.handle Fitree.liftHandler) (k x)
⊢ Fitree.interp (Fitree.case UBE.handle Fitree.liftHandler) (Fitree.bind (Fitree.Vis e✝ k✝) k) =
    Fitree.bind (Fitree.interp (Fitree.case UBE.handle Fitree.liftHandler) (Fitree.Vis e✝ k✝)) fun x =>
      match x with
      | Except.error ε => Fitree.ret (Except.error ε)
      | Except.ok x => Fitree.interp (Fitree.case UBE.handle Fitree.liftHandler) (k x)
Tactic:
simp [Fitree.interp, Fitree.bind, Bind.bind]
Proof state after:
case Vis
T : Type
E : Type → Type
R : Type
k : T → Fitree (UBE +' E) R
T✝ : Type
e✝ : sum1 UBE E T✝
k✝ : T✝ → Fitree (UBE +' E) T
ih :
  ∀ (a : T✝),
    Fitree.interp (Fitree.case UBE.handle Fitree.liftHandler) (Fitree.bind (k✝ a) k) =
      Fitree.bind (Fitree.interp (Fitree.case UBE.handle Fitree.liftHandler) (k✝ a)) fun x =>
        match x with
        | Except.error ε => Fitree.ret (Except.error ε)
        | Except.ok x => Fitree.interp (Fitree.case UBE.handle Fitree.liftHandler) (k x)
⊢ Fitree.bind (Fitree.case UBE.handle Fitree.liftHandler T✝ e✝)
      (ExceptT.bindCont fun t => Fitree.interp (Fitree.case UBE.handle Fitree.liftHandler) (Fitree.bind (k✝ t) k)) =
    Fitree.bind (Fitree.case UBE.handle Fitree.liftHandler T✝ e✝) fun x =>
      Fitree.bind (ExceptT.bindCont (fun t => Fitree.interp (Fitree.case UBE.handle Fitree.liftHandler) (k✝ t)) x)
        fun x =>
        match x with
        | Except.error ε => Fitree.ret (Except.error ε)
        | Except.ok x => Fitree.interp (Fitree.case UBE.handle Fitree.liftHandler) (k x)
Theorem: interpUB'_bind
Proof state before:
case Vis
T : Type
E : Type → Type
R : Type
k : T → Fitree (UBE +' E) R
T✝ : Type
e✝ : sum1 UBE E T✝
k✝ : T✝ → Fitree (UBE +' E) T
ih :
  ∀ (a : T✝),
    Fitree.interp (Fitree.case UBE.handle Fitree.liftHandler) (Fitree.bind (k✝ a) k) =
      Fitree.bind (Fitree.interp (Fitree.case UBE.handle Fitree.liftHandler) (k✝ a)) fun x =>
        match x with
        | Except.error ε => Fitree.ret (Except.error ε)
        | Except.ok x => Fitree.interp (Fitree.case UBE.handle Fitree.liftHandler) (k x)
⊢ Fitree.bind (Fitree.case UBE.handle Fitree.liftHandler T✝ e✝)
      (ExceptT.bindCont fun t => Fitree.interp (Fitree.case UBE.handle Fitree.liftHandler) (Fitree.bind (k✝ t) k)) =
    Fitree.bind (Fitree.case UBE.handle Fitree.liftHandler T✝ e✝) fun x =>
      Fitree.bind (ExceptT.bindCont (fun t => Fitree.interp (Fitree.case UBE.handle Fitree.liftHandler) (k✝ t)) x)
        fun x =>
        match x with
        | Except.error ε => Fitree.ret (Except.error ε)
        | Except.ok x => Fitree.interp (Fitree.case UBE.handle Fitree.liftHandler) (k x)
Tactic:
simp [ExceptT.bind, ExceptT.mk, ExceptT.bindCont]
Proof state after:
case Vis
T : Type
E : Type → Type
R : Type
k : T → Fitree (UBE +' E) R
T✝ : Type
e✝ : sum1 UBE E T✝
k✝ : T✝ → Fitree (UBE +' E) T
ih :
  ∀ (a : T✝),
    Fitree.interp (Fitree.case UBE.handle Fitree.liftHandler) (Fitree.bind (k✝ a) k) =
      Fitree.bind (Fitree.interp (Fitree.case UBE.handle Fitree.liftHandler) (k✝ a)) fun x =>
        match x with
        | Except.error ε => Fitree.ret (Except.error ε)
        | Except.ok x => Fitree.interp (Fitree.case UBE.handle Fitree.liftHandler) (k x)
⊢ (Fitree.bind (Fitree.case UBE.handle Fitree.liftHandler T✝ e✝) fun x =>
      match x with
      | Except.ok a => Fitree.interp (Fitree.case UBE.handle Fitree.liftHandler) (Fitree.bind (k✝ a) k)
      | Except.error e => Fitree.ret (Except.error e)) =
    Fitree.bind (Fitree.case UBE.handle Fitree.liftHandler T✝ e✝) fun x =>
      Fitree.bind
        (match x with
        | Except.ok a => Fitree.interp (Fitree.case UBE.handle Fitree.liftHandler) (k✝ a)
        | Except.error e => Fitree.ret (Except.error e))
        fun x =>
        match x with
        | Except.error e => Fitree.ret (Except.error e)
        | Except.ok x => Fitree.interp (Fitree.case UBE.handle Fitree.liftHandler) (k x)
Theorem: interpUB'_bind
Proof state before:
case Vis
T : Type
E : Type → Type
R : Type
k : T → Fitree (UBE +' E) R
T✝ : Type
e✝ : sum1 UBE E T✝
k✝ : T✝ → Fitree (UBE +' E) T
ih :
  ∀ (a : T✝),
    Fitree.interp (Fitree.case UBE.handle Fitree.liftHandler) (Fitree.bind (k✝ a) k) =
      Fitree.bind (Fitree.interp (Fitree.case UBE.handle Fitree.liftHandler) (k✝ a)) fun x =>
        match x with
        | Except.error ε => Fitree.ret (Except.error ε)
        | Except.ok x => Fitree.interp (Fitree.case UBE.handle Fitree.liftHandler) (k x)
⊢ (Fitree.bind (Fitree.case UBE.handle Fitree.liftHandler T✝ e✝) fun x =>
      match x with
      | Except.ok a => Fitree.interp (Fitree.case UBE.handle Fitree.liftHandler) (Fitree.bind (k✝ a) k)
      | Except.error e => Fitree.ret (Except.error e)) =
    Fitree.bind (Fitree.case UBE.handle Fitree.liftHandler T✝ e✝) fun x =>
      Fitree.bind
        (match x with
        | Except.ok a => Fitree.interp (Fitree.case UBE.handle Fitree.liftHandler) (k✝ a)
        | Except.error e => Fitree.ret (Except.error e))
        fun x =>
        match x with
        | Except.error e => Fitree.ret (Except.error e)
        | Except.ok x => Fitree.interp (Fitree.case UBE.handle Fitree.liftHandler) (k x)
Tactic:
have fequal2 α β (f g: α → β) x y: f = g → x = y → f x = g y :=
  fun h₁ h₂ => by simp [h₁, h₂]
Proof state after:
case Vis
T : Type
E : Type → Type
R : Type
k : T → Fitree (UBE +' E) R
T✝ : Type
e✝ : sum1 UBE E T✝
k✝ : T✝ → Fitree (UBE +' E) T
ih :
  ∀ (a : T✝),
    Fitree.interp (Fitree.case UBE.handle Fitree.liftHandler) (Fitree.bind (k✝ a) k) =
      Fitree.bind (Fitree.interp (Fitree.case UBE.handle Fitree.liftHandler) (k✝ a)) fun x =>
        match x with
        | Except.error ε => Fitree.ret (Except.error ε)
        | Except.ok x => Fitree.interp (Fitree.case UBE.handle Fitree.liftHandler) (k x)
fequal2 : ∀ (α : Sort ?u.10648) (β : Sort ?u.10649) (f g : α → β) (x y : α), f = g → x = y → f x = g y
⊢ (Fitree.bind (Fitree.case UBE.handle Fitree.liftHandler T✝ e✝) fun x =>
      match x with
      | Except.ok a => Fitree.interp (Fitree.case UBE.handle Fitree.liftHandler) (Fitree.bind (k✝ a) k)
      | Except.error e => Fitree.ret (Except.error e)) =
    Fitree.bind (Fitree.case UBE.handle Fitree.liftHandler T✝ e✝) fun x =>
      Fitree.bind
        (match x with
        | Except.ok a => Fitree.interp (Fitree.case UBE.handle Fitree.liftHandler) (k✝ a)
        | Except.error e => Fitree.ret (Except.error e))
        fun x =>
        match x with
        | Except.error e => Fitree.ret (Except.error e)
        | Except.ok x => Fitree.interp (Fitree.case UBE.handle Fitree.liftHandler) (k x)