mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Control.Bitraversable.Instances

Goal state before:
pp: t : Type u → Type u → Type u
inst✝² : Bitraversable t
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : LawfulBitraversable t
⊢ LawfulBitraversable (_root_.flip t)

Tactic:
constructor

Goal state after:
case id_bitraverse
t : Type u → Type u → Type u
inst✝² : Bitraversable t
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : LawfulBitraversable t
⊢ ∀ {α β : Type u} (x : _root_.flip t α β), bitraverse pure pure x = pure x

case comp_bitraverse
t : Type u → Type u → Type u
inst✝² : Bitraversable t
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : LawfulBitraversable t
⊢ ∀ {F G : Type u → Type u} [inst : Applicative F] [inst_1 : Applicative G] [LawfulApplicative F] [LawfulApplicative G]
    {α α' β β' γ γ' : Type u} (f : β → F γ) (f' : β' → F γ') (g : α → G β) (g' : α' → G β') (x : _root_.flip t α α'),
    bitraverse (Comp.mk ∘ map f ∘ g) (Comp.mk ∘ map f' ∘ g') x = Comp.mk (bitraverse f f' <$> bitraverse g g' x)

case bitraverse_eq_bimap_id
t : Type u → Type u → Type u
inst✝² : Bitraversable t
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : LawfulBitraversable t
⊢ ∀ {α α' β β' : Type u} (f : α → β) (f' : α' → β') (x : _root_.flip t α α'),
    bitraverse (pure ∘ f) (pure ∘ f') x = pure (bimap f f' x)

case binaturality
t : Type u → Type u → Type u
inst✝² : Bitraversable t
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : LawfulBitraversable t
⊢ ∀ {F G : Type u → Type u} [inst : Applicative F] [inst_1 : Applicative G] [LawfulApplicative F] [LawfulApplicative G]
    (η : ApplicativeTransformation F G) {α α' β β' : Type u} (f : α → F β) (f' : α' → F β') (x : _root_.flip t α α'),
    (fun {α} ↦ η.app α) (bitraverse f f' x) = bitraverse ((fun {α} ↦ η.app α) ∘ f) ((fun {α} ↦ η.app α) ∘ f') x
Module: Mathlib.Control.Bitraversable.Instances

Goal state before:
pp: t : Type u → Type u → Type u
inst✝² : Bitraversable t
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : LawfulBitraversable t
α : Type u
⊢ LawfulTraversable (t α)

Tactic:
constructor

Goal state after:
case id_traverse
t : Type u → Type u → Type u
inst✝² : Bitraversable t
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : LawfulBitraversable t
α : Type u
⊢ ∀ {α_1 : Type u} (x : t α α_1), traverse pure x = pure x

case comp_traverse
t : Type u → Type u → Type u
inst✝² : Bitraversable t
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : LawfulBitraversable t
α : Type u
⊢ ∀ {F G : Type u → Type u} [inst : Applicative F] [inst_1 : Applicative G] [LawfulApplicative F] [LawfulApplicative G]
    {α_1 β γ : Type u} (f : β → F γ) (g : α_1 → G β) (x : t α α_1),
    traverse (Comp.mk ∘ map f ∘ g) x = Comp.mk (traverse f <$> traverse g x)

case traverse_eq_map_id
t : Type u → Type u → Type u
inst✝² : Bitraversable t
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : LawfulBitraversable t
α : Type u
⊢ ∀ {α_1 β : Type u} (f : α_1 → β) (x : t α α_1), traverse (pure ∘ f) x = pure (f <$> x)

case naturality
t : Type u → Type u → Type u
inst✝² : Bitraversable t
F : Type u → Type u
inst✝¹ : Applicative F
inst✝ : LawfulBitraversable t
α : Type u
⊢ ∀ {F G : Type u → Type u} [inst : Applicative F] [inst_1 : Applicative G] [LawfulApplicative F] [LawfulApplicative G]
    (η : ApplicativeTransformation F G) {α_1 β : Type u} (f : α_1 → F β) (x : t α α_1),
    (fun {α} ↦ η.app α) (traverse f x) = traverse ((fun {α} ↦ η.app α) ∘ f) x
