awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Control.LawfulFix (goal)
Goal:
α : Type u_1
β : α → Type u_2
γ : (a : α) → β a → Type u_3
inst : (x : α) → (y : β x) → OmegaCompletePartialOrder (γ x y)
c : Chain ((x : (a : α) × β a) → γ (x.fst (β := fun (a : α) ↦ β a)) (x.snd (β := fun (a : α) ↦ β a)))
⊢ Eq (α := (a : α) → (b : β a) → γ a b)
    (((monotoneCurry α β γ :
            ((x : (a : α) × β a) → γ (x.fst (β := fun (a : α) ↦ β a)) (x.snd (β := fun (a : α) ↦ β a))) →o
              (a : α) → (b : β a) → γ a b) :
          (a : (x : (a : α) × β a) → γ x.fst x.snd) → (a : α) → (b : β a) → γ a b)
        (ωSup c) :
      (a : α) → (b : β a) → γ a b)
    (ωSup (c.map (monotoneCurry α β γ)) : (a : α) → (b : β a) → γ a b)
have h : ∀ (x : α) (y : β x),
  Eq.{u_3 + 1} (α := γ x y)
    (((monotoneCurry α β γ :
            ((x : (a : α) × β a) → γ (x.fst (β := fun (a : α) ↦ β a)) (x.snd (β := fun (a : α) ↦ β a))) →o
              (a : α) → (b : β a) → γ a b) :
          (a : (x : (a : α) × β a) → γ x.fst x.snd) → (a : α) → (b : β a) → γ a b)
        (ωSup c) x y :
      γ x y)
    (ωSup (c.map (monotoneCurry α β γ)) x y : γ x y)
Tactic: ext x y
-- Lean 4 proof step from Mathlib.Control.LawfulFix (goal)
Goal:
α : Type u_1
β : α → Type u_2
γ : (a : α) → β a → Type u_3
inst : (x : α) → (y : β x) → OmegaCompletePartialOrder (γ x y)
c : Chain ((x : (a : α) × β a) → γ (x.fst (β := fun (a : α) ↦ β a)) (x.snd (β := fun (a : α) ↦ β a)))
x : α
y : β x
⊢ Eq.{u_3 + 1} (α := γ x y)
    (((monotoneCurry α β γ :
            ((x : (a : α) × β a) → γ (x.fst (β := fun (a : α) ↦ β a)) (x.snd (β := fun (a : α) ↦ β a))) →o
              (a : α) → (b : β a) → γ a b) :
          (a : (x : (a : α) × β a) → γ x.fst x.snd) → (a : α) → (b : β a) → γ a b)
        (ωSup c) x y :
      γ x y)
    (ωSup (c.map (monotoneCurry α β γ)) x y : γ x y)
have h : ωSup
    (c.map
      (evalOrderHom (π := fun (x : (a : α) × β a) ↦ γ (x.fst (β := fun (a : α) ↦ β a)) (x.snd (β := fun (a : α) ↦ β a)))
        (Sigma.mk (β := fun (a : α) ↦ β a) x y))) =
  ωSup
    (Chain.map (α := (a : β x) → γ x a)
      (Chain.map (α := (a : α) → (b : β a) → γ a b) (c.map (monotoneCurry α β γ))
          (evalOrderHom (π := fun (a : α) ↦ (b : β a) → γ a b) x) :
        Chain ((b : β x) → γ x b))
      (evalOrderHom (π := γ x) y : ((j : β x) → γ x j) →o γ x y))
