[GOAL]
r : Type u
m : Type u → Type v
α β γ ω : Type w
x y : ContT r m α
h : ∀ (f : α → m r), run x f = run y f
⊢ x = y
[PROOFSTEP]
unfold ContT
[GOAL]
r : Type u
m : Type u → Type v
α β γ ω : Type w
x y : ContT r m α
h : ∀ (f : α → m r), run x f = run y f
⊢ x = y
[PROOFSTEP]
ext
[GOAL]
case h
r : Type u
m : Type u → Type v
α β γ ω : Type w
x y : ContT r m α
h : ∀ (f : α → m r), run x f = run y f
x✝ : α → m r
⊢ x x✝ = y x✝
[PROOFSTEP]
apply h
[GOAL]
r : Type u
m : Type u → Type v
α β γ ω : Type w
⊢ ∀ {α : Type ?u.3230} (x : ContT r m α), id <$> x = x
[PROOFSTEP]
intros
[GOAL]
r : Type u
m : Type u → Type v
α β γ ω : Type w
α✝ : Type ?u.3230
x✝ : ContT r m α✝
⊢ id <$> x✝ = x✝
[PROOFSTEP]
rfl
[GOAL]
r : Type u
m : Type u → Type v
α β γ ω : Type w
⊢ ∀ {α β : Type ?u.3230} (x : α) (f : α → ContT r m β), pure x >>= f = f x
[PROOFSTEP]
intros
[GOAL]
r : Type u
m : Type u → Type v
α β γ ω : Type w
α✝ β✝ : Type ?u.3230
x✝ : α✝
f✝ : α✝ → ContT r m β✝
⊢ pure x✝ >>= f✝ = f✝ x✝
[PROOFSTEP]
ext
[GOAL]
case h
r : Type u
m : Type u → Type v
α β γ ω : Type w
α✝ β✝ : Type ?u.3230
x✝ : α✝
f✝¹ : α✝ → ContT r m β✝
f✝ : β✝ → m r
⊢ run (pure x✝ >>= f✝¹) f✝ = run (f✝¹ x✝) f✝
[PROOFSTEP]
rfl
[GOAL]
r : Type u
m : Type u → Type v
α β γ ω : Type w
⊢ ∀ {α β γ : Type ?u.3230} (x : ContT r m α) (f : α → ContT r m β) (g : β → ContT r m γ),
    x >>= f >>= g = x >>= fun x => f x >>= g
[PROOFSTEP]
intros
[GOAL]
r : Type u
m : Type u → Type v
α β γ ω : Type w
α✝ β✝ γ✝ : Type ?u.3230
x✝ : ContT r m α✝
f✝ : α✝ → ContT r m β✝
g✝ : β✝ → ContT r m γ✝
⊢ x✝ >>= f✝ >>= g✝ = x✝ >>= fun x => f✝ x >>= g✝
[PROOFSTEP]
ext
[GOAL]
case h
r : Type u
m : Type u → Type v
α β γ ω : Type w
α✝ β✝ γ✝ : Type ?u.3230
x✝ : ContT r m α✝
f✝¹ : α✝ → ContT r m β✝
g✝ : β✝ → ContT r m γ✝
f✝ : γ✝ → m r
⊢ run (x✝ >>= f✝¹ >>= g✝) f✝ = run (x✝ >>= fun x => f✝¹ x >>= g✝) f✝
[PROOFSTEP]
rfl
[GOAL]
r : Type u
m : Type u → Type v
α✝ β✝ γ ω : Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α β : Type u
x : m α
f : α → m β
⊢ monadLift (x >>= f) = monadLift x >>= monadLift ∘ f
[PROOFSTEP]
ext
[GOAL]
case h
r : Type u
m : Type u → Type v
α✝ β✝ γ ω : Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α β : Type u
x : m α
f : α → m β
f✝ : β → m r
⊢ run (monadLift (x >>= f)) f✝ = run (monadLift x >>= monadLift ∘ f) f✝
[PROOFSTEP]
simp only [monadLift, MonadLift.monadLift, (· ∘ ·), (· >>= ·), bind_assoc, id.def, run, ContT.monadLift]
[GOAL]
r : Type u
m : Type u → Type v
α β γ ω : Type w
⊢ ∀ {α ω γ : Type ?u.4864} (cmd : ContT r m α) (next : Label ω (ContT r m) γ → α → ContT r m ω),
    (callCC fun f => cmd >>= next f) = do
      let x ← cmd
      callCC fun f => next f x
[PROOFSTEP]
intros
[GOAL]
r : Type u
m : Type u → Type v
α β γ ω : Type w
α✝ ω✝ γ✝ : Type ?u.4864
cmd✝ : ContT r m α✝
next✝ : Label ω✝ (ContT r m) γ✝ → α✝ → ContT r m ω✝
⊢ (callCC fun f => cmd✝ >>= next✝ f) = do
    let x ← cmd✝
    callCC fun f => next✝ f x
[PROOFSTEP]
ext
[GOAL]
case h
r : Type u
m : Type u → Type v
α β γ ω : Type w
α✝ ω✝ γ✝ : Type ?u.4864
cmd✝ : ContT r m α✝
next✝ : Label ω✝ (ContT r m) γ✝ → α✝ → ContT r m ω✝
f✝ : ω✝ → m r
⊢ run (callCC fun f => cmd✝ >>= next✝ f) f✝ =
    run
      (do
        let x ← cmd✝
        callCC fun f => next✝ f x)
      f✝
[PROOFSTEP]
rfl
[GOAL]
r : Type u
m : Type u → Type v
α β γ ω : Type w
⊢ ∀ {α : Type ?u.4864} (β : Type ?u.4864) (x : α) (dead : Label α (ContT r m) β → β → ContT r m α),
    (callCC fun f => goto f x >>= dead f) = pure x
[PROOFSTEP]
intros
[GOAL]
r : Type u
m : Type u → Type v
α β γ ω : Type w
α✝ β✝ : Type ?u.4864
x✝ : α✝
dead✝ : Label α✝ (ContT r m) β✝ → β✝ → ContT r m α✝
⊢ (callCC fun f => goto f x✝ >>= dead✝ f) = pure x✝
[PROOFSTEP]
ext
[GOAL]
case h
r : Type u
m : Type u → Type v
α β γ ω : Type w
α✝ β✝ : Type ?u.4864
x✝ : α✝
dead✝ : Label α✝ (ContT r m) β✝ → β✝ → ContT r m α✝
f✝ : α✝ → m r
⊢ run (callCC fun f => goto f x✝ >>= dead✝ f) f✝ = run (pure x✝) f✝
[PROOFSTEP]
rfl
[GOAL]
r : Type u
m : Type u → Type v
α β γ ω : Type w
⊢ ∀ {α β : Type ?u.4864} (dummy : ContT r m α), (callCC fun x => dummy) = dummy
[PROOFSTEP]
intros
[GOAL]
r : Type u
m : Type u → Type v
α β γ ω : Type w
α✝ β✝ : Type ?u.4864
dummy✝ : ContT r m α✝
⊢ (callCC fun x => dummy✝) = dummy✝
[PROOFSTEP]
ext
[GOAL]
case h
r : Type u
m : Type u → Type v
α β γ ω : Type w
α✝ β✝ : Type ?u.4864
dummy✝ : ContT r m α✝
f✝ : α✝ → m r
⊢ run (callCC fun x => dummy✝) f✝ = run dummy✝ f✝
[PROOFSTEP]
rfl
[GOAL]
m : Type u → Type v
inst✝ : Monad m
α β ε : Type u
x : Label (Except ε α) m β
i : α
⊢ goto (mkLabel x) i = mk (Except.ok <$> goto x (Except.ok i))
[PROOFSTEP]
cases x
[GOAL]
case mk
m : Type u → Type v
inst✝ : Monad m
α β ε : Type u
i : α
apply✝ : Except ε α → m β
⊢ goto (mkLabel { apply := apply✝ }) i = mk (Except.ok <$> goto { apply := apply✝ } (Except.ok i))
[PROOFSTEP]
rfl
[GOAL]
m : Type u → Type v
inst✝² : Monad m
ε : Type u
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
⊢ ∀ {α ω γ : Type u} (cmd : ExceptT ε m α) (next : Label ω (ExceptT ε m) γ → α → ExceptT ε m ω),
    (callCC fun f => cmd >>= next f) = do
      let x ← cmd
      callCC fun f => next f x
[PROOFSTEP]
intros
[GOAL]
m : Type u → Type v
inst✝² : Monad m
ε : Type u
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ ω✝ γ✝ : Type u
cmd✝ : ExceptT ε m α✝
next✝ : Label ω✝ (ExceptT ε m) γ✝ → α✝ → ExceptT ε m ω✝
⊢ (callCC fun f => cmd✝ >>= next✝ f) = do
    let x ← cmd✝
    callCC fun f => next✝ f x
[PROOFSTEP]
simp [callCC, ExceptT.callCC, callCC_bind_right]
[GOAL]
m : Type u → Type v
inst✝² : Monad m
ε : Type u
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ ω✝ γ✝ : Type u
cmd✝ : ExceptT ε m α✝
next✝ : Label ω✝ (ExceptT ε m) γ✝ → α✝ → ExceptT ε m ω✝
⊢ (ExceptT.mk do
      let x ← ExceptT.run cmd✝
      callCC fun f =>
          match x with
          | Except.ok x => ExceptT.run (next✝ (ExceptT.mkLabel f) x)
          | Except.error e => pure (Except.error e)) =
    do
    let x ← cmd✝
    ExceptT.mk (callCC fun x_1 => ExceptT.run (next✝ (ExceptT.mkLabel x_1) x))
[PROOFSTEP]
ext
[GOAL]
case h
m : Type u → Type v
inst✝² : Monad m
ε : Type u
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ ω✝ γ✝ : Type u
cmd✝ : ExceptT ε m α✝
next✝ : Label ω✝ (ExceptT ε m) γ✝ → α✝ → ExceptT ε m ω✝
⊢ ExceptT.run
      (ExceptT.mk do
        let x ← ExceptT.run cmd✝
        callCC fun f =>
            match x with
            | Except.ok x => ExceptT.run (next✝ (ExceptT.mkLabel f) x)
            | Except.error e => pure (Except.error e)) =
    ExceptT.run do
      let x ← cmd✝
      ExceptT.mk (callCC fun x_1 => ExceptT.run (next✝ (ExceptT.mkLabel x_1) x))
[PROOFSTEP]
dsimp
[GOAL]
case h
m : Type u → Type v
inst✝² : Monad m
ε : Type u
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ ω✝ γ✝ : Type u
cmd✝ : ExceptT ε m α✝
next✝ : Label ω✝ (ExceptT ε m) γ✝ → α✝ → ExceptT ε m ω✝
⊢ (do
      let x ← ExceptT.run cmd✝
      callCC fun f =>
          match x with
          | Except.ok x => ExceptT.run (next✝ (ExceptT.mkLabel f) x)
          | Except.error e => pure (Except.error e)) =
    do
    let x ← ExceptT.run cmd✝
    match x with
      | Except.ok x => callCC fun x_1 => ExceptT.run (next✝ (ExceptT.mkLabel x_1) x)
      | Except.error e => pure (Except.error e)
[PROOFSTEP]
congr with ⟨⟩
[GOAL]
case h.e_a.h.error
m : Type u → Type v
inst✝² : Monad m
ε : Type u
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ ω✝ γ✝ : Type u
cmd✝ : ExceptT ε m α✝
next✝ : Label ω✝ (ExceptT ε m) γ✝ → α✝ → ExceptT ε m ω✝
a✝ : ε
⊢ (callCC fun f =>
      match Except.error a✝ with
      | Except.ok x => ExceptT.run (next✝ (ExceptT.mkLabel f) x)
      | Except.error e => pure (Except.error e)) =
    match Except.error a✝ with
    | Except.ok x => callCC fun x_1 => ExceptT.run (next✝ (ExceptT.mkLabel x_1) x)
    | Except.error e => pure (Except.error e)
[PROOFSTEP]
simp [ExceptT.bindCont, @callCC_dummy m _]
[GOAL]
case h.e_a.h.ok
m : Type u → Type v
inst✝² : Monad m
ε : Type u
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ ω✝ γ✝ : Type u
cmd✝ : ExceptT ε m α✝
next✝ : Label ω✝ (ExceptT ε m) γ✝ → α✝ → ExceptT ε m ω✝
a✝ : α✝
⊢ (callCC fun f =>
      match Except.ok a✝ with
      | Except.ok x => ExceptT.run (next✝ (ExceptT.mkLabel f) x)
      | Except.error e => pure (Except.error e)) =
    match Except.ok a✝ with
    | Except.ok x => callCC fun x_1 => ExceptT.run (next✝ (ExceptT.mkLabel x_1) x)
    | Except.error e => pure (Except.error e)
[PROOFSTEP]
simp [ExceptT.bindCont, @callCC_dummy m _]
[GOAL]
m : Type u → Type v
inst✝² : Monad m
ε : Type u
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
⊢ ∀ {α : Type u} (β : Type u) (x : α) (dead : Label α (ExceptT ε m) β → β → ExceptT ε m α),
    (callCC fun f => goto f x >>= dead f) = pure x
[PROOFSTEP]
intros
[GOAL]
m : Type u → Type v
inst✝² : Monad m
ε : Type u
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ β✝ : Type u
x✝ : α✝
dead✝ : Label α✝ (ExceptT ε m) β✝ → β✝ → ExceptT ε m α✝
⊢ (callCC fun f => goto f x✝ >>= dead✝ f) = pure x✝
[PROOFSTEP]
simp [callCC, ExceptT.callCC, callCC_bind_right, ExceptT.goto_mkLabel, map_eq_bind_pure_comp, bind_assoc,
  @callCC_bind_left m _, Function.comp]
[GOAL]
m : Type u → Type v
inst✝² : Monad m
ε : Type u
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ β✝ : Type u
x✝ : α✝
dead✝ : Label α✝ (ExceptT ε m) β✝ → β✝ → ExceptT ε m α✝
⊢ ExceptT.mk (pure (Except.ok x✝)) = pure x✝
[PROOFSTEP]
ext
[GOAL]
case h
m : Type u → Type v
inst✝² : Monad m
ε : Type u
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ β✝ : Type u
x✝ : α✝
dead✝ : Label α✝ (ExceptT ε m) β✝ → β✝ → ExceptT ε m α✝
⊢ ExceptT.run (ExceptT.mk (pure (Except.ok x✝))) = ExceptT.run (pure x✝)
[PROOFSTEP]
rfl
[GOAL]
m : Type u → Type v
inst✝² : Monad m
ε : Type u
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
⊢ ∀ {α β : Type u} (dummy : ExceptT ε m α), (callCC fun x => dummy) = dummy
[PROOFSTEP]
intros
[GOAL]
m : Type u → Type v
inst✝² : Monad m
ε : Type u
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ β✝ : Type u
dummy✝ : ExceptT ε m α✝
⊢ (callCC fun x => dummy✝) = dummy✝
[PROOFSTEP]
simp [callCC, ExceptT.callCC, @callCC_dummy m _]
[GOAL]
m : Type u → Type v
inst✝² : Monad m
ε : Type u
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ β✝ : Type u
dummy✝ : ExceptT ε m α✝
⊢ ExceptT.mk (ExceptT.run dummy✝) = dummy✝
[PROOFSTEP]
ext
[GOAL]
case h
m : Type u → Type v
inst✝² : Monad m
ε : Type u
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ β✝ : Type u
dummy✝ : ExceptT ε m α✝
⊢ ExceptT.run (ExceptT.mk (ExceptT.run dummy✝)) = ExceptT.run dummy✝
[PROOFSTEP]
rfl
[GOAL]
m : Type u → Type v
inst✝² : Monad m
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
⊢ ∀ {α ω γ : Type u} (cmd : OptionT m α) (next : Label ω (OptionT m) γ → α → OptionT m ω),
    (callCC fun f => cmd >>= next f) = do
      let x ← cmd
      callCC fun f => next f x
[PROOFSTEP]
intros
[GOAL]
m : Type u → Type v
inst✝² : Monad m
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ ω✝ γ✝ : Type u
cmd✝ : OptionT m α✝
next✝ : Label ω✝ (OptionT m) γ✝ → α✝ → OptionT m ω✝
⊢ (callCC fun f => cmd✝ >>= next✝ f) = do
    let x ← cmd✝
    callCC fun f => next✝ f x
[PROOFSTEP]
simp [callCC, OptionT.callCC, callCC_bind_right]
[GOAL]
m : Type u → Type v
inst✝² : Monad m
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ ω✝ γ✝ : Type u
cmd✝ : OptionT m α✝
next✝ : Label ω✝ (OptionT m) γ✝ → α✝ → OptionT m ω✝
⊢ (OptionT.mk do
      let x ← OptionT.run cmd✝
      callCC fun f =>
          match x with
          | some a => OptionT.run (next✝ (OptionT.mkLabel f) a)
          | none => pure none) =
    do
    let x ← cmd✝
    OptionT.mk (callCC fun x_1 => OptionT.run (next✝ (OptionT.mkLabel x_1) x))
[PROOFSTEP]
ext
[GOAL]
case h
m : Type u → Type v
inst✝² : Monad m
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ ω✝ γ✝ : Type u
cmd✝ : OptionT m α✝
next✝ : Label ω✝ (OptionT m) γ✝ → α✝ → OptionT m ω✝
⊢ OptionT.run
      (OptionT.mk do
        let x ← OptionT.run cmd✝
        callCC fun f =>
            match x with
            | some a => OptionT.run (next✝ (OptionT.mkLabel f) a)
            | none => pure none) =
    OptionT.run do
      let x ← cmd✝
      OptionT.mk (callCC fun x_1 => OptionT.run (next✝ (OptionT.mkLabel x_1) x))
[PROOFSTEP]
dsimp
[GOAL]
case h
m : Type u → Type v
inst✝² : Monad m
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ ω✝ γ✝ : Type u
cmd✝ : OptionT m α✝
next✝ : Label ω✝ (OptionT m) γ✝ → α✝ → OptionT m ω✝
⊢ (do
      let x ← OptionT.run cmd✝
      callCC fun f =>
          match x with
          | some a => OptionT.run (next✝ (OptionT.mkLabel f) a)
          | none => pure none) =
    do
    let x ← OptionT.run cmd✝
    match x with
      | some a => callCC fun x => OptionT.run (next✝ (OptionT.mkLabel x) a)
      | none => pure none
[PROOFSTEP]
congr with ⟨⟩
[GOAL]
case h.e_a.h.none
m : Type u → Type v
inst✝² : Monad m
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ ω✝ γ✝ : Type u
cmd✝ : OptionT m α✝
next✝ : Label ω✝ (OptionT m) γ✝ → α✝ → OptionT m ω✝
⊢ (callCC fun f =>
      match none with
      | some a => OptionT.run (next✝ (OptionT.mkLabel f) a)
      | none => pure none) =
    match none with
    | some a => callCC fun x => OptionT.run (next✝ (OptionT.mkLabel x) a)
    | none => pure none
[PROOFSTEP]
simp [@callCC_dummy m _]
[GOAL]
case h.e_a.h.some
m : Type u → Type v
inst✝² : Monad m
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ ω✝ γ✝ : Type u
cmd✝ : OptionT m α✝
next✝ : Label ω✝ (OptionT m) γ✝ → α✝ → OptionT m ω✝
val✝ : α✝
⊢ (callCC fun f =>
      match some val✝ with
      | some a => OptionT.run (next✝ (OptionT.mkLabel f) a)
      | none => pure none) =
    match some val✝ with
    | some a => callCC fun x => OptionT.run (next✝ (OptionT.mkLabel x) a)
    | none => pure none
[PROOFSTEP]
simp [@callCC_dummy m _]
[GOAL]
m : Type u → Type v
inst✝² : Monad m
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
⊢ ∀ {α : Type u} (β : Type u) (x : α) (dead : Label α (OptionT m) β → β → OptionT m α),
    (callCC fun f => goto f x >>= dead f) = pure x
[PROOFSTEP]
intros
[GOAL]
m : Type u → Type v
inst✝² : Monad m
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ β✝ : Type u
x✝ : α✝
dead✝ : Label α✝ (OptionT m) β✝ → β✝ → OptionT m α✝
⊢ (callCC fun f => goto f x✝ >>= dead✝ f) = pure x✝
[PROOFSTEP]
simp [callCC, OptionT.callCC, callCC_bind_right, OptionT.goto_mkLabel, map_eq_bind_pure_comp, bind_assoc,
  @callCC_bind_left m _, Function.comp]
[GOAL]
m : Type u → Type v
inst✝² : Monad m
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ β✝ : Type u
x✝ : α✝
dead✝ : Label α✝ (OptionT m) β✝ → β✝ → OptionT m α✝
⊢ OptionT.mk (pure (some x✝)) = pure x✝
[PROOFSTEP]
ext
[GOAL]
case h
m : Type u → Type v
inst✝² : Monad m
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ β✝ : Type u
x✝ : α✝
dead✝ : Label α✝ (OptionT m) β✝ → β✝ → OptionT m α✝
⊢ OptionT.run (OptionT.mk (pure (some x✝))) = OptionT.run (pure x✝)
[PROOFSTEP]
rfl
[GOAL]
m : Type u → Type v
inst✝² : Monad m
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
⊢ ∀ {α β : Type u} (dummy : OptionT m α), (callCC fun x => dummy) = dummy
[PROOFSTEP]
intros
[GOAL]
m : Type u → Type v
inst✝² : Monad m
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ β✝ : Type u
dummy✝ : OptionT m α✝
⊢ (callCC fun x => dummy✝) = dummy✝
[PROOFSTEP]
simp [callCC, OptionT.callCC, @callCC_dummy m _]
[GOAL]
m : Type u → Type v
inst✝² : Monad m
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ β✝ : Type u
dummy✝ : OptionT m α✝
⊢ OptionT.mk (OptionT.run dummy✝) = dummy✝
[PROOFSTEP]
ext
[GOAL]
case h
m : Type u → Type v
inst✝² : Monad m
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ β✝ : Type u
dummy✝ : OptionT m α✝
⊢ OptionT.run (OptionT.mk (OptionT.run dummy✝)) = OptionT.run dummy✝
[PROOFSTEP]
rfl
  /- Porting note: In Lean 3, `One ω` is required for `MonadLift (WriterT ω m)`. In Lean 4,
                   `EmptyCollection ω` or `Monoid ω` is required. So we give definitions for the both
                   instances. -/
[GOAL]
m : Type u → Type v
inst✝¹ : Monad m
α : Type u_1
β ω : Type u
inst✝ : EmptyCollection ω
x : Label (α × ω) m β
i : α
⊢ goto (mkLabel x) i = monadLift (goto x (i, ∅))
[PROOFSTEP]
cases x
[GOAL]
case mk
m : Type u → Type v
inst✝¹ : Monad m
α : Type u_1
β ω : Type u
inst✝ : EmptyCollection ω
i : α
apply✝ : α × ω → m β
⊢ goto (mkLabel { apply := apply✝ }) i = monadLift (goto { apply := apply✝ } (i, ∅))
[PROOFSTEP]
rfl
[GOAL]
m : Type u → Type v
inst✝¹ : Monad m
α : Type u_1
β ω : Type u
inst✝ : Monoid ω
x : Label (α × ω) m β
i : α
⊢ goto (mkLabel' x) i = monadLift (goto x (i, 1))
[PROOFSTEP]
cases x
[GOAL]
case mk
m : Type u → Type v
inst✝¹ : Monad m
α : Type u_1
β ω : Type u
inst✝ : Monoid ω
i : α
apply✝ : α × ω → m β
⊢ goto (mkLabel' { apply := apply✝ }) i = monadLift (goto { apply := apply✝ } (i, 1))
[PROOFSTEP]
rfl
[GOAL]
m : Type u → Type v
inst✝ : Monad m
α β σ : Type u
x : Label (α × σ) m (β × σ)
i : α
⊢ goto (mkLabel x) i = StateT.mk fun s => goto x (i, s)
[PROOFSTEP]
cases x
[GOAL]
case mk
m : Type u → Type v
inst✝ : Monad m
α β σ : Type u
i : α
apply✝ : α × σ → m (β × σ)
⊢ goto (mkLabel { apply := apply✝ }) i = StateT.mk fun s => goto { apply := apply✝ } (i, s)
[PROOFSTEP]
rfl
[GOAL]
m : Type u → Type v
inst✝² : Monad m
σ : Type u
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
⊢ ∀ {α ω γ : Type u} (cmd : StateT σ m α) (next : Label ω (StateT σ m) γ → α → StateT σ m ω),
    (callCC fun f => cmd >>= next f) = do
      let x ← cmd
      callCC fun f => next f x
[PROOFSTEP]
intros
[GOAL]
m : Type u → Type v
inst✝² : Monad m
σ : Type u
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ ω✝ γ✝ : Type u
cmd✝ : StateT σ m α✝
next✝ : Label ω✝ (StateT σ m) γ✝ → α✝ → StateT σ m ω✝
⊢ (callCC fun f => cmd✝ >>= next✝ f) = do
    let x ← cmd✝
    callCC fun f => next✝ f x
[PROOFSTEP]
simp [callCC, StateT.callCC, callCC_bind_right]
[GOAL]
m : Type u → Type v
inst✝² : Monad m
σ : Type u
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ ω✝ γ✝ : Type u
cmd✝ : StateT σ m α✝
next✝ : Label ω✝ (StateT σ m) γ✝ → α✝ → StateT σ m ω✝
⊢ (StateT.mk fun r => do
      let x ← StateT.run cmd✝ r
      callCC fun f => StateT.run (next✝ (StateT.mkLabel f) x.fst) x.snd) =
    do
    let x ← cmd✝
    StateT.mk fun r => callCC fun f' => StateT.run (next✝ (StateT.mkLabel f') x) r
[PROOFSTEP]
ext
[GOAL]
case h
m : Type u → Type v
inst✝² : Monad m
σ : Type u
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ ω✝ γ✝ : Type u
cmd✝ : StateT σ m α✝
next✝ : Label ω✝ (StateT σ m) γ✝ → α✝ → StateT σ m ω✝
s✝ : σ
⊢ StateT.run
      (StateT.mk fun r => do
        let x ← StateT.run cmd✝ r
        callCC fun f => StateT.run (next✝ (StateT.mkLabel f) x.fst) x.snd)
      s✝ =
    StateT.run
      (do
        let x ← cmd✝
        StateT.mk fun r => callCC fun f' => StateT.run (next✝ (StateT.mkLabel f') x) r)
      s✝
[PROOFSTEP]
rfl
[GOAL]
m : Type u → Type v
inst✝² : Monad m
σ : Type u
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
⊢ ∀ {α : Type u} (β : Type u) (x : α) (dead : Label α (StateT σ m) β → β → StateT σ m α),
    (callCC fun f => goto f x >>= dead f) = pure x
[PROOFSTEP]
intros
[GOAL]
m : Type u → Type v
inst✝² : Monad m
σ : Type u
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ β✝ : Type u
x✝ : α✝
dead✝ : Label α✝ (StateT σ m) β✝ → β✝ → StateT σ m α✝
⊢ (callCC fun f => goto f x✝ >>= dead✝ f) = pure x✝
[PROOFSTEP]
simp [callCC, StateT.callCC, callCC_bind_left, StateT.goto_mkLabel]
[GOAL]
m : Type u → Type v
inst✝² : Monad m
σ : Type u
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ β✝ : Type u
x✝ : α✝
dead✝ : Label α✝ (StateT σ m) β✝ → β✝ → StateT σ m α✝
⊢ (StateT.mk fun r => pure (x✝, r)) = pure x✝
[PROOFSTEP]
ext
[GOAL]
case h
m : Type u → Type v
inst✝² : Monad m
σ : Type u
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ β✝ : Type u
x✝ : α✝
dead✝ : Label α✝ (StateT σ m) β✝ → β✝ → StateT σ m α✝
s✝ : σ
⊢ StateT.run (StateT.mk fun r => pure (x✝, r)) s✝ = StateT.run (pure x✝) s✝
[PROOFSTEP]
rfl
[GOAL]
m : Type u → Type v
inst✝² : Monad m
σ : Type u
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
⊢ ∀ {α β : Type u} (dummy : StateT σ m α), (callCC fun x => dummy) = dummy
[PROOFSTEP]
intros
[GOAL]
m : Type u → Type v
inst✝² : Monad m
σ : Type u
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ β✝ : Type u
dummy✝ : StateT σ m α✝
⊢ (callCC fun x => dummy✝) = dummy✝
[PROOFSTEP]
simp [callCC, StateT.callCC, callCC_bind_right, @callCC_dummy m _]
[GOAL]
m : Type u → Type v
inst✝² : Monad m
σ : Type u
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ β✝ : Type u
dummy✝ : StateT σ m α✝
⊢ (StateT.mk fun r => StateT.run dummy✝ r) = dummy✝
[PROOFSTEP]
ext
[GOAL]
case h
m : Type u → Type v
inst✝² : Monad m
σ : Type u
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ β✝ : Type u
dummy✝ : StateT σ m α✝
s✝ : σ
⊢ StateT.run (StateT.mk fun r => StateT.run dummy✝ r) s✝ = StateT.run dummy✝ s✝
[PROOFSTEP]
rfl
[GOAL]
m : Type u → Type v
inst✝ : Monad m
α : Type u_1
ρ β : Type u
x : Label α m β
i : α
⊢ goto (mkLabel ρ x) i = monadLift (goto x i)
[PROOFSTEP]
cases x
[GOAL]
case mk
m : Type u → Type v
inst✝ : Monad m
α : Type u_1
ρ β : Type u
i : α
apply✝ : α → m β
⊢ goto (mkLabel ρ { apply := apply✝ }) i = monadLift (goto { apply := apply✝ } i)
[PROOFSTEP]
rfl
[GOAL]
m : Type u → Type v
inst✝² : Monad m
ρ : Type u
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
⊢ ∀ {α ω γ : Type u} (cmd : ReaderT ρ m α) (next : Label ω (ReaderT ρ m) γ → α → ReaderT ρ m ω),
    (callCC fun f => cmd >>= next f) = do
      let x ← cmd
      callCC fun f => next f x
[PROOFSTEP]
intros
[GOAL]
m : Type u → Type v
inst✝² : Monad m
ρ : Type u
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ ω✝ γ✝ : Type u
cmd✝ : ReaderT ρ m α✝
next✝ : Label ω✝ (ReaderT ρ m) γ✝ → α✝ → ReaderT ρ m ω✝
⊢ (callCC fun f => cmd✝ >>= next✝ f) = do
    let x ← cmd✝
    callCC fun f => next✝ f x
[PROOFSTEP]
simp [callCC, ReaderT.callCC, callCC_bind_right]
[GOAL]
m : Type u → Type v
inst✝² : Monad m
ρ : Type u
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ ω✝ γ✝ : Type u
cmd✝ : ReaderT ρ m α✝
next✝ : Label ω✝ (ReaderT ρ m) γ✝ → α✝ → ReaderT ρ m ω✝
⊢ (ReaderT.mk fun r => do
      let x ← ReaderT.run cmd✝ r
      callCC fun f => ReaderT.run (next✝ (ReaderT.mkLabel ρ f) x) r) =
    do
    let x ← cmd✝
    ReaderT.mk fun r => callCC fun f' => ReaderT.run (next✝ (ReaderT.mkLabel ρ f') x) r
[PROOFSTEP]
ext
[GOAL]
case h
m : Type u → Type v
inst✝² : Monad m
ρ : Type u
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ ω✝ γ✝ : Type u
cmd✝ : ReaderT ρ m α✝
next✝ : Label ω✝ (ReaderT ρ m) γ✝ → α✝ → ReaderT ρ m ω✝
ctx✝ : ρ
⊢ ReaderT.run
      (ReaderT.mk fun r => do
        let x ← ReaderT.run cmd✝ r
        callCC fun f => ReaderT.run (next✝ (ReaderT.mkLabel ρ f) x) r)
      ctx✝ =
    ReaderT.run
      (do
        let x ← cmd✝
        ReaderT.mk fun r => callCC fun f' => ReaderT.run (next✝ (ReaderT.mkLabel ρ f') x) r)
      ctx✝
[PROOFSTEP]
rfl
[GOAL]
m : Type u → Type v
inst✝² : Monad m
ρ : Type u
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
⊢ ∀ {α : Type u} (β : Type u) (x : α) (dead : Label α (ReaderT ρ m) β → β → ReaderT ρ m α),
    (callCC fun f => goto f x >>= dead f) = pure x
[PROOFSTEP]
intros
[GOAL]
m : Type u → Type v
inst✝² : Monad m
ρ : Type u
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ β✝ : Type u
x✝ : α✝
dead✝ : Label α✝ (ReaderT ρ m) β✝ → β✝ → ReaderT ρ m α✝
⊢ (callCC fun f => goto f x✝ >>= dead✝ f) = pure x✝
[PROOFSTEP]
simp [callCC, ReaderT.callCC, callCC_bind_left, ReaderT.goto_mkLabel]
[GOAL]
m : Type u → Type v
inst✝² : Monad m
ρ : Type u
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ β✝ : Type u
x✝ : α✝
dead✝ : Label α✝ (ReaderT ρ m) β✝ → β✝ → ReaderT ρ m α✝
⊢ (ReaderT.mk fun r => pure x✝) = pure x✝
[PROOFSTEP]
ext
[GOAL]
case h
m : Type u → Type v
inst✝² : Monad m
ρ : Type u
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ β✝ : Type u
x✝ : α✝
dead✝ : Label α✝ (ReaderT ρ m) β✝ → β✝ → ReaderT ρ m α✝
ctx✝ : ρ
⊢ ReaderT.run (ReaderT.mk fun r => pure x✝) ctx✝ = ReaderT.run (pure x✝) ctx✝
[PROOFSTEP]
rfl
[GOAL]
m : Type u → Type v
inst✝² : Monad m
ρ : Type u
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
⊢ ∀ {α β : Type u} (dummy : ReaderT ρ m α), (callCC fun x => dummy) = dummy
[PROOFSTEP]
intros
[GOAL]
m : Type u → Type v
inst✝² : Monad m
ρ : Type u
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ β✝ : Type u
dummy✝ : ReaderT ρ m α✝
⊢ (callCC fun x => dummy✝) = dummy✝
[PROOFSTEP]
simp [callCC, ReaderT.callCC, @callCC_dummy m _]
[GOAL]
m : Type u → Type v
inst✝² : Monad m
ρ : Type u
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ β✝ : Type u
dummy✝ : ReaderT ρ m α✝
⊢ (ReaderT.mk fun r => ReaderT.run dummy✝ r) = dummy✝
[PROOFSTEP]
ext
[GOAL]
case h
m : Type u → Type v
inst✝² : Monad m
ρ : Type u
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ β✝ : Type u
dummy✝ : ReaderT ρ m α✝
ctx✝ : ρ
⊢ ReaderT.run (ReaderT.mk fun r => ReaderT.run dummy✝ r) ctx✝ = ReaderT.run dummy✝ ctx✝
[PROOFSTEP]
rfl
[GOAL]
m : Type u → Type v
inst✝ : Monad m
m₁ : Type u₀ → Type v₀
m₂ : Type u₁ → Type v₁
α₁ r₁ : Type u₀
α₂ r₂ : Type u₁
F : m₁ r₁ ≃ m₂ r₂
G : α₁ ≃ α₂
f : ContT r₁ m₁ α₁
⊢ (fun f r => ↑F.symm (f fun x => ↑F (r (↑G.symm x)))) ((fun f r => ↑F (f fun x => ↑F.symm (r (↑G x)))) f) = f
[PROOFSTEP]
funext r
[GOAL]
case h
m : Type u → Type v
inst✝ : Monad m
m₁ : Type u₀ → Type v₀
m₂ : Type u₁ → Type v₁
α₁ r₁ : Type u₀
α₂ r₂ : Type u₁
F : m₁ r₁ ≃ m₂ r₂
G : α₁ ≃ α₂
f : ContT r₁ m₁ α₁
r : α₁ → m₁ r₁
⊢ (fun f r => ↑F.symm (f fun x => ↑F (r (↑G.symm x)))) ((fun f r => ↑F (f fun x => ↑F.symm (r (↑G x)))) f) r = f r
[PROOFSTEP]
simp
[GOAL]
m : Type u → Type v
inst✝ : Monad m
m₁ : Type u₀ → Type v₀
m₂ : Type u₁ → Type v₁
α₁ r₁ : Type u₀
α₂ r₂ : Type u₁
F : m₁ r₁ ≃ m₂ r₂
G : α₁ ≃ α₂
f : ContT r₂ m₂ α₂
⊢ (fun f r => ↑F (f fun x => ↑F.symm (r (↑G x)))) ((fun f r => ↑F.symm (f fun x => ↑F (r (↑G.symm x)))) f) = f
[PROOFSTEP]
funext r
[GOAL]
case h
m : Type u → Type v
inst✝ : Monad m
m₁ : Type u₀ → Type v₀
m₂ : Type u₁ → Type v₁
α₁ r₁ : Type u₀
α₂ r₂ : Type u₁
F : m₁ r₁ ≃ m₂ r₂
G : α₁ ≃ α₂
f : ContT r₂ m₂ α₂
r : α₂ → m₂ r₂
⊢ (fun f r => ↑F (f fun x => ↑F.symm (r (↑G x)))) ((fun f r => ↑F.symm (f fun x => ↑F (r (↑G.symm x)))) f) r = f r
[PROOFSTEP]
simp