Module: Mathlib.Control.Bitraversable.Instances

Goal state before:
pp: t : Type u → Type u → Type u
inst✝⁵ : Bitraversable t
F G : Type u → Type u
inst✝⁴ : Traversable F
inst✝³ : Traversable G
inst✝² : LawfulTraversable F
inst✝¹ : LawfulTraversable G
inst✝ : LawfulBitraversable t
⊢ LawfulBitraversable (bicompl t F G)

Tactic:
constructor

Goal state after:
case id_bitraverse
t : Type u → Type u → Type u
inst✝⁵ : Bitraversable t
F G : Type u → Type u
inst✝⁴ : Traversable F
inst✝³ : Traversable G
inst✝² : LawfulTraversable F
inst✝¹ : LawfulTraversable G
inst✝ : LawfulBitraversable t
⊢ ∀ {α β : Type u} (x : bicompl t F G α β), bitraverse pure pure x = pure x

case comp_bitraverse
t : Type u → Type u → Type u
inst✝⁵ : Bitraversable t
F G : Type u → Type u
inst✝⁴ : Traversable F
inst✝³ : Traversable G
inst✝² : LawfulTraversable F
inst✝¹ : LawfulTraversable G
inst✝ : LawfulBitraversable t
⊢ ∀ {F_1 G_1 : Type u → Type u} [inst : Applicative F_1] [inst_1 : Applicative G_1] [LawfulApplicative F_1]
    [LawfulApplicative G_1] {α α' β β' γ γ' : Type u} (f : β → F_1 γ) (f' : β' → F_1 γ') (g : α → G_1 β)
    (g' : α' → G_1 β') (x : bicompl t F G α α'),
    bitraverse (Functor.Comp.mk ∘ Functor.map f ∘ g) (Functor.Comp.mk ∘ Functor.map f' ∘ g') x =
      Functor.Comp.mk (bitraverse f f' <$> bitraverse g g' x)

case bitraverse_eq_bimap_id
t : Type u → Type u → Type u
inst✝⁵ : Bitraversable t
F G : Type u → Type u
inst✝⁴ : Traversable F
inst✝³ : Traversable G
inst✝² : LawfulTraversable F
inst✝¹ : LawfulTraversable G
inst✝ : LawfulBitraversable t
⊢ ∀ {α α' β β' : Type u} (f : α → β) (f' : α' → β') (x : bicompl t F G α α'),
    bitraverse (pure ∘ f) (pure ∘ f') x = pure (bimap f f' x)

case binaturality
t : Type u → Type u → Type u
inst✝⁵ : Bitraversable t
F G : Type u → Type u
inst✝⁴ : Traversable F
inst✝³ : Traversable G
inst✝² : LawfulTraversable F
inst✝¹ : LawfulTraversable G
inst✝ : LawfulBitraversable t
⊢ ∀ {F_1 G_1 : Type u → Type u} [inst : Applicative F_1] [inst_1 : Applicative G_1] [LawfulApplicative F_1]
    [LawfulApplicative G_1] (η : ApplicativeTransformation F_1 G_1) {α α' β β' : Type u} (f : α → F_1 β)
    (f' : α' → F_1 β') (x : bicompl t F G α α'),
    (fun {α} ↦ η.app α) (bitraverse f f' x) = bitraverse ((fun {α} ↦ η.app α) ∘ f) ((fun {α} ↦ η.app α) ∘ f') x
Module: Mathlib.Control.Bitraversable.Instances

Goal state before:
pp: t : Type u → Type u → Type u
inst✝³ : Bitraversable t
F : Type u → Type u
inst✝² : Traversable F
inst✝¹ : LawfulTraversable F
inst✝ : LawfulBitraversable t
⊢ LawfulBitraversable (bicompr F t)

Tactic:
constructor

Goal state after:
case id_bitraverse
t : Type u → Type u → Type u
inst✝³ : Bitraversable t
F : Type u → Type u
inst✝² : Traversable F
inst✝¹ : LawfulTraversable F
inst✝ : LawfulBitraversable t
⊢ ∀ {α β : Type u} (x : bicompr F t α β), bitraverse pure pure x = pure x