Tactic: dsimp [curry, ωSup]
-- Lean 4 proof step from Mathlib.Control.LawfulFix (goal)
Goal:
α : Type u_1
β : α → Type u_2
γ : (a : α) → β a → Type u_3
inst : (x : α) → (y : β x) → OmegaCompletePartialOrder (γ x y)
c : Chain ((x : (a : α) × β a) → γ (x.fst (β := fun (a : α) ↦ β a)) (x.snd (β := fun (a : α) ↦ β a)))
x : α
y : β x
⊢ ωSup
      (c.map
        (evalOrderHom (π := fun (x : (a : α) × β a) ↦
          γ (x.fst (β := fun (a : α) ↦ β a)) (x.snd (β := fun (a : α) ↦ β a)))
          (Sigma.mk (β := fun (a : α) ↦ β a) x y))) =
    ωSup
      (Chain.map (α := (a : β x) → γ x a)
        (Chain.map (α := (a : α) → (b : β a) → γ a b) (c.map (monotoneCurry α β γ))
            (evalOrderHom (π := fun (a : α) ↦ (b : β a) → γ a b) x) :
          Chain ((b : β x) → γ x b))
        (evalOrderHom (π := γ x) y : ((j : β x) → γ x j) →o γ x y))
have h : ωSup
    (c.map
      (evalOrderHom (π := fun (x : (a : α) × β a) ↦ γ (x.fst (β := fun (a : α) ↦ β a)) (x.snd (β := fun (a : α) ↦ β a)))
        (Sigma.mk (β := fun (a : α) ↦ β a) x y))) =
  ωSup
    (c.map
      (OrderHom.comp (β := (a : α) → (b : β a) → γ a b)
        (OrderHom.comp (evalOrderHom (π := γ x) y) (evalOrderHom (π := fun (a : α) ↦ (b : β a) → γ a b) x))
        (monotoneCurry α β γ)))
Tactic: rw [map_comp, map_comp]
-- Lean 4 proof step from Mathlib.Control.LawfulFix (goal)
Goal:
α : Type u_1
β : α → Type u_2
γ : (a : α) → β a → Type u_3
inst : (x : α) → (y : β x) → OmegaCompletePartialOrder (γ x y)
c : Chain ((a : α) → (b : β a) → γ a b)
⊢ (monotoneUncurry α β γ : (a : (a : α) → (b : β a) → γ a b) → (x : (a : α) × β a) → γ x.fst x.snd) (ωSup c) =
    ωSup (c.map (monotoneUncurry α β γ))
have h : ∀ (x : α) (y : β x),
  (monotoneUncurry α β γ : (a : (a : α) → (b : β a) → γ a b) → (x : (a : α) × β a) → γ x.fst x.snd) (ωSup c)
      (Sigma.mk (β := fun (a : α) ↦ β a) x y) =
    ωSup (c.map (monotoneUncurry α β γ)) (Sigma.mk (β := fun (a : α) ↦ β a) x y)
Tactic: ext ⟨x, y⟩
-- Lean 4 proof step from Mathlib.Control.LawfulFix (goal)
Goal:
α : Type u_1
β : α → Type u_2
γ : (a : α) → β a → Type u_3
inst : (x : α) → (y : β x) → OmegaCompletePartialOrder (γ x y)
c : Chain ((a : α) → (b : β a) → γ a b)
x : α
y : β x
⊢ (monotoneUncurry α β γ : (a : (a : α) → (b : β a) → γ a b) → (x : (a : α) × β a) → γ x.fst x.snd) (ωSup c)
      (Sigma.mk (β := fun (a : α) ↦ β a) x y) =
    ωSup (c.map (monotoneUncurry α β γ)) (Sigma.mk (β := fun (a : α) ↦ β a) x y)
have h : ωSup ((c.map (evalOrderHom (π := fun (a : α) ↦ (b : β a) → γ a b) x)).map (evalOrderHom (π := γ x) y)) =
  ωSup
    ((c.map (monotoneUncurry α β γ)).map
      (evalOrderHom (π := fun (x : (a : α) × β a) ↦ γ (x.fst (β := fun (a : α) ↦ β a)) (x.snd (β := fun (a : α) ↦ β a)))
        (Sigma.mk (β := fun (a : α) ↦ β a) x y)))
