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

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

Tactic:
intros

Goal state after:
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✝ G✝ : Type u → Type u
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
η✝ : ApplicativeTransformation F✝ G✝
α✝ α'✝ β✝ β'✝ : Type u
f✝ : α✝ → F✝ β✝
f'✝ : α'✝ → F✝ β'✝
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: 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

Tactic:
intros

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✝
Module: Mathlib.Control.Bitraversable.Instances

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

Tactic:
intros

Goal state after:
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✝ G✝ : Type u → Type u
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
α✝ α'✝ β✝ β'✝ γ✝ γ'✝ : Type u
f✝ : β✝ → F✝ γ✝
f'✝ : β'✝ → F✝ γ'✝
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✝)
Module: Mathlib.Control.Bitraversable.Instances

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

Tactic:
intros

Goal state after:
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✝)
Module: Mathlib.Control.Bitraversable.Instances

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

Tactic:
intros

Goal state after:
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✝ G✝ : Type u → Type u
inst✝³ : Applicative F✝
inst✝² : Applicative G✝
inst✝¹ : LawfulApplicative F✝
inst✝ : LawfulApplicative G✝
η✝ : ApplicativeTransformation F✝ G✝
α✝ α'✝ β✝ β'✝ : Type u
f✝ : α✝ → F✝ β✝
f'✝ : α'✝ → F✝ β'✝
x✝ : bicompr F t α✝ α'✝
⊢ (fun {α} ↦ η✝.app α) (bitraverse f✝ f'✝ x✝) = bitraverse ((fun {α} ↦ η✝.app α) ∘ f✝) ((fun {α} ↦ η✝.app α) ∘ f'✝) x✝
Module: Mathlib.Control.Fix

Goal state before:
pp: α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ∃ i, (Fix.approx f i x).Dom
p : ℕ → Prop := fun i ↦ (Fix.approx f i x).Dom
k : ℕ
this : p (k + ↑Upto.zero)
⊢ Nat.find h' = k + ↑Upto.zero →
    (assert (∃ i, (Fix.approx f i x).Dom) fun h ↦ ⋯.fix (fixAux f) Upto.zero x) = Fix.approx f (k + 1) x

Tactic:
assert_pos h'

Goal state after:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) → (a : α) → Part (β a)
x : α
h' : ∃ i, (Fix.approx f i x).Dom
p : ℕ → Prop := fun i ↦ (Fix.approx f i x).Dom
k : ℕ
this : p (k + ↑Upto.zero)
⊢ Nat.find h' = k + ↑Upto.zero → ⋯.fix (fixAux f) Upto.zero x = Fix.approx f (k + 1) x
Module: Mathlib.Control.Fold

Goal state before:
pp: m : Type u → Type u
inst✝ : Monad m
α β : Type u
f : β → α → β
⊢ ∀ (x y : FreeMonoid α),
    op (↾flip (List.foldl f) (FreeMonoid.toList (x * y))) =
      op (↾flip (List.foldl f) (FreeMonoid.toList x)) * op (↾flip (List.foldl f) (FreeMonoid.toList y))

Tactic:
intros

Goal state after:
m : Type u → Type u
inst✝ : Monad m
α β : Type u
f : β → α → β
x✝ y✝ : FreeMonoid α
⊢ op (↾flip (List.foldl f) (FreeMonoid.toList (x✝ * y✝))) =
    op (↾flip (List.foldl f) (FreeMonoid.toList x✝)) * op (↾flip (List.foldl f) (FreeMonoid.toList y✝))
Module: Mathlib.Control.Fold

Goal state before:
pp: m : Type u → Type u
inst✝¹ : Monad m
α β : Type u
inst✝ : LawfulMonad m
f : β → α → m β
⊢ ∀ (x y : FreeMonoid α),
    op (flip (List.foldlM f) (FreeMonoid.toList (x * y))) =
      op (flip (List.foldlM f) (FreeMonoid.toList x)) * op (flip (List.foldlM f) (FreeMonoid.toList y))

Tactic:
intros

Goal state after:
m : Type u → Type u
inst✝¹ : Monad m
α β : Type u
inst✝ : LawfulMonad m
f : β → α → m β
x✝ y✝ : FreeMonoid α
⊢ op (flip (List.foldlM f) (FreeMonoid.toList (x✝ * y✝))) =
    op (flip (List.foldlM f) (FreeMonoid.toList x✝)) * op (flip (List.foldlM f) (FreeMonoid.toList y✝))