case comp_bitraverse
t : Type u → Type u → Type u
inst✝³ : Bitraversable t
F : Type u → Type u
inst✝² : Traversable F
inst✝¹ : LawfulTraversable F
inst✝ : LawfulBitraversable t
⊢ ∀ {F_1 G : Type u → Type u} [inst : Applicative F_1] [inst_1 : Applicative G] [LawfulApplicative F_1]
    [LawfulApplicative G] {α α' β β' γ γ' : Type u} (f : β → F_1 γ) (f' : β' → F_1 γ') (g : α → G β) (g' : α' → G β')
    (x : bicompr F t α α'),
    bitraverse (Functor.Comp.mk ∘ Functor.map f ∘ g) (Functor.Comp.mk ∘ Functor.map f' ∘ g') x =
      Functor.Comp.mk (bitraverse f f' <$> bitraverse g g' x)

case bitraverse_eq_bimap_id
t : Type u → Type u → Type u
inst✝³ : Bitraversable t
F : Type u → Type u
inst✝² : Traversable F
inst✝¹ : LawfulTraversable F
inst✝ : LawfulBitraversable t
⊢ ∀ {α α' β β' : Type u} (f : α → β) (f' : α' → β') (x : bicompr F t α α'),
    bitraverse (pure ∘ f) (pure ∘ f') x = pure (bimap f f' x)

case binaturality
t : Type u → Type u → Type u
inst✝³ : Bitraversable t
F : Type u → Type u
inst✝² : Traversable F
inst✝¹ : LawfulTraversable F
inst✝ : LawfulBitraversable t
⊢ ∀ {F_1 G : Type u → Type u} [inst : Applicative F_1] [inst_1 : Applicative G] [LawfulApplicative F_1]
    [LawfulApplicative G] (η : ApplicativeTransformation F_1 G) {α α' β β' : Type u} (f : α → F_1 β) (f' : α' → F_1 β')
    (x : bicompr F t α α'),
    (fun {α} ↦ η.app α) (bitraverse f f' x) = bitraverse ((fun {α} ↦ η.app α) ∘ f) ((fun {α} ↦ η.app α) ∘ f') x
Module: Mathlib.Control.EquivFunctor.Instances

Goal state before:
pp: α : Type ?u.3
⊢ (fun p ↦ ((Equiv.refl α).symm.trans p).trans (Equiv.refl α)) = id

Tactic:
ext

Goal state after:
α : Type ?u.3
x✝¹ : Perm α
x✝ : α
⊢ (((Equiv.refl α).symm.trans x✝¹).trans (Equiv.refl α)) x✝ = (id x✝¹) x✝
Module: Mathlib.Control.EquivFunctor.Instances

Goal state before:
pp: α✝ β✝ γ✝ : Type ?u.3
x✝¹ : α✝ ≃ β✝
x✝ : β✝ ≃ γ✝
⊢ (fun p ↦ ((x✝¹.trans x✝).symm.trans p).trans (x✝¹.trans x✝)) =
    (fun p ↦ (x✝.symm.trans p).trans x✝) ∘ fun p ↦ (x✝¹.symm.trans p).trans x✝¹

Tactic:
ext

Goal state after:
α✝ β✝ γ✝ : Type ?u.3
x✝³ : α✝ ≃ β✝
x✝² : β✝ ≃ γ✝
x✝¹ : Perm α✝
x✝ : γ✝
⊢ (((x✝³.trans x✝²).symm.trans x✝¹).trans (x✝³.trans x✝²)) x✝ =
    (((fun p ↦ (x✝².symm.trans p).trans x✝²) ∘ fun p ↦ (x✝³.symm.trans p).trans x✝³) x✝¹) x✝
Module: Mathlib.Control.EquivFunctor.Instances

Goal state before:
pp: α : Type ?u.4
⊢ (fun s ↦ Finset.map (Equiv.refl α).toEmbedding s) = id

Tactic:
ext

Goal state after:
α : Type ?u.4
x✝ : Finset α
a✝ : α
⊢ a✝ ∈ Finset.map (Equiv.refl α).toEmbedding x✝ ↔ a✝ ∈ id x✝
Module: Mathlib.Control.EquivFunctor.Instances

Goal state before:
pp: α✝ β✝ γ✝ : Type ?u.4
k : α✝ ≃ β✝
h : β✝ ≃ γ✝
⊢ (fun s ↦ Finset.map (k.trans h).toEmbedding s) =
    (fun s ↦ Finset.map h.toEmbedding s) ∘ fun s ↦ Finset.map k.toEmbedding s

Tactic:
ext

Goal state after:
α✝ β✝ γ✝ : Type ?u.4
k : α✝ ≃ β✝
h : β✝ ≃ γ✝
x✝ : Finset α✝
a✝ : γ✝
⊢ a✝ ∈ Finset.map (k.trans h).toEmbedding x✝ ↔
    a✝ ∈ ((fun s ↦ Finset.map h.toEmbedding s) ∘ fun s ↦ Finset.map k.toEmbedding s) x✝
Module: Mathlib.Control.EquivFunctor.Instances

Goal state before:
pp: α : Type ?u.4
⊢ (fun x ↦ Fintype.ofBijective ⇑(Equiv.refl α) ⋯) = id

Tactic:
ext

Goal state after:
α : Type ?u.4
x✝ : Fintype α
⊢ Fintype.ofBijective ⇑(Equiv.refl α) ⋯ = id x✝
Module: Mathlib.Control.Fold

Goal state before:
pp: m : Type u → Type u
inst✝ : Monad m
α β : Type u
f : α → β → β
x✝¹ x✝ : FreeMonoid α
⊢ ConcreteCategory.hom (↾flip (List.foldr f) (FreeMonoid.toList (x✝¹ * x✝))) =
    ConcreteCategory.hom (↾flip (List.foldr f) (FreeMonoid.toList x✝¹) * ↾flip (List.foldr f) (FreeMonoid.toList x✝))

Tactic:
ext

Goal state after:
m : Type u → Type u
inst✝ : Monad m
α β : Type u
f : α → β → β
x✝² x✝¹ : FreeMonoid α
x✝ : β
⊢ (ConcreteCategory.hom (↾flip (List.foldr f) (FreeMonoid.toList (x✝² * x✝¹)))).toFun x✝ =
    (ConcreteCategory.hom
          (↾flip (List.foldr f) (FreeMonoid.toList x✝²) * ↾flip (List.foldr f) (FreeMonoid.toList x✝¹))).toFun
      x✝
Module: Mathlib.Control.Fold

Goal state before:
pp: α β : Type u
m : Type u → Type u
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : β → α → m α
⊢ ⇑(foldrM.ofFreeMonoid f) ∘ FreeMonoid.of = foldrM.mk ∘ f

Tactic:
ext

Goal state after:
α β : Type u
m : Type u → Type u
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : β → α → m α
x✝ : β
⊢ (⇑(foldrM.ofFreeMonoid f) ∘ FreeMonoid.of) x✝ = (foldrM.mk ∘ f) x✝
Module: Mathlib.Control.Functor.Multivariate

Goal state before:
pp: n : ℕ
α β : TypeVec.{u} n
F : TypeVec.{u} n → Type v
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
P : F α → Prop
q : F β → Prop
f : α ⟹ β
g : β ⟹ α
h₀ : f ⊚ g = TypeVec.id
h₁ : ∀ (u : F α), P u ↔ q (f <$$> u)
⊢ (∃ u, P u) ↔ ∃ u, q u

Tactic:
constructor

Goal state after:
case mp
n : ℕ
α β : TypeVec.{u} n
F : TypeVec.{u} n → Type v
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
P : F α → Prop
q : F β → Prop
f : α ⟹ β
g : β ⟹ α
h₀ : f ⊚ g = TypeVec.id
h₁ : ∀ (u : F α), P u ↔ q (f <$$> u)
⊢ (∃ u, P u) → ∃ u, q u

case mpr
n : ℕ
α β : TypeVec.{u} n
F : TypeVec.{u} n → Type v
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
P : F α → Prop
q : F β → Prop
f : α ⟹ β
g : β ⟹ α
h₀ : f ⊚ g = TypeVec.id
h₁ : ∀ (u : F α), P u ↔ q (f <$$> u)
⊢ (∃ u, q u) → ∃ u, P u
Module: Mathlib.Control.LawfulFix

Goal state before:
pp: case pos
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∃ i, (approx (⇑f) i a).Dom
⊢ b ∈ approx (⇑f) (Nat.find h₀).succ a ↔ ∃ i, b ∈ approx (⇑f) i a

Tactic:
constructor

Goal state after:
case pos.mp
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∃ i, (approx (⇑f) i a).Dom
⊢ b ∈ approx (⇑f) (Nat.find h₀).succ a → ∃ i, b ∈ approx (⇑f) i a

case pos.mpr
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
h₀ : ∃ i, (approx (⇑f) i a).Dom
⊢ (∃ i, b ∈ approx (⇑f) i a) → b ∈ approx (⇑f) (Nat.find h₀).succ a
Module: Mathlib.Control.Monad.Writer

Goal state before:
pp: M : Type u → Type v
α β ω ρ σ : Type u
inst✝² : Monad M
inst✝¹ : Monoid ω
inst✝ : LawfulMonad M
α✝ : Type u
x✝ : WriterT ω M α✝
⊢ id <$> x✝ = x✝

Tactic:
ext

Goal state after:
M : Type u → Type v
α β ω ρ σ : Type u
inst✝² : Monad M
inst✝¹ : Monoid ω
inst✝ : LawfulMonad M
α✝ : Type u
x✝ : WriterT ω M α✝
⊢ (id <$> x✝).run = x✝.run
Module: Mathlib.Control.Monad.Writer

Goal state before:
pp: M : Type u → Type v
α β ω ρ σ : Type u
inst✝² : Monad M
inst✝¹ : Monoid ω
inst✝ : LawfulMonad M
α✝ β✝ : Type u
x✝¹ : α✝
x✝ : α✝ → WriterT ω M β✝
⊢ pure x✝¹ >>= x✝ = x✝ x✝¹

Tactic:
ext

Goal state after:
M : Type u → Type v
α β ω ρ σ : Type u
inst✝² : Monad M
inst✝¹ : Monoid ω
inst✝ : LawfulMonad M
α✝ β✝ : Type u
x✝¹ : α✝
x✝ : α✝ → WriterT ω M β✝
⊢ (pure x✝¹ >>= x✝).run = (x✝ x✝¹).run
Module: Mathlib.Control.Monad.Writer

Goal state before:
pp: M : Type u → Type v
α β ω ρ σ : Type u
inst✝² : Monad M
inst✝¹ : Monoid ω
inst✝ : LawfulMonad M
α✝ β✝ γ✝ : Type u
x✝² : WriterT ω M α✝
x✝¹ : α✝ → WriterT ω M β✝
x✝ : β✝ → WriterT ω M γ✝
⊢ x✝² >>= x✝¹ >>= x✝ = x✝² >>= fun x ↦ x✝¹ x >>= x✝

Tactic:
ext

Goal state after:
M : Type u → Type v
α β ω ρ σ : Type u
inst✝² : Monad M
inst✝¹ : Monoid ω
inst✝ : LawfulMonad M
α✝ β✝ γ✝ : Type u
x✝² : WriterT ω M α✝
x✝¹ : α✝ → WriterT ω M β✝
x✝ : β✝ → WriterT ω M γ✝
⊢ (x✝² >>= x✝¹ >>= x✝).run = (x✝² >>= fun x ↦ x✝¹ x >>= x✝).run
Module: Mathlib.Control.Monad.Writer

Goal state before:
pp: M : Type u → Type v
α β ω ρ σ : Type u
inst✝² : Monad M
inst✝¹ : Monoid ω
inst✝ : LawfulMonad M
α✝ β✝ : Type u
x✝¹ : α✝ → β✝
x✝ : WriterT ω M α✝
⊢ (do
      let y ← x✝
      pure (x✝¹ y)) =
    x✝¹ <$> x✝

Tactic:
ext

Goal state after:
M : Type u → Type v
α β ω ρ σ : Type u
inst✝² : Monad M
inst✝¹ : Monoid ω
inst✝ : LawfulMonad M
α✝ β✝ : Type u
x✝¹ : α✝ → β✝
x✝ : WriterT ω M α✝
⊢ (do
        let y ← x✝
        pure (x✝¹ y)).run =
    (x✝¹ <$> x✝).run
Module: Mathlib.Control.Monad.Cont

Goal state before:
pp: 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

Tactic:
ext

Goal state after:
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✝ : α → m r
⊢ x x✝ = y x✝
Module: Mathlib.Control.Monad.Cont

Goal state before:
pp: r : Type u
m : Type u → Type v
α β : Type w
α✝ β✝ : Type u_1
x✝ : α✝
f✝ : α✝ → ContT r m β✝
⊢ pure x✝ >>= f✝ = f✝ x✝

Tactic:
ext

Goal state after:
r : Type u
m : Type u → Type v
α β : Type w
α✝ β✝ : Type u_1
x✝ : α✝
f✝¹ : α✝ → ContT r m β✝
f✝ : β✝ → m r
⊢ (pure x✝ >>= f✝¹).run f✝ = (f✝¹ x✝).run f✝
Module: Mathlib.Control.Monad.Cont

Goal state before:
pp: r : Type u
m : Type u → Type v
α β : Type w
α✝ β✝ γ✝ : Type u_1
x✝ : ContT r m α✝
f✝ : α✝ → ContT r m β✝
g✝ : β✝ → ContT r m γ✝
⊢ x✝ >>= f✝ >>= g✝ = x✝ >>= fun x ↦ f✝ x >>= g✝

Tactic:
ext

Goal state after:
r : Type u
m : Type u → Type v
α β : Type w
α✝ β✝ γ✝ : Type u_1
x✝ : ContT r m α✝
f✝¹ : α✝ → ContT r m β✝
g✝ : β✝ → ContT r m γ✝
f✝ : γ✝ → m r
⊢ (x✝ >>= f✝¹ >>= g✝).run f✝ = (x✝ >>= fun x ↦ f✝¹ x >>= g✝).run f✝
Module: Mathlib.Control.Monad.Cont

Goal state before:
pp: r : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α β : Type u
x : m α
f : α → m β
⊢ monadLift (x >>= f) = monadLift x >>= monadLift ∘ f

Tactic:
ext

Goal state after:
r : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α β : Type u
x : m α
f : α → m β
f✝ : β → m r
⊢ (monadLift (x >>= f)).run f✝ = (monadLift x >>= monadLift ∘ f).run f✝
Module: Mathlib.Control.Monad.Cont

Goal state before:
pp: r : Type u
m : Type u → Type v
α β : Type w
α✝ ω✝ γ✝ : Type u_1
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

Tactic:
ext

Goal state after:
r : Type u
m : Type u → Type v
α β : Type w
α✝ ω✝ γ✝ : Type u_1
cmd✝ : ContT r m α✝
next✝ : Label ω✝ (ContT r m) γ✝ → α✝ → ContT r m ω✝
f✝ : ω✝ → m r
⊢ (callCC fun f ↦ cmd✝ >>= next✝ f).run f✝ =
    (do
          let x ← cmd✝
          callCC fun f ↦ next✝ f x).run
      f✝
Module: Mathlib.Control.Monad.Cont

Goal state before:
pp: r : Type u
m : Type u → Type v
α β : Type w
α✝ β✝ : Type u_1
x✝ : α✝
dead✝ : Label α✝ (ContT r m) β✝ → β✝ → ContT r m α✝
⊢ (callCC fun f ↦ goto f x✝ >>= dead✝ f) = pure x✝

Tactic:
ext

Goal state after:
r : Type u
m : Type u → Type v
α β : Type w
α✝ β✝ : Type u_1
x✝ : α✝
dead✝ : Label α✝ (ContT r m) β✝ → β✝ → ContT r m α✝
f✝ : α✝ → m r
⊢ (callCC fun f ↦ goto f x✝ >>= dead✝ f).run f✝ = (pure x✝).run f✝
Module: Mathlib.Control.Monad.Cont

Goal state before:
pp: r : Type u
m : Type u → Type v
α β : Type w
α✝ β✝ : Type u_1
dummy✝ : ContT r m α✝
⊢ (callCC fun x ↦ dummy✝) = dummy✝

Tactic:
ext

Goal state after:
r : Type u
m : Type u → Type v
α β : Type w
α✝ β✝ : Type u_1
dummy✝ : ContT r m α✝
f✝ : α✝ → m r
⊢ (callCC fun x ↦ dummy✝).run f✝ = dummy✝.run f✝
Module: Mathlib.Control.Monad.Cont

Goal state before:
pp: 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 ← cmd✝.run
      callCC fun f ↦
          match 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 ↦ (next✝ (ExceptT.mkLabel x_1) x).run)

Tactic:
ext

Goal state after:
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 ← cmd✝.run
        callCC fun f ↦
            match x with
            | Except.ok x => (next✝ (ExceptT.mkLabel f) x).run
            | Except.error e => pure (Except.error e)).run =
    (do
        let x ← cmd✝
        ExceptT.mk (callCC fun x_1 ↦ (next✝ (ExceptT.mkLabel x_1) x).run)).run
Module: Mathlib.Control.Monad.Cont

Goal state before:
pp: 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✝

Tactic:
ext

Goal state after:
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✝))).run = (pure x✝).run
Module: Mathlib.Control.Monad.Cont