Tactic: dsimp [uncurry, ωSup]
-- Lean 4 proof step from Mathlib.Control.LawfulFix (goal)
Goal:
α : Type u_1
β : α → Type u_2
γ : (a : α) → β a → Type u_3
inst : (x : α) → (y : β x) → OmegaCompletePartialOrder (γ x y)
c : Chain ((a : α) → (b : β a) → γ a b)
x : α
y : β x
⊢ ωSup ((c.map (evalOrderHom (π := fun (a : α) ↦ (b : β a) → γ a b) x)).map (evalOrderHom (π := γ x) y)) =
    ωSup
      ((c.map (monotoneUncurry α β γ)).map
        (evalOrderHom (π := fun (x : (a : α) × β a) ↦
          γ (x.fst (β := fun (a : α) ↦ β a)) (x.snd (β := fun (a : α) ↦ β a))) (Sigma.mk (β := fun (a : α) ↦ β a) x y)))
have h : ωSup (c.map (OrderHom.comp (evalOrderHom (π := γ x) y) (evalOrderHom (π := fun (a : α) ↦ (b : β a) → γ a b) x))) =
  ωSup
    (c.map
      (OrderHom.comp
        (evalOrderHom (π := fun (x : (a : α) × β a) ↦
          γ (x.fst (β := fun (a : α) ↦ β a)) (x.snd (β := fun (a : α) ↦ β a))) (Sigma.mk (β := fun (a : α) ↦ β a) x y))
        (monotoneUncurry α β γ)))
Tactic: rw [map_comp, map_comp]
-- Lean 4 proof step from Mathlib.Control.LawfulFix (goal)
Goal:
α : Type u_1
β : α → Type u_2
γ : (a : α) → β a → Type u_3
inst : (x : α) → (y : β x) → OmegaCompletePartialOrder (γ x y)
inst_1 : LawfulFix ((x : Sigma β) → γ (x.fst (β := β)) (x.snd (β := β)))
_f : ((x : α) → (y : β x) → γ x y) → (x : α) → (y : β x) → γ x y
hc : ωScottContinuous _f
⊢ fix _f = _f (fix _f)
have dsimp : curry (β := β) (γ := γ) (fix (uncurry (β := β) (γ := γ) ∘ _f ∘ curry (β := β) (γ := γ))) =
  _f (curry (β := β) (γ := γ) (fix (uncurry (β := β) (γ := γ) ∘ _f ∘ curry (β := β) (γ := γ))))
