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

Goal state before:
pp: α β : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
f : α → β
xs : t α
⊢ toList (f <$> xs) = f <$> toList xs

Tactic:
by

Goal state after:
Module: Mathlib.Control.Fold

Goal state before:
pp: α β γ : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
g : β → γ
f : α → γ → α
a : α
l : t β
⊢ foldl f a (g <$> l) = foldl (fun x y ↦ f x (g y)) a l

Tactic:
by

Goal state after:
Module: Mathlib.Control.Fold

Goal state before:
pp: α β γ : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
g : β → γ
f : γ → α → α
a : α
l : t β
⊢ foldr f a (g <$> l) = foldr (f ∘ g) a l

Tactic:
by

Goal state after:
Module: Mathlib.Control.Fold

Goal state before:
pp: α : Type u
xs : List α
⊢ toList xs = xs

Tactic:
by

Goal state after:
Module: Mathlib.Control.Fold

Goal state before:
pp: α : Type u
t : Type u → Type u
inst✝¹ : Traversable t
inst✝ : LawfulTraversable t
xs : t α
⊢ length xs = (toList xs).length

Tactic:
by

Goal state after:
Module: Mathlib.Control.Fold

Goal state before:
pp: α β : Type u
t : Type u → Type u
inst✝³ : Traversable t
inst✝² : LawfulTraversable t
m : Type u → Type u
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β → m α
x : α
xs : t β
⊢ foldlm f x xs = unop ((foldlM.ofFreeMonoid f) (FreeMonoid.ofList (toList xs))) x

Tactic:
by

Goal state after:
Module: Mathlib.Control.Fold

Goal state before:
pp: α β : Type u
t : Type u → Type u
inst✝³ : Traversable t
inst✝² : LawfulTraversable t
m : Type u → Type u
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β → m α
x : α
xs : t β
⊢ unop ((foldlM.ofFreeMonoid f) (FreeMonoid.ofList (toList xs))) x = List.foldlM f x (toList xs)

Tactic:
by

Goal state after:
Module: Mathlib.Control.Fold

Goal state before:
pp: α β : Type u
t : Type u → Type u
inst✝³ : Traversable t
inst✝² : LawfulTraversable t
m : Type u → Type u
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β → m β
x : β
xs : t α
⊢ foldrm f x xs = List.foldrM f x (toList xs)

Tactic:
by

Goal state after:
Module: Mathlib.Control.Fold

Goal state before:
pp: α β γ : Type u
t : Type u → Type u
inst✝³ : Traversable t
inst✝² : LawfulTraversable t
m : Type u → Type u
inst✝¹ : Monad m
inst✝ : LawfulMonad m
g : β → γ
f : α → γ → m α
a : α
l : t β
⊢ foldlm f a (g <$> l) = foldlm (fun x y ↦ f x (g y)) a l

Tactic:
by

Goal state after:
Module: Mathlib.Control.Fold

Goal state before:
pp: α β γ : Type u
t : Type u → Type u
inst✝³ : Traversable t
inst✝² : LawfulTraversable t
m : Type u → Type u
inst✝¹ : Monad m
inst✝ : LawfulMonad m
g : β → γ
f : γ → α → m α
a : α
l : t β
⊢ foldrm f a (g <$> l) = foldrm (f ∘ g) a l

Tactic:
by

Goal state after:
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:
by

Goal state after:
Module: Mathlib.Control.Functor.Multivariate

Goal state before:
pp: n : ℕ
α : TypeVec.{u} n
F : TypeVec.{u} n → Type v
inst✝¹ : MvFunctor F
P : α ⟹ TypeVec.repeat n Prop
inst✝ : LawfulMvFunctor F
x : F α
⊢ ∀ (u : F fun i ↦ Subtype ((fun i x ↦ ofRepeat (P i x)) i)),
    (fun i ↦ Subtype.val) <$$> u = x ↔ subtypeVal P <$$> toSubtype P <$$> u = x

Tactic:
by

Goal state after:
Module: Mathlib.Control.Functor.Multivariate