Module: Mathlib.Control.Fold

Goal state before:
pp: m : Type u → Type u
inst✝¹ : Monad m
α β : Type u
inst✝ : LawfulMonad m
f : α → β → m β
⊢ ∀ (x y : FreeMonoid α),
    flip (List.foldrM f) (FreeMonoid.toList (x * y)) =
      flip (List.foldrM f) (FreeMonoid.toList x) * flip (List.foldrM f) (FreeMonoid.toList y)

Tactic:
intros

Goal state after:
m : Type u → Type u
inst✝¹ : Monad m
α β : Type u
inst✝ : LawfulMonad m
f : α → β → m β
x✝ y✝ : FreeMonoid α
⊢ flip (List.foldrM f) (FreeMonoid.toList (x✝ * y✝)) =
    flip (List.foldrM f) (FreeMonoid.toList x✝) * flip (List.foldrM f) (FreeMonoid.toList y✝)
Module: Mathlib.Control.Fold

Goal state before:
pp: α β γ : Type u
inst✝¹ : Monoid α
inst✝ : Monoid β
f : α →* β
⊢ ∀ {α_1 : Type ?u.17} (x : α_1), f (pure x) = pure x

Tactic:
intros

Goal state after:
α β γ : Type u
inst✝¹ : Monoid α
inst✝ : Monoid β
f : α →* β
α✝ : Type ?u.17
x✝ : α✝
⊢ f (pure x✝) = pure x✝
Module: Mathlib.Control.Fold

Goal state before:
pp: α β γ : Type u
inst✝¹ : Monoid α
inst✝ : Monoid β
f : α →* β
⊢ ∀ {α_1 β_1 : Type ?u.17} (x : Const α (α_1 → β_1)) (y : Const α α_1), f (x <*> y) = f x <*> f y

Tactic:
intros

Goal state after:
α β γ : Type u
inst✝¹ : Monoid α
inst✝ : Monoid β
f : α →* β
α✝ β✝ : Type ?u.17
x✝ : Const α (α✝ → β✝)
y✝ : Const α α✝
⊢ f (x✝ <*> y✝) = f x✝ <*> f y✝
Module: Mathlib.Control.Functor.Multivariate

Goal state before:
pp: case h₁
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec.{u} n
β : Type u
P : β → Prop
x : F (α ::: β)
⊢ ∀ (u : F fun i ↦ { p_1 // ofRepeat (α.PredLast' P i p_1) }),
    (fun i ↦ Subtype.val) <$$> u = x ↔ (fun i ↦ Subtype.val) <$$> f P n α <$$> u = x

Tactic:
intros

Goal state after:
case h₁
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec.{u} n
β : Type u
P : β → Prop
x : F (α ::: β)
u✝ : F fun i ↦ { p_1 // ofRepeat (α.PredLast' P i p_1) }
⊢ (fun i ↦ Subtype.val) <$$> u✝ = x ↔ (fun i ↦ Subtype.val) <$$> f P n α <$$> u✝ = x
Module: Mathlib.Control.Functor.Multivariate

Goal state before:
pp: case h₁
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec.{u} n
β : Type u
rr : β → β → Prop
x y : F (α ::: β)
⊢ ∀ (u : F fun i ↦ { p_1 // ofRepeat (α.RelLast' rr i (prod.mk i p_1.1 p_1.2)) }),
    (fun i t ↦ (↑t).1) <$$> u = x ∧ (fun i t ↦ (↑t).2) <$$> u = y ↔
      (fun i t ↦ (↑t).1) <$$> f' rr n α <$$> u = x ∧ (fun i t ↦ (↑t).2) <$$> f' rr n α <$$> u = y

Tactic:
intros

Goal state after:
case h₁
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec.{u} n
β : Type u
rr : β → β → Prop
x y : F (α ::: β)
u✝ : F fun i ↦ { p_1 // ofRepeat (α.RelLast' rr i (prod.mk i p_1.1 p_1.2)) }
⊢ (fun i t ↦ (↑t).1) <$$> u✝ = x ∧ (fun i t ↦ (↑t).2) <$$> u✝ = y ↔
    (fun i t ↦ (↑t).1) <$$> f' rr n α <$$> u✝ = x ∧ (fun i t ↦ (↑t).2) <$$> f' rr n α <$$> u✝ = y
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 α), id <$> x = x

Tactic:
intros

Goal state after:
r : Type u
m : Type u → Type v
α β : Type w
α✝ : Type u_1
x✝ : ContT r m α✝
⊢ id <$> x✝ = 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:
intros

Goal state after:
r : Type u
m : Type u → Type v
α β : Type w
α✝ β✝ : Type u_1
x✝ : α✝
f✝ : α✝ → ContT r m β✝
⊢ pure x✝ >>= f✝ = f✝ x✝
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:
intros

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 γ✝
⊢ x✝ >>= f✝ >>= g✝ = x✝ >>= fun x ↦ f✝ x >>= g✝
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:
intros

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 ω✝
⊢ (callCC fun f ↦ cmd✝ >>= next✝ f) = do
    let x ← cmd✝
    callCC fun f ↦ next✝ f x
Module: Mathlib.Control.Monad.Cont

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

Tactic:
intros

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 α✝
⊢ (callCC fun f ↦ goto f x✝ >>= dead✝ f) = pure x✝
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:
intros

Goal state after:
r : Type u
m : Type u → Type v
α β : Type w
α✝ β✝ : Type u_1
dummy✝ : ContT r m α✝
⊢ (callCC fun x ↦ dummy✝) = dummy✝
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 ω),
    (callCC fun f ↦ cmd >>= next f) = do
      let x ← cmd
      callCC fun f ↦ next f x

Tactic:
intros

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 ω✝
⊢ (callCC fun f ↦ cmd✝ >>= next✝ f) = do
    let x ← cmd✝
    callCC fun f ↦ next✝ f x
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} (β : Type u) (x : α) (dead : Label α (ExceptT ε m) β → β → ExceptT ε m α),
    (callCC fun f ↦ goto f x >>= dead f) = pure x

Tactic:
intros

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 α✝
⊢ (callCC fun f ↦ goto f x✝ >>= dead✝ f) = pure x✝
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 α), (callCC fun x ↦ dummy) = dummy

Tactic:
intros

Goal state after:
m : Type u → Type v
inst✝² : Monad m
ε : Type u
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ β✝ : Type u
dummy✝ : ExceptT ε m α✝
⊢ (callCC fun x ↦ dummy✝) = dummy✝
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} (β : Type u) (x : α) (dead : Label α (OptionT m) β → β → OptionT m α),
    (callCC fun f ↦ goto f x >>= dead f) = pure x

Tactic:
intros

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) = pure x✝
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:
intros

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✝) = dummy✝
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 ω),
    (callCC fun f ↦ cmd >>= next f) = do
      let x ← cmd
      callCC fun f ↦ next f x

Tactic:
intros

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 ω✝
⊢ (callCC fun f ↦ cmd✝ >>= next✝ f) = do
    let x ← cmd✝
    callCC fun f ↦ next✝ f x
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} (β : Type u) (x : α) (dead : Label α (StateT σ m) β → β → StateT σ m α),
    (callCC fun f ↦ goto f x >>= dead f) = pure x

Tactic:
intros

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 α✝
⊢ (callCC fun f ↦ goto f x✝ >>= dead✝ f) = pure x✝
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 α), (callCC fun x ↦ dummy) = dummy

Tactic:
intros

Goal state after:
m : Type u → Type v
σ : Type u
inst✝² : Monad m
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ β✝ : Type u
dummy✝ : StateT σ m α✝
⊢ (callCC fun x ↦ dummy✝) = dummy✝
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 ω),
    (callCC fun f ↦ cmd >>= next f) = do
      let x ← cmd
      callCC fun f ↦ next f x

Tactic:
intros

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 ω✝
⊢ (callCC fun f ↦ cmd✝ >>= next✝ f) = do
    let x ← cmd✝
    callCC fun f ↦ next✝ f x
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} (β : Type u) (x : α) (dead : Label α (ReaderT ρ m) β → β → ReaderT ρ m α),
    (callCC fun f ↦ goto f x >>= dead f) = pure x

Tactic:
intros

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 α✝
⊢ (callCC fun f ↦ goto f x✝ >>= dead✝ f) = pure x✝
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 α), (callCC fun x ↦ dummy) = dummy

Tactic:
intros

Goal state after:
m : Type u → Type v
ρ : Type u
inst✝² : Monad m
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ β✝ : Type u
dummy✝ : ReaderT ρ m α✝
⊢ (callCC fun x ↦ dummy✝) = dummy✝
Module: Mathlib.Data.TypeVec

Goal state before:
pp: ⊢ ∀ {n : ℕ} {α β : TypeVec.{u} n}, (id ⊗' id) = id

Tactic:
intros

Goal state after:
n✝ : ℕ
α✝ β✝ : TypeVec.{u} n✝
⊢ (id ⊗' id) = id
Module: Mathlib.Data.Analysis.Filter

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
τ : Type u_4
f g : Filter α
F : f.Realizer
G : g.Realizer
x✝ : Set α
⊢ x✝ ∈
      {
            f := fun x ↦
              match x with
              | (s, t) => F.F.f s ∪ G.F.f t,
            pt := (F.F.pt, G.F.pt),
            inf := fun x x_1 ↦
              match x with
              | (a, a') =>
                match x_1 with
                | (b, b') => (F.F.inf a b, G.F.inf a' b'),
            inf_le_left := ⋯, inf_le_right := ⋯ }.toFilter.sets ↔
    x✝ ∈ (f ⊔ g).sets

Tactic:
cases F; cases G; subst f g; simp [CFilter.toFilter]

Goal state after:
Module: Mathlib.Data.Erased

Goal state before:
pp: ⊢ ∀ {α β : Type u_1}, Functor.mapConst = Functor.map ∘ Function.const β

Tactic:
intros

Goal state after:
α✝ β✝ : Type u_1
⊢ Functor.mapConst = Functor.map ∘ Function.const β✝
Module: Mathlib.Data.Erased

Goal state before:
pp: ⊢ ∀ {α : Type u_1} (x : Erased α), id <$> x = x

Tactic:
intros

Goal state after:
α✝ : Type u_1
x✝ : Erased α✝
⊢ id <$> x✝ = x✝
Module: Mathlib.Data.Erased

Goal state before:
pp: ⊢ ∀ {α β : Type u_1} (x : Erased α) (y : Erased β), x <* y = Function.const β <$> x <*> y

Tactic:
intros

Goal state after:
α✝ β✝ : Type u_1
x✝ : Erased α✝
y✝ : Erased β✝
⊢ x✝ <* y✝ = Function.const β✝ <$> x✝ <*> y✝
Module: Mathlib.Data.Erased

Goal state before:
pp: ⊢ ∀ {α β : Type u_1} (x : Erased α) (y : Erased β), x *> y = Function.const α id <$> x <*> y

Tactic:
intros

Goal state after:
α✝ β✝ : Type u_1
x✝ : Erased α✝
y✝ : Erased β✝
⊢ x✝ *> y✝ = Function.const α✝ id <$> x✝ <*> y✝
Module: Mathlib.Data.Erased

Goal state before:
pp: ⊢ ∀ {α β : Type u_1} (g : α → β) (x : Erased α), pure g <*> x = g <$> x

Tactic:
intros

Goal state after:
α✝ β✝ : Type u_1
g✝ : α✝ → β✝
x✝ : Erased α✝
⊢ pure g✝ <*> x✝ = g✝ <$> x✝
Module: Mathlib.Data.Erased

Goal state before:
pp: ⊢ ∀ {α β : Type u_1} (f : α → β) (x : Erased α),
    (do
        let a ← x
        pure (f a)) =
      f <$> x

Tactic:
intros

Goal state after:
α✝ β✝ : Type u_1
f✝ : α✝ → β✝
x✝ : Erased α✝
⊢ (do
      let a ← x✝
      pure (f✝ a)) =
    f✝ <$> x✝
Module: Mathlib.Data.Erased

Goal state before:
pp: ⊢ ∀ {α β : Type u_1} (f : Erased (α → β)) (x : Erased α),
    (do
        let x_1 ← f
        x_1 <$> x) =
      f <*> x

Tactic:
intros

Goal state after:
α✝ β✝ : Type u_1
f✝ : Erased (α✝ → β✝)
x✝ : Erased α✝
⊢ (do
      let x ← f✝
      x <$> x✝) =
    f✝ <*> x✝
Module: Mathlib.Data.Erased

Goal state before:
pp: ⊢ ∀ {α β : Type u_1} (x : α) (f : α → Erased β), pure x >>= f = f x

Tactic:
intros

Goal state after:
α✝ β✝ : Type u_1
x✝ : α✝
f✝ : α✝ → Erased β✝
⊢ pure x✝ >>= f✝ = f✝ x✝
Module: Mathlib.Data.Erased

Goal state before:
pp: ⊢ ∀ {α β γ : Type u_1} (x : Erased α) (f : α → Erased β) (g : β → Erased γ), x >>= f >>= g = x >>= fun x ↦ f x >>= g

Tactic:
intros

Goal state after:
α✝ β✝ γ✝ : Type u_1
x✝ : Erased α✝
f✝ : α✝ → Erased β✝
g✝ : β✝ → Erased γ✝
⊢ x✝ >>= f✝ >>= g✝ = x✝ >>= fun x ↦ f✝ x >>= g✝
Module: Mathlib.Data.FP.Basic

Goal state before:
pp: C : FloatCfg
n d : ℕ+
e₁ : ℤ := ↑(↑n).size - ↑(↑d).size - ↑prec
d₁ n₁ : ℕ
e₂ : ℤ := if n₁ < d₁ then e₁ - 1 else e₁
e₃ : ℤ := max e₂ emin
d₂ n₂ : ℕ
r : ℚ := mkRat (↑n₂) d₂
⊢ Float × Bool

Tactic:
let m := r.floor

Goal state after:
C : FloatCfg
n d : ℕ+
e₁ : ℤ := ↑(↑n).size - ↑(↑d).size - ↑prec
d₁ n₁ : ℕ
e₂ : ℤ := if n₁ < d₁ then e₁ - 1 else e₁
e₃ : ℤ := max e₂ emin
d₂ n₂ : ℕ
r : ℚ := mkRat (↑n₂) d₂
m : ℤ := r.floor
⊢ Float × Bool
Module: Mathlib.Data.Fin.Tuple.Take

Goal state before:
pp: case pos
n n' : ℕ
motive : Fin (n + n') → Sort u_2
m : ℕ
h : m ≤ n'
u : (i : Fin n) → motive (castAdd n' i)
v : (i : Fin n') → motive (natAdd n i)
i : Fin (n + m)
h' : ↑i < n
⊢ (if h_1 : ↑i < n then u ((castLE ⋯ i).castLT ⋯) else ⋯ ▸ v (subNat n (Fin.cast ⋯ (castLE ⋯ i)) ⋯)) =
    if h : ↑i < n then u (i.castLT ⋯) else ⋯ ▸ v (castLE h (subNat n (Fin.cast ⋯ i) ⋯))

Tactic:
simp only [h', ↓reduceDIte]
    congr

Goal state after:
Module: Mathlib.Data.FinEnum

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : FinEnum α
⊢ ∀ (x : α), x ∈ map equiv.symm.toEmbedding univ

Tactic:
intros

Goal state after:
α : Type u
β : α → Type v
inst✝ : FinEnum α
x✝ : α
⊢ x✝ ∈ map equiv.symm.toEmbedding univ
Module: Mathlib.Data.Finite.Perm

Goal state before:
pp: α : Type u_1
inst✝ : Finite α
h : ∀ (a b : Perm α), a * b = b * a
⊢ Nat.card α ≤ 2

Tactic:
rw [← not_lt, ← Set.ncard_univ, Set.two_lt_ncard_iff]

Goal state after:
α : Type u_1
inst✝ : Finite α
h : ∀ (a b : Perm α), a * b = b * a
⊢ ¬∃ a b c, a ∈ _root_.Set.univ ∧ b ∈ _root_.Set.univ ∧ c ∈ _root_.Set.univ ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c
Module: Mathlib.Data.List.AList

Goal state before:
pp: α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : s₁.Disjoint s₂
⊢ ∀ (x : α) (y : β x), y ∈ dlookup x (s₁ ∪ s₂).entries ↔ y ∈ dlookup x (s₂ ∪ s₁).entries

Tactic:
intros

Goal state after:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : s₁.Disjoint s₂
x✝ : α
y✝ : β x✝
⊢ y✝ ∈ dlookup x✝ (s₁ ∪ s₂).entries ↔ y✝ ∈ dlookup x✝ (s₂ ∪ s₁).entries
Module: Mathlib.Data.List.AList

Goal state before:
pp: case mp.inr
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : s₁.Disjoint s₂
x✝ : α
y✝ : β x✝
h' : ¬x✝ ∈ s₁.entries.keys ∧ dlookup x✝ s₂.entries = some y✝
⊢ dlookup x✝ s₂.entries = some y✝

Tactic:
h'.2

Goal state after:
case mp.inr
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ : AList β
h : s₁.Disjoint s₂
x✝ : α
y✝ : β x✝
h' : ¬x✝ ∈ s₁.entries.keys ∧ dlookup x✝ s₂.entries = some y✝
⊢ some y✝ = some y✝