Tactic: dsimp [fix]
-- Lean 4 proof step from Mathlib.Control.LawfulFix (goal)
Goal:
α : Type u_1
β : α → Type u_2
γ : (a : α) → β a → Type u_3
inst : (x : α) → (y : β x) → OmegaCompletePartialOrder (γ x y)
inst_1 : LawfulFix ((x : Sigma β) → γ (x.fst (β := β)) (x.snd (β := β)))
_f : ((x : α) → (y : β x) → γ x y) → (x : α) → (y : β x) → γ x y
hc : ωScottContinuous _f
| curry (β := β) (γ := γ) (fix (uncurry (β := β) (γ := γ) ∘ _f ∘ curry (β := β) (γ := γ)))
have erw : curry (β := β) (γ := γ)
  ((OrderHom.comp (monotoneUncurry α β γ)
        ({ toFun := _f, monotone' := sorry : ((x : α) → (y : β x) → γ x y) →o (x : α) → (y : β x) → γ x y }.comp
          (monotoneCurry α β γ)) :
      (a : (x : (a : α) × β a) → γ x.fst x.snd) → (x : (a : α) × β a) → γ x.fst x.snd)
    (fix
      (⇑(OrderHom.comp (monotoneUncurry α β γ)
            ({ toFun := _f, monotone' := sorry : ((x : α) → (y : β x) → γ x y) →o (x : α) → (y : β x) → γ x y }.comp
              (monotoneCurry α β γ))) :
        (a : (x : (a : α) × β a) → γ x.fst x.snd) → (x : (a : α) × β a) → γ x.fst x.snd)))
Tactic: erw [LawfulFix.fix_eq (uncurry_curry_ωScottContinuous hc)]
-- Lean 4 proof step from Mathlib.Control.LawfulFix (goal)
Goal:
α : Type u_1
β : α → Type u_2
γ : (a : α) → β a → Type u_3
inst : (x : α) → (y : β x) → OmegaCompletePartialOrder (γ x y)
inst_1 : LawfulFix ((x : Sigma β) → γ (x.fst (β := β)) (x.snd (β := β)))
_f : ((x : α) → (y : β x) → γ x y) → (x : α) → (y : β x) → γ x y
hc : ωScottContinuous _f
⊢ curry (β := β) (γ := γ) (fix (uncurry (β := β) (γ := γ) ∘ _f ∘ curry (β := β) (γ := γ))) =
    _f (curry (β := β) (γ := γ) (fix (uncurry (β := β) (γ := γ) ∘ _f ∘ curry (β := β) (γ := γ))))
have conv_lhs : curry (β := β) (γ := γ)
    ((OrderHom.comp (monotoneUncurry α β γ)
          ({ toFun := _f, monotone' := sorry : ((x : α) → (y : β x) → γ x y) →o (x : α) → (y : β x) → γ x y }.comp
            (monotoneCurry α β γ)) :
        (a : (x : (a : α) × β a) → γ x.fst x.snd) → (x : (a : α) × β a) → γ x.fst x.snd)
      (fix
        (⇑(OrderHom.comp (monotoneUncurry α β γ)
              ({ toFun := _f, monotone' := sorry : ((x : α) → (y : β x) → γ x y) →o (x : α) → (y : β x) → γ x y }.comp
                (monotoneCurry α β γ))) :
          (a : (x : (a : α) × β a) → γ x.fst x.snd) → (x : (a : α) × β a) → γ x.fst x.snd))) =
  _f (curry (β := β) (γ := γ) (fix (uncurry (β := β) (γ := γ) ∘ _f ∘ curry (β := β) (γ := γ))))
Tactic: conv_lhs => erw [LawfulFix.fix_eq (uncurry_curry_ωScottContinuous hc)]
-- Lean 4 proof step from Mathlib.Control.Monad.Cont (goal)
Goal:
r : Type u
m : Type u → Type v
α : Type w
x y : ContT r m α
h : ∀ (f : α → m r), x.run f = y.run f
⊢ x = y
have h₁ : ∀ (x_1 : α → m r), x x_1 = y x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Control.Monad.Cont (goal)
Goal:
r : Type u
m : Type u → Type v
α β : Type w
α_1 β_1 : Type u_1
x : α_1
f : α_1 → ContT r m β_1
⊢ pure x >>= f = f x
have h : ∀ (f_1 : β_1 → m r), (pure x >>= f).run f_1 = (f x).run f_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Control.Monad.Cont (goal)
Goal:
r : Type u
m : Type u → Type v
α β : Type w
α_1 β_1 γ : Type u_1
x : ContT r m α_1
f : α_1 → ContT r m β_1
g : β_1 → ContT r m γ
⊢ x >>= f >>= g = x >>= fun (x : α_1) ↦ f x >>= g
have h : ∀ (f_1 : γ → m r), (x >>= f >>= g).run f_1 = run (x >>= fun (x : α_1) ↦ f x >>= g) f_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Control.Monad.Cont (goal)
Goal:
r : Type u
m : Type u → Type v
inst : Monad m
inst_1 : LawfulMonad m
α β : Type u
x : m α
f : α → m β
⊢ Eq (α := ContT r m β) (monadLift (x >>= f)) (monadLift x >>= monadLift ∘ f)
have h : ∀ (f_1 : β → m r), run (monadLift (x >>= f)) f_1 = run (monadLift x >>= monadLift ∘ f) f_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Control.Monad.Cont (goal)
Goal:
r : Type u
m : Type u → Type v
α β : Type w
α_1 ω γ : Type u_1
cmd : ContT r m α_1
next : Label ω (ContT r m) γ → α_1 → ContT r m ω
⊢ Eq (α := ContT r m ω) (callCC (β := γ) fun (f : Label ω (ContT r m) γ) ↦ cmd >>= next f) do
    let x ← cmd
    callCC (β := γ) fun (f : Label ω (ContT r m) γ) ↦ next f x
have h : ∀ (f : ω → m r),
  run (callCC (β := γ) fun (f : Label ω (ContT r m) γ) ↦ cmd >>= next f) f =
    run
      (do
        let x ← cmd
        callCC (β := γ) fun (f : Label ω (ContT r m) γ) ↦ next f x)
      f
Tactic: ext
-- Lean 4 proof step from Mathlib.Control.Monad.Cont (goal)
Goal:
r : Type u
m : Type u → Type v
α β : Type w
α_1 β_1 : Type u_1
x : α_1
dead : Label α_1 (ContT r m) β_1 → β_1 → ContT r m α_1
⊢ Eq (α := ContT r m α_1) (callCC (β := β_1) fun (f : Label α_1 (ContT r m) β_1) ↦ goto f x >>= dead f) (pure x)
have h : ∀ (f : α_1 → m r), run (callCC (β := β_1) fun (f : Label α_1 (ContT r m) β_1) ↦ goto f x >>= dead f) f = run (pure x) f
Tactic: ext
-- Lean 4 proof step from Mathlib.Control.Monad.Cont (goal)
Goal:
r : Type u
m : Type u → Type v
α β : Type w
α_1 β_1 : Type u_1
dummy : ContT r m α_1
⊢ (callCC (β := β_1) fun (x : Label α_1 (ContT r m) β_1) ↦ dummy) = dummy
have h : ∀ (f : α_1 → m r), run (callCC (β := β_1) fun (x : Label α_1 (ContT r m) β_1) ↦ dummy) f = dummy.run f
Tactic: ext
-- Lean 4 proof step from Mathlib.Control.Monad.Cont (goal)
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))
have mk : ∀ (apply : Except ε α → m β),
  goto (mkLabel { apply := apply : Label (Except ε α) m β }) i =
    mk (Except.ok <$> goto { apply := apply : Label (Except ε α) m β } (Except.ok i))
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Control.Monad.Cont (goal)
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 ω
⊢ Eq (α := ExceptT ε m ω) (callCC (β := γ) fun (f : Label.{u, v, u} ω (ExceptT ε m) γ) ↦ cmd >>= next f) do
    let x ← cmd
    callCC (β := γ) fun (f : Label.{u, v, u} ω (ExceptT ε m) γ) ↦ next f x
have simp : Eq (α := ExceptT ε m ω)
  (ExceptT.mk do
    let x ← cmd.run
    callCC (β := γ) fun (f : Label (Except ε ω) m γ) ↦
        match (motive := Except ε α → m (Except ε ω)) x with
        | Except.ok x => (next (ExceptT.mkLabel f) x).run
        | Except.error e => pure (Except.error e))
  do
  let x ← cmd
  ExceptT.mk (callCC (β := γ) fun (x_1 : Label (Except ε ω) m γ) ↦ (next (ExceptT.mkLabel x_1) x).run)
Tactic: simp only [callCC, ExceptT.callCC, ExceptT.run_bind, callCC_bind_right]
-- Lean 4 proof step from Mathlib.Control.Monad.Cont (goal)
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 ω
⊢ Eq (α := ExceptT ε m ω)
    (ExceptT.mk do
      let x ← cmd.run
      callCC (β := γ) fun (f : Label (Except ε ω) m γ) ↦
          match (motive := Except ε α → m (Except ε ω)) x with
          | Except.ok x => (next (ExceptT.mkLabel f) x).run
          | Except.error e => pure (Except.error e))
    do
    let x ← cmd
    ExceptT.mk (callCC (β := γ) fun (x_1 : Label (Except ε ω) m γ) ↦ (next (ExceptT.mkLabel x_1) x).run)
have h : Eq (α := m (Except ε ω))
  (ExceptT.run
    (ExceptT.mk do
      let x ← cmd.run
      callCC (β := γ) fun (f : Label (Except ε ω) m γ) ↦
          match (motive := Except ε α → m (Except ε ω)) x with
          | Except.ok x => (next (ExceptT.mkLabel f) x).run
          | Except.error e => pure (Except.error e)))
  (ExceptT.run do
    let x ← cmd
    ExceptT.mk (callCC (β := γ) fun (x_1 : Label (Except ε ω) m γ) ↦ (next (ExceptT.mkLabel x_1) x).run))
Tactic: ext
-- Lean 4 proof step from Mathlib.Control.Monad.Cont (goal)
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 ω
⊢ Eq (α := m (Except ε ω))
    (ExceptT.run
      (ExceptT.mk do
        let x ← cmd.run
        callCC (β := γ) fun (f : Label (Except ε ω) m γ) ↦
            match (motive := Except ε α → m (Except ε ω)) x with
            | Except.ok x => (next (ExceptT.mkLabel f) x).run
            | Except.error e => pure (Except.error e)))
    (ExceptT.run do
      let x ← cmd
      ExceptT.mk (callCC (β := γ) fun (x_1 : Label (Except ε ω) m γ) ↦ (next (ExceptT.mkLabel x_1) x).run))
have h : Eq (α := m (Except ε ω))
  (do
    let x ← cmd.run
    callCC (β := γ) fun (f : Label (Except ε ω) m γ) ↦
        match (motive := Except ε α → m (Except ε ω)) x with
        | Except.ok x => (next (ExceptT.mkLabel f) x).run
        | Except.error e => pure (Except.error e))
  do
  let x ← cmd.run
  match (motive := Except ε α → m (Except ε ω)) x 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: dsimp
-- Lean 4 proof step from Mathlib.Control.Monad.Cont (goal)
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 ω
⊢ Eq (α := m (Except ε ω))
    (do
      let x ← cmd.run
      callCC (β := γ) fun (f : Label (Except ε ω) m γ) ↦
          match (motive := Except ε α → m (Except ε ω)) x with
          | Except.ok x => (next (ExceptT.mkLabel f) x).run
          | Except.error e => pure (Except.error e))
    do
    let x ← cmd.run
    match (motive := Except ε α → m (Except ε ω)) x 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)
have h : ∀ (a : ε),
  Eq.{v + 1} (α := m (Except ε ω))
    (callCC (β := γ) fun (f : Label (Except ε ω) m γ) ↦
      match (motive := Except ε α → m (Except ε ω)) Except.error a with
      | Except.ok x => (next (ExceptT.mkLabel f) x).run
      | Except.error e => pure (Except.error e))
    (match (motive := Except ε α → m (Except ε ω)) Except.error 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: congr with ⟨⟩
-- Lean 4 proof step from Mathlib.Control.Monad.Cont (goal)
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 ω
h :
  ∀ (a : ε),
    Eq.{v + 1} (α := m (Except ε ω))
      (callCC (β := γ) fun (f : Label (Except ε ω) m γ) ↦
        match (motive := Except ε α → m (Except ε ω)) Except.error a with
        | Except.ok x => (next (ExceptT.mkLabel f) x).run
        | Except.error e => pure (Except.error e))
      (match (motive := Except ε α → m (Except ε ω)) Except.error 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))
⊢ Eq (α := m (Except ε ω))
    (do
      let x ← cmd.run
      callCC (β := γ) fun (f : Label (Except ε ω) m γ) ↦
          match (motive := Except ε α → m (Except ε ω)) x with
          | Except.ok x => (next (ExceptT.mkLabel f) x).run
          | Except.error e => pure (Except.error e))
    do
    let x ← cmd.run
    match (motive := Except ε α → m (Except ε ω)) x 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)