Goal state before:
pp: n : ℕ
α : TypeVec.{u} n
F : TypeVec.{u} n → Type v
inst✝¹ : MvFunctor F
R : α ⊗ α ⟹ TypeVec.repeat n Prop
inst✝ : LawfulMvFunctor F
x y : F α
⊢ ∀ (u : F fun i ↦ { p // (fun i x y ↦ ofRepeat (R i (prod.mk i x y))) i p.1 p.2 }),
    (fun i t ↦ (↑t).1) <$$> u = x ∧ (fun i t ↦ (↑t).2) <$$> u = y ↔
      (prod.fst ⊚ subtypeVal R) <$$> toSubtype' R <$$> u = x ∧ (prod.snd ⊚ subtypeVal R) <$$> toSubtype' R <$$> u = y

Tactic:
by

Goal state after:
Module: Mathlib.Control.Functor.Multivariate

Goal state before:
pp: n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α✝ : TypeVec.{u} n
β : Type u
pp : β → Prop
x✝ : ℕ
α : TypeVec.{u} x✝
i : Fin2 x✝
x : (fun i ↦ { p_1 // ofRepeat (α.PredLast' pp i p_1) }) i.fs
⊢ ofRepeat (α.PredLast' pp i.fs ↑x) = α.PredLast pp ↑x

Tactic:
by

Goal state after:
Module: Mathlib.Control.Functor.Multivariate

Goal state before:
pp: n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α✝ : TypeVec.{u} n
β : Type u
pp : β → Prop
x✝ : ℕ
α : TypeVec.{u} x✝
i : Fin2 x✝
x : (fun i ↦ { p_1 // α.PredLast pp p_1 }) i.fs
⊢ α.PredLast pp ↑x = ofRepeat (α.PredLast' pp i.fs ↑x)

Tactic:
by

Goal state after:
Module: Mathlib.Control.Functor.Multivariate

Goal state before:
pp: 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) }
this : (fun i ↦ Subtype.val) = fun i x ↦ ↑(f P n α i x)
⊢ (fun i ↦ Subtype.val) <$$> u✝ = x ↔ (fun i x ↦ ↑(f P n α i x)) <$$> u✝ = x

Tactic:
by

Goal state after:
Module: Mathlib.Control.Functor.Multivariate

Goal state before:
pp: n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec.{u} n
β : Type u
P : β → Prop
x : F (α ::: β)
⊢ LiftP' (α.PredLast' P) x ↔ LiftP (α.PredLast P) x

Tactic:
by

Goal state after:
Module: Mathlib.Control.Functor.Multivariate

Goal state before:
pp: n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α✝ : TypeVec.{u} n
β : Type u
pp : β → Prop
rr : β → β → Prop
x✝ : ℕ
α : TypeVec.{u} x✝
i : Fin2 x✝
x : (fun i ↦ { p_1 // ofRepeat (α.RelLast' rr i (prod.mk i p_1.1 p_1.2)) }) i.fs
⊢ ofRepeat (α.RelLast' rr i.fs (prod.mk i.fs (↑x).1 (↑x).2)) = α.RelLast rr (↑x).1 (↑x).2

Tactic:
by

Goal state after:
Module: Mathlib.Control.Functor.Multivariate

Goal state before:
pp: n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α✝ : TypeVec.{u} n
β : Type u
pp : β → Prop
rr : β → β → Prop
x✝ : ℕ
α : TypeVec.{u} x✝
i : Fin2 x✝
x : (fun i ↦ { p_1 // α.RelLast rr p_1.1 p_1.2 }) i.fs
⊢ α.RelLast rr (↑x).1 (↑x).2 = ofRepeat (α.RelLast' rr i.fs (prod.mk i.fs (↑x).1 (↑x).2))

Tactic:
by

Goal state after:
Module: Mathlib.Control.LawfulFix

Goal state before:
pp: α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
i : ℕ
⊢ approx (⇑f) i ≤ approx (⇑f) i.succ

Tactic:
by

Goal state after:
Module: Mathlib.Control.LawfulFix

Goal state before:
pp: α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
i j : ℕ
hij : i ≤ j
⊢ approx (⇑f) i ≤ approx (⇑f) j

Tactic:
by

Goal state after:
Module: Mathlib.Control.LawfulFix

Goal state before:
pp: 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
hh : b ∈ approx (⇑f) (Nat.find h₀).succ a
⊢ ∃ i, b ∈ approx (⇑f) i a

pp: 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
hh : ∃ i, b ∈ approx (⇑f) i a
⊢ b ∈ approx (⇑f) (Nat.find h₀).succ a

Tactic:
· exact ⟨_, hh⟩

Goal state after:
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
hh : ∃ i, b ∈ approx (⇑f) i a
⊢ b ∈ approx (⇑f) (Nat.find h₀).succ a
Module: Mathlib.Control.Functor.Multivariate

Goal state before:
pp: 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 (α ::: β)
⊢ LiftR' (α.RelLast' rr) x y ↔ LiftR (α.RelLast rr) x y

Tactic:
by

Goal state after:
Module: Mathlib.Control.LawfulFix

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

Tactic:
by

Goal state after:
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:
by

Goal state after:
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:
by

Goal state after:
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:
by

Goal state after:
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:
by

Goal state after:
Module: Mathlib.Data.TypeVec

Goal state before:
pp: n : ℕ
α : TypeVec.{u} n
β : TypeVec.{v} n
f g : α ⟹ β
⊢ (∀ (i : Fin2 n), f i = g i) → f = g

Tactic:
by

Goal state after:
Module: Mathlib.Data.TypeVec

Goal state before:
pp: n : ℕ
α : TypeVec.{u_1} (n + 1)
i : Fin2 (n + 1)
⊢ (α.drop ::: α.last) i = α i

Tactic:
by

Goal state after:
Module: Mathlib.Data.TypeVec

Goal state before:
pp: n : ℕ
C : TypeVec.{?u.15} (n + 1) → Sort u
H : (α : TypeVec.{?u.15} n) → (β : Type ?u.15) → C (α ::: β)
γ : TypeVec.{?u.15} (n + 1)
⊢ C γ

Tactic:
by

Goal state after:
Module: Mathlib.Data.TypeVec

Goal state before:
pp: n : ℕ
α : TypeVec.{?u.3} 0
β : TypeVec.{?u.6} 0
i : Fin2 0
⊢ α i → β i

Tactic:
by

Goal state after:
Module: Mathlib.Data.TypeVec

Goal state before:
pp: n : ℕ
α : TypeVec.{u_1} (n + 1)
β : TypeVec.{u_2} (n + 1)
f g : α ⟹ β
h₀ : dropFun f = dropFun g
h₁ : lastFun f = lastFun g
⊢ f = g

Tactic:
by

Goal state after:
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:
by

Goal state after:
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:
by

Goal state after:
Module: Mathlib.Data.TypeVec

Goal state before:
pp: n : ℕ
α : TypeVec.{u_1} (n + 1)
α' : TypeVec.{u_2} (n + 1)
f f' : α.drop ⟹ α'.drop
g g' : α.last → α'.last
H : splitFun f g = splitFun f' g'
⊢ f = f' ∧ g = g'

Tactic:
by

Goal state after:
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:
by

Goal state after:
Module: Mathlib.Data.TypeVec

Goal state before:
pp: n : ℕ
β : TypeVec.{?u.4} 0 → Sort u_1
f : β Fin2.elim0
v : TypeVec.{?u.4} 0
⊢ β Fin2.elim0 = β v

Tactic:
by

Goal state after:
Module: Mathlib.Data.TypeVec

Goal state before:
pp: n✝ n : ℕ
β : TypeVec.{?u.30} (n + 1) → Sort u_1
f : (t : Type ?u.30) → (v : TypeVec.{?u.30} n) → β (v ::: t)
v : TypeVec.{?u.30} (n + 1)
⊢ β (v.drop ::: v.last) = β v

Tactic:
by

Goal state after:
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:
by

Goal state after:
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:
by

Goal state after:
Module: Mathlib.Data.TypeVec

Goal state before:
pp: n : ℕ
β : (v : TypeVec.{?u.4} 0) → (v' : TypeVec.{?u.7} 0) → v ⟹ v' → Sort u_1
f : β Fin2.elim0 Fin2.elim0 nilFun
v : TypeVec.{?u.4} 0
v' : TypeVec.{?u.7} 0
fs : v ⟹ v'
⊢ v = Fin2.elim0

Tactic:
by

Goal state after:
Module: Mathlib.Data.TypeVec

Goal state before:
pp: n : ℕ
β : (v : TypeVec.{?u.4} 0) → (v' : TypeVec.{?u.7} 0) → v ⟹ v' → Sort u_1
f : β Fin2.elim0 Fin2.elim0 nilFun
v : TypeVec.{?u.4} 0
v' : TypeVec.{?u.7} 0
fs : v ⟹ v'
eq₁ : v = Fin2.elim0
⊢ v' = Fin2.elim0

Tactic:
by

Goal state after:
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:
by

Goal state after:
Module: Mathlib.Data.TypeVec

Goal state before:
pp: n : ℕ
β : (v : TypeVec.{?u.4} 0) → (v' : TypeVec.{?u.7} 0) → v ⟹ v' → Sort u_1
f : β Fin2.elim0 Fin2.elim0 nilFun
v : TypeVec.{?u.4} 0
v' : TypeVec.{?u.7} 0
fs : v ⟹ v'
eq₁ : v = Fin2.elim0
eq₂ : v' = Fin2.elim0
⊢ fs = nilFun

Tactic:
by

Goal state after:
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:
by

Goal state after:
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:
by

Goal state after:
Module: Mathlib.Data.TypeVec

Goal state before:
pp: n : ℕ
β : (v : TypeVec.{?u.4} 0) → (v' : TypeVec.{?u.7} 0) → v ⟹ v' → Sort u_1
f : β Fin2.elim0 Fin2.elim0 nilFun
v : TypeVec.{?u.4} 0
v' : TypeVec.{?u.7} 0
fs : v ⟹ v'
⊢ β v v' fs

Tactic:
by

Goal state after:
Module: Mathlib.Control.Monad.Cont

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

Tactic:
by

Goal state after:
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:
by

Goal state after:
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:
by

Goal state after:
Module: Mathlib.Data.TypeVec

Goal state before:
pp: n✝ n : ℕ
β : (v : TypeVec.{?u.30} (n + 1)) → (v' : TypeVec.{?u.32} (n + 1)) → v ⟹ v' → Sort u_1
F :
  (t : Type ?u.30) →
    (t' : Type ?u.32) →
      (f : t → t') →
        (v : TypeVec.{?u.30} n) → (v' : TypeVec.{?u.32} n) → (fs : v ⟹ v') → β (v ::: t) (v' ::: t') (fs ::: f)
⊢ (v : TypeVec.{?u.30} (n + 1)) → (v' : TypeVec.{?u.32} (n + 1)) → (fs : v ⟹ v') → β v v' fs

Tactic:
by

Goal state after:
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:
by

Goal state after:
Module: Mathlib.Data.TypeVec

Goal state before:
pp: n : ℕ
β : Fin2.elim0 ⟹ Fin2.elim0 → Sort u_1
f : β nilFun
g : Fin2.elim0 ⟹ Fin2.elim0
this : g = nilFun
⊢ β g

Tactic:
by

Goal state after:
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✝¹ : OptionT m α✝
x✝ : Label ω✝ (OptionT m) γ✝ → α✝ → OptionT m ω✝
⊢ (callCC fun f ↦ none.elim (pure none) fun x ↦ (x✝ (OptionT.mkLabel f) x).run) =
    none.elim (pure none) fun x ↦ callCC fun x_1 ↦ (x✝ (OptionT.mkLabel x_1) x).run

Tactic:
by

Goal state after:
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} (cmd : OptionT m α) (next : Label ω (OptionT m) γ → α → OptionT m ω),
    (callCC fun f ↦ cmd >>= next f) = do
      let x ← cmd
      callCC fun f ↦ next f x

Tactic:
by

Goal state after:
Module: Mathlib.Data.TypeVec

Goal state before:
pp: n : ℕ
β : Fin2.elim0 ⟹ Fin2.elim0 → Sort u_1
f : β nilFun
⊢ (f : Fin2.elim0 ⟹ Fin2.elim0) → β f

Tactic:
by

Goal state after:
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:
by

Goal state after:
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:
by

Goal state after:
Module: Mathlib.Condensed.Light.Sequence

Goal state before:
pp: R : Type
inst✝ : CommRing R
X Y : LightProfinite
y : ↑Y.toTop
f : X ⟶ Y
⊢ Continuous ⇑(ConcreteCategory.hom f)

Tactic:
by

Goal state after:
Module: Mathlib.Data.TypeVec

Goal state before:
pp: n✝ n : ℕ
t : Type u_1
t' : Type u_2
v : TypeVec.{u_1} n
v' : TypeVec.{u_2} n
β : v ::: t ⟹ v' ::: t' → Sort u_3
F : (f : t → t') → (fs : v ⟹ v') → β (fs ::: f)
⊢ (fs : v ::: t ⟹ v' ::: t') → β fs

Tactic:
by

Goal state after:
Module: Mathlib.Condensed.Light.Sequence

Goal state before:
pp: S : Type u_1
T : Type u_2
X : Type u_3
π : T → S × Option X
σ : Option X → S → T
t : T
⊢ t ∈ fibres π σ ↔ (π t).2 = none ∨ ∃ x s, σ (Option.some x) s = t

Tactic:
by

Goal state after:
Module: Mathlib.Control.Monad.Cont

Goal state before:
pp: m : Type u → Type v
inst✝¹ : Monad m
α : Type u_1
β ω : Type u
inst✝ : EmptyCollection ω
x : Label (α × ω) m β
i : α
⊢ goto (mkLabel x) i = monadLift (goto x (i, ∅))

Tactic:
by

Goal state after:
Module: Mathlib.Control.Monad.Cont

Goal state before:
pp: m : Type u → Type v
inst✝¹ : Monad m
α : Type u_1
β ω : Type u
inst✝ : Monoid ω
x : Label (α × ω) m β
i : α
⊢ goto (mkLabel' x) i = monadLift (goto x (i, 1))

Tactic:
by

Goal state after:
Module: Mathlib.Control.Monad.Cont

Goal state before:
pp: m : Type u → Type v
α β σ : Type u
x : Label (α × σ) m (β × σ)
i : α
⊢ goto (mkLabel x) i = mk fun s ↦ goto x (i, s)

Tactic:
by

Goal state after:
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:
by

Goal state after:
Module: Mathlib.Data.TypeVec

Goal state before:
pp: β : Type u_1
γ : Type u_2
x : γ
n : ℕ
α : TypeVec.{u_1} n
⊢ TypeVec.const x (α ::: β) = (TypeVec.const x α ::: fun x_1 ↦ x)

Tactic:
by

Goal state after:
Module: Mathlib.Data.TypeVec

Goal state before:
pp: α : TypeVec.{u_1} 0
β : TypeVec.{u_2} 0
f : α ⟹ β
⊢ f = nilFun

Tactic:
by

Goal state after:
Module: Mathlib.Data.TypeVec

Goal state before:
pp: α : TypeVec.{u_1} 0
⊢ id = nilFun

Tactic:
by

Goal state after:
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:
by

Goal state after:
Module: Mathlib.Data.TypeVec

Goal state before:
pp: β : Type u_1
x : β
α : TypeVec.{u_2} 0
⊢ TypeVec.const x α = nilFun

Tactic:
by

Goal state after:
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:
by

Goal state after:
Module: Mathlib.Control.Monad.Cont

Goal state before:
pp: m : Type u → Type v
α : Type u_1
ρ β : Type u
x : Label α m β
i : α
⊢ goto (mkLabel ρ x) i = monadLift (goto x i)

Tactic:
by

Goal state after:
Module: Mathlib.Data.TypeVec

Goal state before:
pp: β : Type u_1
n : ℕ
α : TypeVec.{u_1} n
⊢ (α ::: β).repeatEq = splitFun α.repeatEq (uncurry Eq)

Tactic:
by

Goal state after:
Module: Mathlib.Control.LawfulFix

Goal state before:
pp: α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
a : α
b : β a
⊢ b ∈ Part.fix (⇑f) a ↔ ∃ i, b ∈ approx (⇑f) i a

Tactic:
by

Goal state after:
Module: Mathlib.Data.TypeVec

Goal state before:
pp: α : TypeVec.{u_1} 0
⊢ α.repeatEq = nilFun

Tactic:
by

Goal state after:
Module: Mathlib.Control.LawfulFix

Goal state before:
pp: α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
i : ℕ
a : α
b : β a
hh : b ∈ approx (⇑f) i a
⊢ b ∈ Part.fix (⇑f) a

Tactic:
by

Goal state after:
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:
by

Goal state after:
Module: Mathlib.Condensed.Light.Sequence

Goal state before:
pp: S : Type u_1
T : Type u_2
X : Type u_3
π : T → S × Option X
σ : Option X → S → T
hσ' : ∀ (x : Option X) (s : S), (π (σ x s)).2 = x
x : T
x✝ : ∃ i, (∀ (x_1 : S), ¬σ (Option.some i) x_1 = x) ∧ (π x).2 = ↑i
n : X
hn : ∀ (x_1 : S), ¬σ (Option.some n) x_1 = x
hn' : (π x).2 = ↑n
⊢ ¬(π x).2 = none

Tactic:
by

Goal state after:
Module: Mathlib.Data.TypeVec

Goal state before:
pp: n : ℕ
α : TypeVec.{u_1} n
i : Fin2 n
x : α i
p : Prop
⊢ ofRepeat (TypeVec.const p α i x) ↔ p

Tactic:
by

Goal state after:
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:
by

Goal state after:
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:
by

Goal state after:
Module: Mathlib.Data.TypeVec

Goal state before:
pp: n : ℕ
α β : TypeVec.{u_1} n
i : Fin2 n
a : α i
b : β i
⊢ prod.fst i (prod.mk i a b) = a

Tactic:
by

Goal state after:
Module: Mathlib.Control.Monad.Cont

Goal state before:
pp: m : Type u → Type v
m₁ : Type u₀ → Type v₀
m₂ : Type u₁ → Type v₁
α₁ r₁ : Type u₀
α₂ r₂ : Type u₁
F : m₁ r₁ ≃ m₂ r₂
G : α₁ ≃ α₂
f : ContT r₁ m₁ α₁
⊢ (fun f r ↦ F.symm (f fun x ↦ F (r (G.symm x)))) ((fun f r ↦ F (f fun x ↦ F.symm (r (G x)))) f) = f

Tactic:
by

Goal state after:
Module: Mathlib.Data.TypeVec

Goal state before:
pp: n : ℕ
α β : TypeVec.{u_1} n
i : Fin2 n
a : α i
b : β i
⊢ prod.snd i (prod.mk i a b) = b

Tactic:
by

Goal state after:
Module: Mathlib.Control.Monad.Cont

Goal state before:
pp: m : Type u → Type v
m₁ : Type u₀ → Type v₀
m₂ : Type u₁ → Type v₁
α₁ r₁ : Type u₀
α₂ r₂ : Type u₁
F : m₁ r₁ ≃ m₂ r₂
G : α₁ ≃ α₂
f : ContT r₂ m₂ α₂
⊢ (fun f r ↦ F (f fun x ↦ F.symm (r (G x)))) ((fun f r ↦ F.symm (f fun x ↦ F (r (G.symm x)))) f) = f

Tactic:
by

Goal state after:
Module: Mathlib.Control.LawfulFix

Goal state before:
pp: α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
x : α
⊢ ∃ i, Part.fix (⇑f) x ≤ approx (⇑f) i x

Tactic:
by

Goal state after:
Module: Mathlib.Control.LawfulFix

Goal state before:
pp: α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
x : (a : α) → Part (β a)
⊢ x ∈ approxChain f → x ≤ f x

Tactic:
by

Goal state after:
Module: Mathlib.Data.TypeVec

Goal state before:
pp: n : ℕ
α α' β β' : TypeVec.{u_1} n
f : α ⟹ β
g : α' ⟹ β'
⊢ prod.fst ⊚ (f ⊗' g) = f ⊚ prod.fst

Tactic:
by

Goal state after: