awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Control.Monad.Cont
Goal:
m : Type u → Type v
inst : Monad m
ε : Type u
inst_1 : MonadCont m
inst_2 : LawfulMonadCont m
α ω γ : Type u
cmd : ExceptT ε m α
next : Label.{u, v, u} ω (ExceptT ε m) γ → α → ExceptT ε m ω
a : α
⊢ Eq.{v + 1} (α := m (Except ε ω))
    (callCC (β := γ) fun (f : Label (Except ε ω) m γ) ↦
      match (motive := Except ε α → m (Except ε ω)) Except.ok a with
      | Except.ok x => (next (ExceptT.mkLabel f) x).run
      | Except.error e => pure (Except.error e))
    (match (motive := Except ε α → m (Except ε ω)) Except.ok a with
    | Except.ok x => callCC (β := γ) fun (x_1 : Label (Except ε ω) m γ) ↦ (next (ExceptT.mkLabel x_1) x).run
    | Except.error e => pure (Except.error e))

Tactic:
simp [@callCC_dummy m _]

Premises used: LawfulMonadCont.callCC_dummy
-- Module: Mathlib.Control.Monad.Cont
Goal:
m : Type u → Type v
inst : Monad m
ε : Type u
inst_1 : MonadCont m
inst_2 : LawfulMonadCont m
α β : Type u
x : α
dead : Label.{u, v, u} α (ExceptT ε m) β → β → ExceptT ε m α
simp : Eq.{v + 1} (α := ExceptT ε m α) (ExceptT.mk (pure (Except.ok x))) (pure x)
⊢ Eq.{v + 1} (α := ExceptT ε m α) (callCC (β := β) fun (f : Label.{u, v, u} α (ExceptT ε m) β) ↦ goto f x >>= dead f)
    (pure x)

Tactic:
simp only [callCC, ExceptT.callCC, ExceptT.goto_mkLabel, map_eq_bind_pure_comp, Function.comp,
      ExceptT.run_bind, ExceptT.run_mk, bind_assoc, pure_bind, @callCC_bind_left m _]

Premises used: LawfulMonad.bind_assoc, Function.comp, LawfulMonadCont.callCC_bind_left, MonadCont.callCC, ExceptT.run_bind, ExceptT.goto_mkLabel, ExceptT.callCC, ExceptT.run_mk, LawfulMonad.pure_bind, map_eq_bind_pure_comp
-- Module: Mathlib.Control.Monad.Cont
Goal:
m : Type u → Type v
inst : Monad m
ε : Type u
inst_1 : MonadCont m
inst_2 : LawfulMonadCont m
α β : Type u
x : α
dead : Label.{u, v, u} α (ExceptT ε m) β → β → ExceptT ε m α
h : Eq.{v + 1} (α := m (Except ε α)) (ExceptT.run (ExceptT.mk (pure (Except.ok x)))) (ExceptT.run (pure x))
⊢ Eq.{v + 1} (α := ExceptT ε m α) (ExceptT.mk (pure (Except.ok x))) (pure x)

Tactic:
ext
-- Module: Mathlib.Control.Monad.Cont
Goal:
m : Type u → Type v
inst : Monad m
ε : Type u
inst_1 : MonadCont m
inst_2 : LawfulMonadCont m
α β : Type u
x : α
dead : Label.{u, v, u} α (ExceptT ε m) β → β → ExceptT ε m α
⊢ Eq.{v + 1} (α := m (Except ε α)) (ExceptT.run (ExceptT.mk (pure (Except.ok x)))) (ExceptT.run (pure x))

Tactic:
rfl
-- Module: Mathlib.Control.Monad.Cont
Goal:
m : Type u → Type v
inst : Monad m
ε : Type u
inst_1 : MonadCont m
inst_2 : LawfulMonadCont m
α β : Type u
dummy : ExceptT ε m α
simp : ExceptT.mk dummy.run = dummy
⊢ (callCC (β := β) fun (x : Label.{u, v, u} α (ExceptT ε m) β) ↦ dummy) = dummy

Tactic:
simp only [callCC, ExceptT.callCC, @callCC_dummy m _]

Premises used: LawfulMonadCont.callCC_dummy, MonadCont.callCC, ExceptT.callCC
-- Module: Mathlib.Control.Monad.Cont
Goal:
m : Type u → Type v
inst : Monad m
ε : Type u
inst_1 : MonadCont m
inst_2 : LawfulMonadCont m
α β : Type u
dummy : ExceptT ε m α
h : (ExceptT.mk dummy.run).run = dummy.run
⊢ ExceptT.mk dummy.run = dummy

Tactic:
ext
-- Module: Mathlib.Control.Monad.Cont
Goal:
m : Type u → Type v
inst : Monad m
ε : Type u
inst_1 : MonadCont m
inst_2 : LawfulMonadCont m
α β : Type u
dummy : ExceptT ε m α
⊢ (ExceptT.mk dummy.run).run = dummy.run

Tactic:
rfl
-- Module: Mathlib.Control.Monad.Cont
Goal:
m : Type u → Type v
inst : Monad m
α β : Type u
x : Label (Option α) m β
i : α
⊢ goto (mkLabel x) i =
    OptionT.mk do
      let a ← goto x (some i)
      pure (some a)

Tactic:
(rfl)

Premises used: rfl
-- Module: Mathlib.Control.Monad.Cont
Goal:
m : Type u → Type v
inst : Monad m
inst_1 : MonadCont m
α β : Type u
f : Label.{u, v, u} α (OptionT m) β → OptionT m α
⊢ (OptionT.callCC f).run = callCC (β := β) fun (x : Label (Option α) m β) ↦ (f (OptionT.mkLabel x)).run

Tactic:
(rfl)

Premises used: OptionT.callCC, rfl
-- Module: Mathlib.Control.Monad.Cont
Goal:
m : Type u → Type v
inst : Monad m
inst_1 : MonadCont m
inst_2 : LawfulMonadCont m
α ω γ : Type u
⊢ ∀ (cmd : OptionT m α) (next : Label.{u, v, u} ω (OptionT m) γ → α → OptionT m ω),
    Eq (α := OptionT m ω) (callCC (β := γ) fun (f : Label.{u, v, u} ω (OptionT m) γ) ↦ cmd >>= next f) do
      let x ← cmd
      callCC (β := γ) fun (f : Label.{u, v, u} ω (OptionT m) γ) ↦ next f x

Tactic:
fun _ _ => OptionT.ext ?_

Premises used: OptionT.ext
-- Module: Mathlib.Control.Monad.Cont
Goal:
m : Type u → Type v
inst : Monad m
inst_1 : MonadCont m
inst_2 : LawfulMonadCont m
refine :
  ∀ {α ω γ : Type u} (x : OptionT m α) (x_1 : Label.{u, v, u} ω (OptionT m) γ → α → OptionT m ω),
    Eq (α := m (Option ω)) (OptionT.run (callCC (β := γ) fun (f : Label.{u, v, u} ω (OptionT m) γ) ↦ x >>= x_1 f))
      (OptionT.run do
        let x ← x
        callCC (β := γ) fun (f : Label.{u, v, u} ω (OptionT m) γ) ↦ x_1 f x)
⊢ ∀ {α ω γ : Type u} (cmd : OptionT m α) (next : Label.{u, v, u} ω (OptionT m) γ → α → OptionT m ω),
    Eq (α := OptionT m ω) (callCC (β := γ) fun (f : Label.{u, v, u} ω (OptionT m) γ) ↦ cmd >>= next f) do
      let x ← cmd
      callCC (β := γ) fun (f : Label.{u, v, u} ω (OptionT m) γ) ↦ next f x

Tactic:
refine fun _ _ => OptionT.ext ?_

Premises used: OptionT.ext
-- Module: Mathlib.Control.Monad.Cont
Goal:
m : Type u → Type v
inst : Monad m
inst_1 : MonadCont m
inst_2 : LawfulMonadCont m
α ω γ : Type u
x : OptionT m α
x_1 : Label.{u, v, u} ω (OptionT m) γ → α → OptionT m ω
⊢ Eq.{v + 1} (α := m (Option ω))
    (callCC (β := γ) fun (f : Label (Option ω) m γ) ↦
      Option.elim none (pure none) fun (x : α) ↦ (x_1 (OptionT.mkLabel f) x).run)
    (Option.elim none (pure none) fun (x : α) ↦
      callCC (β := γ) fun (x_2 : Label (Option ω) m γ) ↦ (x_1 (OptionT.mkLabel x_2) x).run)

Tactic:
simp [@callCC_dummy m _]

Premises used: LawfulMonadCont.callCC_dummy
-- Module: Mathlib.Control.Monad.Cont
Goal:
m : Type u → Type v
inst : Monad m
inst_1 : MonadCont m
inst_2 : LawfulMonadCont m
α ω γ : Type u
x : OptionT m α
x_1 : Label.{u, v, u} ω (OptionT m) γ → α → OptionT m ω
⊢ Eq (α := m (Option ω)) (OptionT.run (callCC (β := γ) fun (f : Label.{u, v, u} ω (OptionT m) γ) ↦ x >>= x_1 f))
    (OptionT.run do
      let x ← x
      callCC (β := γ) fun (f : Label.{u, v, u} ω (OptionT m) γ) ↦ x_1 f x)

Tactic:
simpa [callCC, Option.elimM, callCC_bind_right] using
      bind_congr fun | some _ => rfl | none => by simp [@callCC_dummy m _]

Premises used: bind_congr, MonadCont.callCC, LawfulMonadCont.callCC_bind_right, Option.elimM
-- Module: Mathlib.Control.Monad.Cont
Goal:
m : Type u → Type v
inst : Monad m
inst_1 : MonadCont m
inst_2 : LawfulMonadCont m
α β : Type u
x : α
dead : Label.{u, v, u} α (OptionT m) β → β → OptionT m α
h :
  Eq.{v + 1} (α := m (Option α))
    (OptionT.run (callCC (β := β) fun (f : Label.{u, v, u} α (OptionT m) β) ↦ goto f x >>= dead f))
    (OptionT.run (pure x))
⊢ Eq.{v + 1} (α := OptionT m α) (callCC (β := β) fun (f : Label.{u, v, u} α (OptionT m) β) ↦ goto f x >>= dead f)
    (pure x)

Tactic:
ext
-- Module: Mathlib.Control.Monad.Cont
Goal:
m : Type u → Type v
inst : Monad m
inst_1 : MonadCont m
inst_2 : LawfulMonadCont m
α β : Type u
x : α
dead : Label.{u, v, u} α (OptionT m) β → β → OptionT m α
⊢ Eq.{v + 1} (α := m (Option α))
    (OptionT.run (callCC (β := β) fun (f : Label.{u, v, u} α (OptionT m) β) ↦ goto f x >>= dead f))
    (OptionT.run (pure x))

Tactic:
simp [callCC, OptionT.goto_mkLabel, @callCC_bind_left m _]

Premises used: LawfulMonadCont.callCC_bind_left, MonadCont.callCC, OptionT.goto_mkLabel
-- Module: Mathlib.Control.Monad.Cont
Goal:
m : Type u → Type v
inst : Monad m
inst_1 : MonadCont m
inst_2 : LawfulMonadCont m
α β : Type u
dummy : OptionT m α
h : OptionT.run (callCC (β := β) fun (x : Label.{u, v, u} α (OptionT m) β) ↦ dummy) = dummy.run
⊢ (callCC (β := β) fun (x : Label.{u, v, u} α (OptionT m) β) ↦ dummy) = dummy

Tactic:
ext
-- Module: Mathlib.Control.Monad.Cont
Goal:
m : Type u → Type v
inst : Monad m
inst_1 : MonadCont m
inst_2 : LawfulMonadCont m
α β : Type u
dummy : OptionT m α
⊢ OptionT.run (callCC (β := β) fun (x : Label.{u, v, u} α (OptionT m) β) ↦ dummy) = dummy.run

Tactic:
simp [callCC, OptionT.callCC, @callCC_dummy m _]

Premises used: LawfulMonadCont.callCC_dummy, MonadCont.callCC, OptionT.callCC
-- Module: Mathlib.Control.Monad.Cont
Goal:
m : Type u → Type v
inst : Monad m
α : Type u_1
β ω : Type u
inst_1 : EmptyCollection ω
x : Label (α × ω) m β
i : α
mk :
  ∀ (apply : α × ω → m β),
    goto (mkLabel { apply := apply : Label (α × ω) m β }) i =
      monadLift (goto { apply := apply : Label (α × ω) m β } (i, ∅))
⊢ goto (mkLabel x) i = monadLift (goto x (i, ∅))

Tactic:
cases x
-- Module: Mathlib.Control.Monad.Cont
Goal:
m : Type u → Type v
inst : Monad m
α : Type u_1
β ω : Type u
inst_1 : EmptyCollection ω
i : α
apply : α × ω → m β
⊢ goto (mkLabel { apply := apply : Label (α × ω) m β }) i =
    monadLift (goto { apply := apply : Label (α × ω) m β } (i, ∅))

Tactic:
rfl
-- Module: Mathlib.Control.Monad.Cont
Goal:
m : Type u → Type v
inst : Monad m
α : Type u_1
β ω : Type u
inst_1 : Monoid ω
x : Label (α × ω) m β
i : α
mk :
  ∀ (apply : α × ω → m β),
    goto (mkLabel' { apply := apply : Label (α × ω) m β }) i =
      monadLift (goto { apply := apply : Label (α × ω) m β } (i, 1))
⊢ goto (mkLabel' x) i = monadLift (goto x (i, 1))

Tactic:
cases x
-- Module: Mathlib.Control.Monad.Cont
Goal:
m : Type u → Type v
inst : Monad m
α : Type u_1
β ω : Type u
inst_1 : Monoid ω
i : α
apply : α × ω → m β
⊢ goto (mkLabel' { apply := apply : Label (α × ω) m β }) i =
    monadLift (goto { apply := apply : Label (α × ω) m β } (i, 1))

Tactic:
rfl
-- Module: Mathlib.Control.Monad.Cont
Goal:
m : Type u → Type v
α β σ : Type u
x : Label (α × σ) m (β × σ)
i : α
mk :
  ∀ (apply : α × σ → m (β × σ)),
    goto (mkLabel { apply := apply : Label (α × σ) m (β × σ) }) i =
      StateT.mk fun (s : σ) ↦ goto { apply := apply : Label (α × σ) m (β × σ) } (i, s)
⊢ goto (mkLabel x) i = StateT.mk fun (s : σ) ↦ goto x (i, s)

Tactic:
cases x
-- Module: Mathlib.Control.Monad.Cont
Goal:
m : Type u → Type v
α β σ : Type u
i : α
apply : α × σ → m (β × σ)
⊢ goto (mkLabel { apply := apply : Label (α × σ) m (β × σ) }) i =
    mk fun (s : σ) ↦ goto { apply := apply : Label (α × σ) m (β × σ) } (i, s)

Tactic:
rfl
-- Module: Mathlib.Control.Monad.Cont
Goal:
m : Type u → Type v
σ : Type u
inst : Monad m
inst_1 : MonadCont m
inst_2 : LawfulMonadCont m
α ω γ : Type u
cmd : StateT σ m α
next : Label ω (StateT σ m) γ → α → StateT σ m ω
simp :
  Eq (α := StateT σ m ω)
    (StateT.mk fun (r : σ) ↦ do
      let x ← cmd.run r
      callCC (β := γ × σ) fun (f : Label (ω × σ) m (γ × σ)) ↦ (next (StateT.mkLabel f) x.fst).run x.snd)
    do
    let x ← cmd
    StateT.mk fun (r : σ) ↦ callCC (β := γ × σ) fun (f' : Label (ω × σ) m (γ × σ)) ↦ (next (StateT.mkLabel f') x).run r
⊢ Eq (α := StateT σ m ω) (callCC (β := γ) fun (f : Label ω (StateT σ m) γ) ↦ cmd >>= next f) do
    let x ← cmd
    callCC (β := γ) fun (f : Label ω (StateT σ m) γ) ↦ next f x

Tactic:
simp only [callCC, StateT.callCC, StateT.run_bind, callCC_bind_right]

Premises used: StateT.callCC, StateT.run_bind, MonadCont.callCC, LawfulMonadCont.callCC_bind_right
-- Module: Mathlib.Control.Monad.Cont
Goal:
m : Type u → Type v
σ : Type u
inst : Monad m
inst_1 : MonadCont m
inst_2 : LawfulMonadCont m
α ω γ : Type u
cmd : StateT σ m α
next : Label ω (StateT σ m) γ → α → StateT σ m ω
h :
  ∀ (s : σ),
    Eq (α := m (ω × σ))
      (StateT.run
        (StateT.mk fun (r : σ) ↦ do
          let x ← cmd.run r
          callCC (β := γ × σ) fun (f : Label (ω × σ) m (γ × σ)) ↦ (next (StateT.mkLabel f) x.fst).run x.snd)
        s)
      (StateT.run
        (do
          let x ← cmd
          StateT.mk fun (r : σ) ↦
              callCC (β := γ × σ) fun (f' : Label (ω × σ) m (γ × σ)) ↦ (next (StateT.mkLabel f') x).run r)
        s)
⊢ Eq (α := StateT σ m ω)
    (StateT.mk fun (r : σ) ↦ do
      let x ← cmd.run r
      callCC (β := γ × σ) fun (f : Label (ω × σ) m (γ × σ)) ↦ (next (StateT.mkLabel f) x.fst).run x.snd)
    do
    let x ← cmd
    StateT.mk fun (r : σ) ↦ callCC (β := γ × σ) fun (f' : Label (ω × σ) m (γ × σ)) ↦ (next (StateT.mkLabel f') x).run r

Tactic:
ext
-- Module: Mathlib.Control.Monad.Cont
Goal:
m : Type u → Type v
σ : Type u
inst : Monad m
inst_1 : MonadCont m
inst_2 : LawfulMonadCont m
α ω γ : Type u
cmd : StateT σ m α
next : Label ω (StateT σ m) γ → α → StateT σ m ω
s : σ
⊢ Eq (α := m (ω × σ))
    (StateT.run
      (StateT.mk fun (r : σ) ↦ do
        let x ← cmd.run r
        callCC (β := γ × σ) fun (f : Label (ω × σ) m (γ × σ)) ↦ (next (StateT.mkLabel f) x.fst).run x.snd)
      s)
    (StateT.run
      (do
        let x ← cmd
        StateT.mk fun (r : σ) ↦
            callCC (β := γ × σ) fun (f' : Label (ω × σ) m (γ × σ)) ↦ (next (StateT.mkLabel f') x).run r)
      s)

Tactic:
rfl
-- Module: Mathlib.Control.Monad.Cont
Goal:
m : Type u → Type v
σ : Type u
inst : Monad m
inst_1 : MonadCont m
inst_2 : LawfulMonadCont m
α β : Type u
x : α
dead : Label α (StateT σ m) β → β → StateT σ m α
simp : Eq (α := StateT σ m α) (StateT.mk fun (r : σ) ↦ pure (x, r)) (pure x)
⊢ Eq (α := StateT σ m α) (callCC (β := β) fun (f : Label α (StateT σ m) β) ↦ goto f x >>= dead f) (pure x)

Tactic:
simp only [callCC, StateT.callCC, StateT.goto_mkLabel, StateT.run_bind, StateT.run_mk,
      callCC_bind_left]

Premises used: StateT.callCC, StateT.run_bind, LawfulMonadCont.callCC_bind_left, MonadCont.callCC, StateT.run_mk, StateT.goto_mkLabel
-- Module: Mathlib.Control.Monad.Cont
Goal:
m : Type u → Type v
σ : Type u
inst : Monad m
inst_1 : MonadCont m
inst_2 : LawfulMonadCont m
α β : Type u
x : α
dead : Label α (StateT σ m) β → β → StateT σ m α
h : ∀ (s : σ), Eq.{v + 1} (α := m (α × σ)) (StateT.run (StateT.mk fun (r : σ) ↦ pure (x, r)) s) (StateT.run (pure x) s)
⊢ Eq (α := StateT σ m α) (StateT.mk fun (r : σ) ↦ pure (x, r)) (pure x)

Tactic:
ext
-- Module: Mathlib.Control.Monad.Cont
Goal:
m : Type u → Type v
σ : Type u
inst : Monad m
inst_1 : MonadCont m
inst_2 : LawfulMonadCont m
α β : Type u
x : α
dead : Label α (StateT σ m) β → β → StateT σ m α
s : σ
⊢ Eq.{v + 1} (α := m (α × σ)) (StateT.run (StateT.mk fun (r : σ) ↦ pure (x, r)) s) (StateT.run (pure x) s)

Tactic:
rfl
-- Module: Mathlib.Control.Monad.Cont
Goal:
m : Type u → Type v
σ : Type u
inst : Monad m
inst_1 : MonadCont m
inst_2 : LawfulMonadCont m
α β : Type u
dummy : StateT σ m α
simp : (StateT.mk fun (r : σ) ↦ dummy.run r) = dummy
⊢ (callCC (β := β) fun (x : Label α (StateT σ m) β) ↦ dummy) = dummy

Tactic:
simp only [callCC, StateT.callCC, @callCC_dummy m _]

Premises used: StateT.callCC, LawfulMonadCont.callCC_dummy, MonadCont.callCC
-- Module: Mathlib.Control.Monad.Cont
Goal:
m : Type u → Type v
σ : Type u
inst : Monad m
inst_1 : MonadCont m
inst_2 : LawfulMonadCont m
α β : Type u
dummy : StateT σ m α
h : ∀ (s : σ), StateT.run (StateT.mk fun (r : σ) ↦ dummy.run r) s = dummy.run s
⊢ (StateT.mk fun (r : σ) ↦ dummy.run r) = dummy

Tactic:
ext
-- Module: Mathlib.Control.Monad.Cont
Goal:
m : Type u → Type v
σ : Type u
inst : Monad m
inst_1 : MonadCont m
inst_2 : LawfulMonadCont m
α β : Type u
dummy : StateT σ m α
s : σ
⊢ StateT.run (StateT.mk fun (r : σ) ↦ dummy.run r) s = dummy.run s

Tactic:
rfl
-- Module: Mathlib.Control.Monad.Cont
Goal:
m : Type u → Type v
α : Type u_1
ρ β : Type u
x : Label α m β
i : α
mk :
  ∀ (apply : α → m β),
    goto (mkLabel ρ { apply := apply : Label α m β }) i = monadLift (goto { apply := apply : Label α m β } i)
⊢ goto (mkLabel ρ x) i = monadLift (goto x i)

Tactic:
cases x
-- Module: Mathlib.Control.Monad.Cont
Goal:
m : Type u → Type v
α : Type u_1
ρ β : Type u
i : α
apply : α → m β
⊢ goto (mkLabel ρ { apply := apply : Label α m β }) i = monadLift (goto { apply := apply : Label α m β } i)

Tactic:
rfl
-- Module: Mathlib.Control.Monad.Cont
Goal:
m : Type u → Type v
ρ : Type u
inst : Monad m
inst_1 : MonadCont m
inst_2 : LawfulMonadCont m
α ω γ : Type u
cmd : ReaderT ρ m α
next : Label ω (ReaderT ρ m) γ → α → ReaderT ρ m ω
simp :
  Eq (α := ReaderT ρ m ω)
    (ReaderT.mk fun (r : ρ) ↦ do
      let x ← cmd.run r
      callCC (β := γ) fun (f : Label ω m γ) ↦ (next (ReaderT.mkLabel ρ f) x).run r)
    do
    let x ← cmd
    ReaderT.mk fun (r : ρ) ↦ callCC (β := γ) fun (f' : Label ω m γ) ↦ (next (ReaderT.mkLabel ρ f') x).run r
⊢ Eq (α := ReaderT ρ m ω) (callCC (β := γ) fun (f : Label ω (ReaderT ρ m) γ) ↦ cmd >>= next f) do
    let x ← cmd
    callCC (β := γ) fun (f : Label ω (ReaderT ρ m) γ) ↦ next f x

Tactic:
simp only [callCC, ReaderT.callCC, ReaderT.run_bind,
                                    callCC_bind_right]

Premises used: MonadCont.callCC, LawfulMonadCont.callCC_bind_right, ReaderT.callCC, ReaderT.run_bind
-- Module: Mathlib.Control.Monad.Cont
Goal:
m : Type u → Type v
ρ : Type u
inst : Monad m
inst_1 : MonadCont m
inst_2 : LawfulMonadCont m
α ω γ : Type u
cmd : ReaderT ρ m α
next : Label ω (ReaderT ρ m) γ → α → ReaderT ρ m ω
h :
  ∀ (ctx : ρ),
    Eq (α := m ω)
      (ReaderT.run
        (ReaderT.mk fun (r : ρ) ↦ do
          let x ← cmd.run r
          callCC (β := γ) fun (f : Label ω m γ) ↦ (next (ReaderT.mkLabel ρ f) x).run r)
        ctx)
      (ReaderT.run
        (do
          let x ← cmd
          ReaderT.mk fun (r : ρ) ↦ callCC (β := γ) fun (f' : Label ω m γ) ↦ (next (ReaderT.mkLabel ρ f') x).run r)
        ctx)
⊢ Eq (α := ReaderT ρ m ω)
    (ReaderT.mk fun (r : ρ) ↦ do
      let x ← cmd.run r
      callCC (β := γ) fun (f : Label ω m γ) ↦ (next (ReaderT.mkLabel ρ f) x).run r)
    do
    let x ← cmd
    ReaderT.mk fun (r : ρ) ↦ callCC (β := γ) fun (f' : Label ω m γ) ↦ (next (ReaderT.mkLabel ρ f') x).run r

Tactic:
ext
-- Module: Mathlib.Control.Monad.Cont
Goal:
m : Type u → Type v
ρ : Type u
inst : Monad m
inst_1 : MonadCont m
inst_2 : LawfulMonadCont m
α ω γ : Type u
cmd : ReaderT ρ m α
next : Label ω (ReaderT ρ m) γ → α → ReaderT ρ m ω
ctx : ρ
⊢ Eq (α := m ω)
    (ReaderT.run
      (ReaderT.mk fun (r : ρ) ↦ do
        let x ← cmd.run r
        callCC (β := γ) fun (f : Label ω m γ) ↦ (next (ReaderT.mkLabel ρ f) x).run r)
      ctx)
    (ReaderT.run
      (do
        let x ← cmd
        ReaderT.mk fun (r : ρ) ↦ callCC (β := γ) fun (f' : Label ω m γ) ↦ (next (ReaderT.mkLabel ρ f') x).run r)
      ctx)

Tactic:
rfl
-- Module: Mathlib.Control.Monad.Cont
Goal:
m : Type u → Type v
ρ : Type u
inst : Monad m
inst_1 : MonadCont m
inst_2 : LawfulMonadCont m
α β : Type u
x : α
dead : Label α (ReaderT ρ m) β → β → ReaderT ρ m α
simp : Eq (α := ReaderT ρ m α) (ReaderT.mk fun (r : ρ) ↦ pure x) (pure x)
⊢ Eq (α := ReaderT ρ m α) (callCC (β := β) fun (f : Label α (ReaderT ρ m) β) ↦ goto f x >>= dead f) (pure x)

Tactic:
simp only [callCC, ReaderT.callCC, ReaderT.goto_mkLabel, ReaderT.run_bind,
      ReaderT.run_monadLift, monadLift_self, callCC_bind_left]

Premises used: LawfulMonadCont.callCC_bind_left, MonadCont.callCC, ReaderT.callCC, monadLift_self, ReaderT.goto_mkLabel, ReaderT.run_bind, ReaderT.run_monadLift
-- Module: Mathlib.Control.Monad.Cont
Goal:
m : Type u → Type v
ρ : Type u
inst : Monad m
inst_1 : MonadCont m
inst_2 : LawfulMonadCont m
α β : Type u
x : α
dead : Label α (ReaderT ρ m) β → β → ReaderT ρ m α
h : ∀ (ctx : ρ), Eq.{v + 1} (α := m α) (ReaderT.run (ReaderT.mk fun (r : ρ) ↦ pure x) ctx) (ReaderT.run (pure x) ctx)
⊢ Eq (α := ReaderT ρ m α) (ReaderT.mk fun (r : ρ) ↦ pure x) (pure x)

Tactic:
ext
-- Module: Mathlib.Control.Monad.Cont
Goal:
m : Type u → Type v
ρ : Type u
inst : Monad m
inst_1 : MonadCont m
inst_2 : LawfulMonadCont m
α β : Type u
x : α
dead : Label α (ReaderT ρ m) β → β → ReaderT ρ m α
ctx : ρ
⊢ Eq.{v + 1} (α := m α) (ReaderT.run (ReaderT.mk fun (r : ρ) ↦ pure x) ctx) (ReaderT.run (pure x) ctx)

Tactic:
rfl
-- Module: Mathlib.Control.Monad.Cont
Goal:
m : Type u → Type v
ρ : Type u
inst : Monad m
inst_1 : MonadCont m
inst_2 : LawfulMonadCont m
α β : Type u
dummy : ReaderT ρ m α
simp : (ReaderT.mk fun (r : ρ) ↦ dummy.run r) = dummy
⊢ (callCC (β := β) fun (x : Label α (ReaderT ρ m) β) ↦ dummy) = dummy

Tactic:
simp only [callCC, ReaderT.callCC, @callCC_dummy m _]

Premises used: LawfulMonadCont.callCC_dummy, MonadCont.callCC, ReaderT.callCC
-- Module: Mathlib.Control.Monad.Cont
Goal:
m : Type u → Type v
ρ : Type u
inst : Monad m
inst_1 : MonadCont m
inst_2 : LawfulMonadCont m
α β : Type u
dummy : ReaderT ρ m α
h : ∀ (ctx : ρ), ReaderT.run (ReaderT.mk fun (r : ρ) ↦ dummy.run r) ctx = dummy.run ctx
⊢ (ReaderT.mk fun (r : ρ) ↦ dummy.run r) = dummy

Tactic:
ext
-- Module: Mathlib.Control.Monad.Cont
Goal:
m : Type u → Type v
ρ : Type u
inst : Monad m
inst_1 : MonadCont m
inst_2 : LawfulMonadCont m
α β : Type u
dummy : ReaderT ρ m α
ctx : ρ
⊢ ReaderT.run (ReaderT.mk fun (r : ρ) ↦ dummy.run r) ctx = dummy.run ctx

Tactic:
rfl
-- Module: Mathlib.Control.Monad.Cont
Goal:
m : Type u → Type v
m₁ : Type u₀ → Type v₀
m₂ : Type u₁ → Type v₁
α₁ r₁ : Type u₀
α₂ r₂ : Type u₁
F : Equiv.{v₀ + 1, v₁ + 1} (m₁ r₁) (m₂ r₂)
G : α₁ ≃ α₂
f : ContT r₁ m₁ α₁
h :
  ∀ (r : α₁ → m₁ r₁),
    (fun (f : ContT r₂ m₂ α₂) (r : α₁ → m₁ r₁) ↦
          ((F.symm : (a : m₂ r₂) → m₁ r₁)
              (f fun (x : α₂) ↦ (F : (a : m₁ r₁) → m₂ r₂) (r ((G.symm : (a : α₂) → α₁) x))) :
            m₁ r₁))
        ((fun (f : ContT r₁ m₁ α₁) (r : α₂ → m₂ r₂) ↦
            ((F : (a : m₁ r₁) → m₂ r₂) (f fun (x : α₁) ↦ (F.symm : (a : m₂ r₂) → m₁ r₁) (r ((G : (a : α₁) → α₂) x))) :
              m₂ r₂))
          f)
        r =
      f r
⊢ (fun (f : ContT r₂ m₂ α₂) (r : α₁ → m₁ r₁) ↦
        ((F.symm : (a : m₂ r₂) → m₁ r₁) (f fun (x : α₂) ↦ (F : (a : m₁ r₁) → m₂ r₂) (r ((G.symm : (a : α₂) → α₁) x))) :
          m₁ r₁))
      ((fun (f : ContT r₁ m₁ α₁) (r : α₂ → m₂ r₂) ↦
          ((F : (a : m₁ r₁) → m₂ r₂) (f fun (x : α₁) ↦ (F.symm : (a : m₂ r₂) → m₁ r₁) (r ((G : (a : α₁) → α₂) x))) :
            m₂ r₂))
        f) =
    f

Tactic:
funext r
-- Module: Mathlib.Control.Monad.Cont
Goal:
m : Type u → Type v
m₁ : Type u₀ → Type v₀
m₂ : Type u₁ → Type v₁
α₁ r₁ : Type u₀
α₂ r₂ : Type u₁
F : Equiv.{v₀ + 1, v₁ + 1} (m₁ r₁) (m₂ r₂)
G : α₁ ≃ α₂
f : ContT r₁ m₁ α₁
r : α₁ → m₁ r₁
⊢ (fun (f : ContT r₂ m₂ α₂) (r : α₁ → m₁ r₁) ↦
        ((F.symm : (a : m₂ r₂) → m₁ r₁) (f fun (x : α₂) ↦ (F : (a : m₁ r₁) → m₂ r₂) (r ((G.symm : (a : α₂) → α₁) x))) :
          m₁ r₁))
      ((fun (f : ContT r₁ m₁ α₁) (r : α₂ → m₂ r₂) ↦
          ((F : (a : m₁ r₁) → m₂ r₂) (f fun (x : α₁) ↦ (F.symm : (a : m₂ r₂) → m₁ r₁) (r ((G : (a : α₁) → α₂) x))) :
            m₂ r₂))
        f)
      r =
    f r

Tactic:
simp
-- Module: Mathlib.Control.Monad.Cont
Goal:
m : Type u → Type v
m₁ : Type u₀ → Type v₀
m₂ : Type u₁ → Type v₁
α₁ r₁ : Type u₀
α₂ r₂ : Type u₁
F : Equiv.{v₀ + 1, v₁ + 1} (m₁ r₁) (m₂ r₂)
G : α₁ ≃ α₂
f : ContT r₂ m₂ α₂
h :
  ∀ (r : α₂ → m₂ r₂),
    (fun (f : ContT r₁ m₁ α₁) (r : α₂ → m₂ r₂) ↦
          ((F : (a : m₁ r₁) → m₂ r₂) (f fun (x : α₁) ↦ (F.symm : (a : m₂ r₂) → m₁ r₁) (r ((G : (a : α₁) → α₂) x))) :
            m₂ r₂))
        ((fun (f : ContT r₂ m₂ α₂) (r : α₁ → m₁ r₁) ↦
            ((F.symm : (a : m₂ r₂) → m₁ r₁)
                (f fun (x : α₂) ↦ (F : (a : m₁ r₁) → m₂ r₂) (r ((G.symm : (a : α₂) → α₁) x))) :
              m₁ r₁))
          f)
        r =
      f r
⊢ (fun (f : ContT r₁ m₁ α₁) (r : α₂ → m₂ r₂) ↦
        ((F : (a : m₁ r₁) → m₂ r₂) (f fun (x : α₁) ↦ (F.symm : (a : m₂ r₂) → m₁ r₁) (r ((G : (a : α₁) → α₂) x))) :
          m₂ r₂))
      ((fun (f : ContT r₂ m₂ α₂) (r : α₁ → m₁ r₁) ↦
          ((F.symm : (a : m₂ r₂) → m₁ r₁)
              (f fun (x : α₂) ↦ (F : (a : m₁ r₁) → m₂ r₂) (r ((G.symm : (a : α₂) → α₁) x))) :
            m₁ r₁))
        f) =
    f

Tactic:
funext r
-- Module: Mathlib.Control.Monad.Cont
Goal:
m : Type u → Type v
m₁ : Type u₀ → Type v₀
m₂ : Type u₁ → Type v₁
α₁ r₁ : Type u₀
α₂ r₂ : Type u₁
F : Equiv.{v₀ + 1, v₁ + 1} (m₁ r₁) (m₂ r₂)
G : α₁ ≃ α₂
f : ContT r₂ m₂ α₂
r : α₂ → m₂ r₂
⊢ (fun (f : ContT r₁ m₁ α₁) (r : α₂ → m₂ r₂) ↦
        ((F : (a : m₁ r₁) → m₂ r₂) (f fun (x : α₁) ↦ (F.symm : (a : m₂ r₂) → m₁ r₁) (r ((G : (a : α₁) → α₂) x))) :
          m₂ r₂))
      ((fun (f : ContT r₂ m₂ α₂) (r : α₁ → m₁ r₁) ↦
          ((F.symm : (a : m₂ r₂) → m₁ r₁)
              (f fun (x : α₂) ↦ (F : (a : m₁ r₁) → m₂ r₂) (r ((G.symm : (a : α₂) → α₁) x))) :
            m₁ r₁))
        f)
      r =
    f r

Tactic:
simp
-- Module: Mathlib.Control.Monad.Writer
Goal:
M : Type u → Type v
α ω : Type u
cmd : M (α × ω)
⊢ (WriterT.mk cmd).run = cmd

Tactic:
rfl

Premises used: rfl