Goal state before:
pp: m : Type u → Type v
inst✝² : Monad m
ε : Type u
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ β✝ : Type u
dummy✝ : ExceptT ε m α✝
⊢ ExceptT.mk dummy✝.run = dummy✝

Tactic:
ext

Goal state after:
m : Type u → Type v
inst✝² : Monad m
ε : Type u
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ β✝ : Type u
dummy✝ : ExceptT ε m α✝
⊢ (ExceptT.mk dummy✝.run).run = dummy✝.run
Module: Mathlib.Control.Monad.Cont

Goal state before:
pp: 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✝

Tactic:
ext

Goal state after:
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).run = (pure x✝).run
Module: Mathlib.Control.Monad.Cont

Goal state before:
pp: m : Type u → Type v
inst✝² : Monad m
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ β✝ : Type u
dummy✝ : OptionT m α✝
⊢ (callCC fun x ↦ dummy✝) = dummy✝

Tactic:
ext

Goal state after:
m : Type u → Type v
inst✝² : Monad m
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ β✝ : Type u
dummy✝ : OptionT m α✝
⊢ (callCC fun x ↦ dummy✝).run = dummy✝.run
Module: Mathlib.Control.Monad.Cont

Goal state before:
pp: m : Type u → Type v
σ : Type u
inst✝² : Monad m
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ ω✝ γ✝ : Type u
cmd✝ : StateT σ m α✝
next✝ : Label ω✝ (StateT σ m) γ✝ → α✝ → StateT σ m ω✝
⊢ (StateT.mk fun r ↦ do
      let x ← cmd✝.run r
      callCC fun f ↦ (next✝ (StateT.mkLabel f) x.fst).run x.snd) =
    do
    let x ← cmd✝
    StateT.mk fun r ↦ callCC fun f' ↦ (next✝ (StateT.mkLabel f') x).run r

Tactic:
ext

Goal state after:
m : Type u → Type v
σ : Type u
inst✝² : Monad m
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ ω✝ γ✝ : Type u
cmd✝ : StateT σ m α✝
next✝ : Label ω✝ (StateT σ m) γ✝ → α✝ → StateT σ m ω✝
s✝ : σ
⊢ (StateT.mk fun r ↦ do
          let x ← cmd✝.run r
          callCC fun f ↦ (next✝ (StateT.mkLabel f) x.fst).run x.snd).run
      s✝ =
    (do
          let x ← cmd✝
          StateT.mk fun r ↦ callCC fun f' ↦ (next✝ (StateT.mkLabel f') x).run r).run
      s✝
Module: Mathlib.Control.Monad.Cont

Goal state before:
pp: m : Type u → Type v
σ : Type u
inst✝² : Monad m
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ β✝ : Type u
x✝ : α✝
dead✝ : Label α✝ (StateT σ m) β✝ → β✝ → StateT σ m α✝
⊢ (StateT.mk fun r ↦ pure (x✝, r)) = pure x✝

Tactic:
ext

Goal state after:
m : Type u → Type v
σ : Type u
inst✝² : Monad m
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ β✝ : Type u
x✝ : α✝
dead✝ : Label α✝ (StateT σ m) β✝ → β✝ → StateT σ m α✝
s✝ : σ
⊢ (StateT.mk fun r ↦ pure (x✝, r)).run s✝ = (pure x✝).run s✝
Module: Mathlib.Control.Monad.Cont

Goal state before:
pp: m : Type u → Type v
σ : Type u
inst✝² : Monad m
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ β✝ : Type u
dummy✝ : StateT σ m α✝
⊢ (StateT.mk fun r ↦ dummy✝.run r) = dummy✝

Tactic:
ext

Goal state after:
m : Type u → Type v
σ : Type u
inst✝² : Monad m
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ β✝ : Type u
dummy✝ : StateT σ m α✝
s✝ : σ
⊢ (StateT.mk fun r ↦ dummy✝.run r).run s✝ = dummy✝.run s✝
Module: Mathlib.Control.Monad.Cont

Goal state before:
pp: m : Type u → Type v
ρ : Type u
inst✝² : Monad m
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ ω✝ γ✝ : Type u
cmd✝ : ReaderT ρ m α✝
next✝ : Label ω✝ (ReaderT ρ m) γ✝ → α✝ → ReaderT ρ m ω✝
⊢ (ReaderT.mk fun r ↦ do
      let x ← cmd✝.run r
      callCC fun f ↦ (next✝ (ReaderT.mkLabel ρ f) x).run r) =
    do
    let x ← cmd✝
    ReaderT.mk fun r ↦ callCC fun f' ↦ (next✝ (ReaderT.mkLabel ρ f') x).run r

Tactic:
ext

Goal state after:
m : Type u → Type v
ρ : Type u
inst✝² : Monad m
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ ω✝ γ✝ : Type u
cmd✝ : ReaderT ρ m α✝
next✝ : Label ω✝ (ReaderT ρ m) γ✝ → α✝ → ReaderT ρ m ω✝
ctx✝ : ρ
⊢ (ReaderT.mk fun r ↦ do
          let x ← cmd✝.run r
          callCC fun f ↦ (next✝ (ReaderT.mkLabel ρ f) x).run r).run
      ctx✝ =
    (do
          let x ← cmd✝
          ReaderT.mk fun r ↦ callCC fun f' ↦ (next✝ (ReaderT.mkLabel ρ f') x).run r).run
      ctx✝
Module: Mathlib.Control.Monad.Cont

Goal state before:
pp: m : Type u → Type v
ρ : Type u
inst✝² : Monad m
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ β✝ : Type u
x✝ : α✝
dead✝ : Label α✝ (ReaderT ρ m) β✝ → β✝ → ReaderT ρ m α✝
⊢ (ReaderT.mk fun r ↦ pure x✝) = pure x✝

Tactic:
ext

Goal state after:
m : Type u → Type v
ρ : Type u
inst✝² : Monad m
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ β✝ : Type u
x✝ : α✝
dead✝ : Label α✝ (ReaderT ρ m) β✝ → β✝ → ReaderT ρ m α✝
ctx✝ : ρ
⊢ (ReaderT.mk fun r ↦ pure x✝).run ctx✝ = (pure x✝).run ctx✝
Module: Mathlib.Control.Monad.Cont

Goal state before:
pp: m : Type u → Type v
ρ : Type u
inst✝² : Monad m
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ β✝ : Type u
dummy✝ : ReaderT ρ m α✝
⊢ (ReaderT.mk fun r ↦ dummy✝.run r) = dummy✝

Tactic:
ext

Goal state after:
m : Type u → Type v
ρ : Type u
inst✝² : Monad m
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ β✝ : Type u
dummy✝ : ReaderT ρ m α✝
ctx✝ : ρ
⊢ (ReaderT.mk fun r ↦ dummy✝.run r).run ctx✝ = dummy✝.run ctx✝