have h₁ : ∀ (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: congr with ⟨⟩
-- Lean 4 proof step from Mathlib.Control.Monad.Cont (goal)
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} (α := ExceptT ε m α) (callCC (β := β) fun (f : Label.{u, v, u} α (ExceptT ε m) β) ↦ goto f x >>= dead f)
    (pure x)
have simp : Eq.{v + 1} (α := ExceptT ε m α) (ExceptT.mk (pure (Except.ok x))) (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 _]
-- Lean 4 proof step from Mathlib.Control.Monad.Cont (goal)
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} (α := ExceptT ε m α) (ExceptT.mk (pure (Except.ok x))) (pure x)
have h : Eq.{v + 1} (α := m (Except ε α)) (ExceptT.run (ExceptT.mk (pure (Except.ok x)))) (ExceptT.run (pure x))
Tactic: ext
-- Lean 4 proof step from Mathlib.Control.Monad.Cont (goal)
Goal:
m : Type u → Type v
inst : Monad m
ε : Type u
inst_1 : MonadCont m
inst_2 : LawfulMonadCont m
α β : Type u
dummy : ExceptT ε m α
⊢ (callCC (β := β) fun (x : Label.{u, v, u} α (ExceptT ε m) β) ↦ dummy) = dummy
have simp : ExceptT.mk dummy.run = dummy
Tactic: simp only [callCC, ExceptT.callCC, @callCC_dummy m _]
-- Lean 4 proof step from Mathlib.Control.Monad.Cont (goal)
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 = dummy
have h : (ExceptT.mk dummy.run).run = dummy.run
Tactic: ext
-- Lean 4 proof step from Mathlib.Control.Monad.Cont (goal)
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
have 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)
Tactic: refine fun _ _ => OptionT.ext ?_
-- Lean 4 proof step from Mathlib.Control.Monad.Cont (goal)
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} (α := OptionT m α) (callCC (β := β) fun (f : Label.{u, v, u} α (OptionT m) β) ↦ goto f x >>= dead f)
    (pure x)
have 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))
Tactic: ext
-- Lean 4 proof step from Mathlib.Control.Monad.Cont (goal)
Goal:
m : Type u → Type v
inst : Monad m
inst_1 : MonadCont m
inst_2 : LawfulMonadCont m
α β : Type u
dummy : OptionT m α
⊢ (callCC (β := β) fun (x : Label.{u, v, u} α (OptionT m) β) ↦ dummy) = dummy
have h : OptionT.run (callCC (β := β) fun (x : Label.{u, v, u} α (OptionT m) β) ↦ dummy) = dummy.run
Tactic: ext
-- Lean 4 proof step from Mathlib.Control.Monad.Cont (goal)
Goal:
m : Type u → Type v
inst : Monad m
α : Type u_1
β ω : Type u
inst_1 : EmptyCollection ω
x : Label (α × ω) m β
i : α
⊢ goto (mkLabel x) i = monadLift (goto x (i, ∅))
have mk : ∀ (apply : α × ω → m β),
  goto (mkLabel { apply := apply : Label (α × ω) m β }) i =
    monadLift (goto { apply := apply : Label (α × ω) m β } (i, ∅))
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Control.Monad.Cont (goal)
Goal:
m : Type u → Type v
inst : Monad m
α : Type u_1
β ω : Type u
inst_1 : Monoid ω
x : Label (α × ω) m β
i : α
⊢ goto (mkLabel' x) i = monadLift (goto x (i, 1))
have mk : ∀ (apply : α × ω → m β),
  goto (mkLabel' { apply := apply : Label (α × ω) m β }) i =
    monadLift (goto { apply := apply : Label (α × ω) m β } (i, 1))
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Control.Monad.Cont (goal)
Goal:
m : Type u → Type v
α β σ : Type u
x : Label (α × σ) m (β × σ)
i : α
⊢ goto (mkLabel x) i = mk fun (s : σ) ↦ goto x (i, s)
have mk : ∀ (apply : α × σ → m (β × σ)),
  goto (mkLabel { apply := apply : Label (α × σ) m (β × σ) }) i =
    mk fun (s : σ) ↦ goto { apply := apply : Label (α × σ) m (β × σ) } (i, s)
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Control.Monad.Cont (goal)
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 ω
⊢ 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
have 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
Tactic: simp only [callCC, StateT.callCC, StateT.run_bind, callCC_bind_right]