awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Control.LawfulFix
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
      (c.map
        (OrderHom.comp (β := (a : α) → (b : β a) → γ a b)
          (OrderHom.comp (evalOrderHom (π := γ x) y) (evalOrderHom (π := fun (a : α) ↦ (b : β a) → γ a b) x))
          (monotoneCurry α β γ)))

Tactic:
rfl
-- Module: Mathlib.Control.LawfulFix
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)
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)
⊢ (monotoneUncurry α β γ : (a : (a : α) → (b : β a) → γ a b) → (x : (a : α) × β a) → γ x.fst x.snd) (ωSup c) =
    ωSup (c.map (monotoneUncurry α β γ))

Tactic:
ext ⟨x, y⟩
-- Module: Mathlib.Control.LawfulFix
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
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)))
⊢ (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:
dsimp [uncurry, ωSup]

Premises used: Sigma.uncurry, OmegaCompletePartialOrder.ωSup
-- Module: Mathlib.Control.LawfulFix
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
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 α β γ)))
⊢ ω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:
rw [map_comp, map_comp]

Premises used: OmegaCompletePartialOrder.Chain.map_comp
-- Module: Mathlib.Control.LawfulFix
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 (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:
rfl
-- Module: Mathlib.Control.LawfulFix
Goal:
α : Type u_1
β : α → Type u_2
γ : (a : α) → β a → Type u_3
inst : (x : α) → (y : β x) → OmegaCompletePartialOrder (γ x y)
f : ((a : α) → (b : β a) → γ a b) → (a : α) → (b : β a) → γ a b
hc : ωScottContinuous f
⊢ ωScottContinuous (α := (x : (a : α) × β a) → γ (x.fst (β := fun (a : α) ↦ β a)) (x.snd (β := fun (a : α) ↦ β a)))
    (β := (x : (a : α) × β a) → γ (x.fst (β := fun (a : α) ↦ β a)) (x.snd (β := fun (a : α) ↦ β a)))
    (⇑(OrderHom.comp (monotoneUncurry α β γ)
          ({ toFun := f, monotone' := ⋯ : ((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:
(ωScottContinuous_uncurry _ _ _).comp (hc.comp (ωScottContinuous_curry _ _ _))

Premises used: Sigma.uncurry, OmegaCompletePartialOrder.ωScottContinuous.comp, Pi.ωScottContinuous_uncurry, Pi.ωScottContinuous_curry
-- Module: Mathlib.Control.LawfulFix
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
dsimp :
  curry (β := β) (γ := γ) (fix (uncurry (β := β) (γ := γ) ∘ _f ∘ curry (β := β) (γ := γ))) =
    _f (curry (β := β) (γ := γ) (fix (uncurry (β := β) (γ := γ) ∘ _f ∘ curry (β := β) (γ := γ))))
⊢ fix _f = _f (fix _f)

Tactic:
dsimp [fix]

Premises used: Fix.fix
-- Module: Mathlib.Control.LawfulFix
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
erw :
  curry (β := β) (γ := γ)
    ((OrderHom.comp (monotoneUncurry α β γ)
          ({ toFun := _f, monotone' := ⋯ : ((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' := ⋯ : ((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)))
| curry (β := β) (γ := γ) (fix (uncurry (β := β) (γ := γ) ∘ _f ∘ curry (β := β) (γ := γ)))

Tactic:
erw [LawfulFix.fix_eq (uncurry_curry_ωScottContinuous hc)]

Premises used: LawfulFix.fix_eq, Pi.uncurry_curry_ωScottContinuous
-- Module: Mathlib.Control.LawfulFix
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
conv_lhs :
  curry (β := β) (γ := γ)
      ((OrderHom.comp (monotoneUncurry α β γ)
            ({ toFun := _f, monotone' := ⋯ : ((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' := ⋯ : ((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 (β := β) (γ := γ))))
⊢ curry (β := β) (γ := γ) (fix (uncurry (β := β) (γ := γ) ∘ _f ∘ curry (β := β) (γ := γ))) =
    _f (curry (β := β) (γ := γ) (fix (uncurry (β := β) (γ := γ) ∘ _f ∘ curry (β := β) (γ := γ))))

Tactic:
conv_lhs => erw [LawfulFix.fix_eq (uncurry_curry_ωScottContinuous hc)]

Premises used: LawfulFix.fix_eq, Pi.uncurry_curry_ωScottContinuous
-- Module: Mathlib.Control.LawfulFix
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 (β := β) (γ := γ)
      ((OrderHom.comp (monotoneUncurry α β γ)
            ({ toFun := _f, monotone' := ⋯ : ((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' := ⋯ : ((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:
rfl
-- Module: Mathlib.Control.Monad.Basic
Goal:
α β : Type u
m : Type u → Type v
inst : Monad m
inst_1 : LawfulMonad m
f : α → β
x : m α
⊢ f <$> x = x >>= pure ∘ f

Tactic:
(bind_pure_comp f x).symm

Premises used: LawfulMonad.bind_pure_comp, Eq.symm
-- Module: Mathlib.Control.Monad.Cont
Goal:
r : Type u
m : Type u → Type v
α : Type w
f : m r → m r
x : ContT r m α
⊢ (map f x).run = f ∘ x.run

Tactic:
rfl

Premises used: ContT.run, ContT.map, rfl
-- Module: Mathlib.Control.Monad.Cont
Goal:
r : Type u
m : Type u → Type v
α β : Type w
f : (β → m r) → α → m r
x : ContT r m α
⊢ (withContT f x).run = x.run ∘ f

Tactic:
rfl

Premises used: ContT.withContT, ContT.run, rfl
-- Module: Mathlib.Control.Monad.Cont
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
h₁ : ∀ (x_1 : α → m r), x x_1 = y x_1
⊢ x = y

Tactic:
ext
-- Module: Mathlib.Control.Monad.Cont
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_1 : α → m r
⊢ x x_1 = y x_1

Tactic:
apply h
-- Module: Mathlib.Control.Monad.Cont
Goal:
r : Type u
m : Type u → Type v
α : Type w
f : (α → m r) → m r
k : α → m r
⊢ (mk f).run k = f k

Tactic:
rfl

Premises used: ContT.run, ContT.mk, rfl
-- Module: Mathlib.Control.Monad.Cont
Goal:
r : Type u
m : Type u → Type v
α : Type w
a : α
k : α → m r
⊢ run (pure a) k = k a

Tactic:
rfl

Premises used: ContT.run, rfl
-- Module: Mathlib.Control.Monad.Cont
Goal:
r : Type u
m : Type u → Type v
α β : Type w
x : ContT r m α
f : α → ContT r m β
k : β → m r
⊢ (x >>= f).run k = x.run fun (x : α) ↦ (f x).run k

Tactic:
rfl

Premises used: ContT.run, rfl
-- Module: Mathlib.Control.Monad.Cont
Goal:
r : Type u
m : Type u → Type v
α β : Type w
f : α → β
x : ContT r m α
k : β → m r
⊢ (f <$> x).run k = x.run (k ∘ f)

Tactic:
rfl

Premises used: ContT.run, rfl
-- Module: Mathlib.Control.Monad.Cont
Goal:
r : Type u
m : Type u → Type v
α β : Type w
f : ContT.{u, v, w} r m (α → β)
x : ContT r m α
k : β → m r
⊢ (f <*> x).run k = f.run fun (f : α → β) ↦ x.run (k ∘ f)

Tactic:
rfl

Premises used: ContT.run, rfl
-- Module: Mathlib.Control.Monad.Cont
Goal:
r : Type u
m : Type u → Type v
α β : Type w
x : ContT r m α
y : ContT r m β
k : α → m r
⊢ (x <* y).run k = x.run fun (x : α) ↦ y.run fun (x_1 : β) ↦ k x

Tactic:
rfl

Premises used: ContT.run, rfl
-- Module: Mathlib.Control.Monad.Cont
Goal:
r : Type u
m : Type u → Type v
α β : Type w
x : ContT r m α
y : ContT r m β
k : β → m r
⊢ run (x *> y) k = x.run fun (x : α) ↦ y.run k

Tactic:
rfl

Premises used: ContT.run, rfl
-- Module: Mathlib.Control.Monad.Cont
Goal:
r : Type u
m : Type u → Type v
α β : Type w
α_1 : Type u_1
x : ContT r m α_1
⊢ id <$> x = x

Tactic:
rfl
-- Module: Mathlib.Control.Monad.Cont
Goal:
r : Type u
m : Type u → Type v
α β : Type w
α_1 β_1 : Type u_1
x : α_1
f : α_1 → ContT r m β_1
h : ∀ (f_1 : β_1 → m r), (pure x >>= f).run f_1 = (f x).run f_1
⊢ pure x >>= f = f x

Tactic:
ext
-- Module: Mathlib.Control.Monad.Cont
Goal:
r : Type u
m : Type u → Type v
α β : Type w
α_1 β_1 : Type u_1
x : α_1
f : α_1 → ContT r m β_1
f_1 : β_1 → m r
⊢ (pure x >>= f).run f_1 = (f x).run f_1

Tactic:
rfl
-- Module: Mathlib.Control.Monad.Cont
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 γ
h : ∀ (f_1 : γ → m r), (x >>= f >>= g).run f_1 = run (x >>= fun (x : α_1) ↦ f x >>= g) f_1
⊢ x >>= f >>= g = x >>= fun (x : α_1) ↦ f x >>= g

Tactic:
ext
-- Module: Mathlib.Control.Monad.Cont
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 γ
f_1 : γ → m r
⊢ (x >>= f >>= g).run f_1 = run (x >>= fun (x : α_1) ↦ f x >>= g) f_1

Tactic:
rfl
-- Module: Mathlib.Control.Monad.Cont
Goal:
r : Type u
m : Type u → Type v
inst : Monad m
α : Type u
x : m α
k : α → m r
⊢ run (monadLift x) k = x >>= k

Tactic:
rfl

Premises used: ContT.run, ContT.mk, rfl
-- Module: Mathlib.Control.Monad.Cont
Goal:
r : Type u
m : Type u → Type v
inst : Monad m
inst_1 : LawfulMonad m
α β : Type u
x : m α
f : α → m β
h : ∀ (f_1 : β → m r), run (monadLift (x >>= f)) f_1 = run (monadLift x >>= monadLift ∘ f) f_1
⊢ Eq (α := ContT r m β) (monadLift (x >>= f)) (monadLift x >>= monadLift ∘ f)

Tactic:
ext
-- Module: Mathlib.Control.Monad.Cont
Goal:
r : Type u
m : Type u → Type v
inst : Monad m
inst_1 : LawfulMonad m
α β : Type u
x : m α
f : α → m β
f_1 : β → m r
⊢ run (monadLift (x >>= f)) f_1 = run (monadLift x >>= monadLift ∘ f) f_1

Tactic:
simp only [bind_assoc, run_bind, run_monadLift, Function.comp_apply]

Premises used: LawfulMonad.bind_assoc, ContT.run_monadLift, ContT.run_bind, Function.comp_apply
-- Module: Mathlib.Control.Monad.Cont
Goal:
r : Type u
m : Type u → Type v
α β : Type w
f : Label α (ContT r m) β → ContT r m α
k : α → m r
⊢ (callCC f).run k = (f { apply := fun (x : α) ↦ mk fun (x_1 : β → m r) ↦ k x : Label α (ContT r m) β }).run k

Tactic:
rfl

Premises used: ContT.run, ContT.mk, rfl
-- Module: Mathlib.Control.Monad.Cont
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 ω
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
⊢ 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

Tactic:
ext
-- Module: Mathlib.Control.Monad.Cont
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 ω
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:
rfl
-- Module: Mathlib.Control.Monad.Cont
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
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
⊢ Eq (α := ContT r m α_1) (callCC (β := β_1) fun (f : Label α_1 (ContT r m) β_1) ↦ goto f x >>= dead f) (pure x)

Tactic:
ext
-- Module: Mathlib.Control.Monad.Cont
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
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:
rfl
-- Module: Mathlib.Control.Monad.Cont
Goal:
r : Type u
m : Type u → Type v
α β : Type w
α_1 β_1 : Type u_1
dummy : ContT r m α_1
h : ∀ (f : α_1 → m r), run (callCC (β := β_1) fun (x : Label α_1 (ContT r m) β_1) ↦ dummy) f = dummy.run f
⊢ (callCC (β := β_1) fun (x : Label α_1 (ContT r m) β_1) ↦ dummy) = dummy

Tactic:
ext
-- Module: Mathlib.Control.Monad.Cont
Goal:
r : Type u
m : Type u → Type v
α β : Type w
α_1 β_1 : Type u_1
dummy : ContT r m α_1
f : α_1 → m r
⊢ run (callCC (β := β_1) fun (x : Label α_1 (ContT r m) β_1) ↦ dummy) f = dummy.run f

Tactic:
rfl
-- Module: Mathlib.Control.Monad.Cont
Goal:
r : Type u
m : Type u → Type v
α : Type w
ε : Type u_1
inst : MonadExceptOf ε m
e : ε
f : α → m r
⊢ run (throw e) f = throw e

Tactic:
rfl

Premises used: ContT.run, ContT.mk, rfl
-- Module: Mathlib.Control.Monad.Cont
Goal:
r : Type u
m : Type u → Type v
α : Type w
ε : Type u_1
inst : MonadExceptOf ε m
act : ContT r m α
h : ε → ContT r m α
f : α → m r
⊢ (tryCatch act h).run f = tryCatch (act.run f) fun (e : ε) ↦ (h e).run f

Tactic:
rfl

Premises used: ContT.run, ContT.mk, rfl
-- Module: Mathlib.Control.Monad.Cont
Goal:
m : Type u → Type v
inst : Monad m
α β ε : Type u
x : Label (Except ε α) m β
i : α
mk :
  ∀ (apply : Except ε α → m β),
    goto (mkLabel { apply := apply : Label (Except ε α) m β }) i =
      ExceptT.mk (Except.ok <$> goto { apply := apply : Label (Except ε α) m β } (Except.ok i))
⊢ goto (mkLabel x) i = ExceptT.mk (Except.ok <$> goto x (Except.ok i))

Tactic:
cases x
-- Module: Mathlib.Control.Monad.Cont
Goal:
m : Type u → Type v
inst : Monad m
α β ε : Type u
i : α
apply : Except ε α → m β
⊢ goto (mkLabel { apply := apply : Label (Except ε α) m β }) i =
    mk (Except.ok <$> goto { apply := apply : Label (Except ε α) m β } (Except.ok i))

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
cmd : ExceptT ε m α
next : Label.{u, v, u} ω (ExceptT ε m) γ → α → ExceptT ε m ω
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)
⊢ 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

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

Premises used: MonadCont.callCC, ExceptT.run_bind, LawfulMonadCont.callCC_bind_right, 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
cmd : ExceptT ε m α
next : Label.{u, v, u} ω (ExceptT ε m) γ → α → ExceptT ε m ω
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))
⊢ 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:
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
cmd : ExceptT ε m α
next : Label.{u, v, u} ω (ExceptT ε m) γ → α → ExceptT ε m ω
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)
⊢ 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:
dsimp
-- 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 ω
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))
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))
⊢ 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:
congr with ⟨⟩
-- 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.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:
simp [@callCC_dummy m _]

Premises used: LawfulMonadCont.callCC_dummy