mathlib-initiative/mathlib-tactics huggingface dataset:
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✝).run = (x✝² >>= fun x ↦ x✝¹ x >>= x✝).run

Tactic:
;

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)).run =
    (x✝¹ <$> x✝).run

Tactic:
;

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.LawfulFix

Goal state before:
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
y : β a
i : ℕ
hh : b ∈ approx (⇑f) i a
⊢ y ∈ approx (⇑f) (Nat.find h₀).succ a → y = b

Tactic:
;

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
y : β a
i : ℕ
hh : b ∈ approx (⇑f) i a
⊢ y ∈ approx (⇑f) (Nat.find h₀).succ a → y = b
Module: Mathlib.Control.LawfulFix

Goal state before:
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
y : β a
i : ℕ
hh : b ∈ approx (⇑f) i a
j : ℕ
⊢ y ∈ approx (⇑f) j a → y = b

Tactic:
;

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
y : β a
i : ℕ
hh : b ∈ approx (⇑f) i a
j : ℕ
⊢ y ∈ approx (⇑f) j a → y = b
Module: Mathlib.Data.TypeVec

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

Tactic:
;

Goal state after:
n : ℕ
α : TypeVec.{u} n
β : TypeVec.{v} n
f g : α ⟹ β
h : ∀ (i : Fin2 n), f i = g i
⊢ f = g
Module: Mathlib.Data.TypeVec

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

Tactic:
;

Goal state after:
n : ℕ
α : TypeVec.{u} n
β : TypeVec.{v} n
f g : α ⟹ β
h : ∀ (i : Fin2 n), f i = g i
i : Fin2 n
⊢ f i = g i
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 (γ.drop ::: γ.last)

Tactic:
;

Goal state after:
n : ℕ
C : TypeVec.{?u.15} (n + 1) → Sort u
H : (α : TypeVec.{?u.15} n) → (β : Type ?u.15) → C (α ::: β)
γ : TypeVec.{?u.15} (n + 1)
⊢ C (γ.drop ::: γ.last)
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:
;

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 = y
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✝ : α → m r
⊢ x x✝ = y x✝

Tactic:
;

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.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'
⊢ dropFun (splitFun f' g') = f' ∧ lastFun (splitFun f' g') = g'

Tactic:
;

Goal state after:
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'
⊢ dropFun (splitFun f' g') = f' ∧ lastFun (splitFun f' g') = g'
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:
;

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:
;

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✝ : α✝
f✝¹ : α✝ → ContT r m β✝
f✝ : β✝ → m r
⊢ (pure x✝ >>= f✝¹).run f✝ = (f✝¹ x✝).run f✝

Tactic:
;

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.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:
;

Goal state after:
n : ℕ
β : TypeVec.{?u.4} 0 → Sort u_1
f : β Fin2.elim0
v : TypeVec.{?u.4} 0
⊢ Fin2.elim0 = v
Module: Mathlib.Data.TypeVec

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

Tactic:
;

Goal state after:
n : ℕ
β : TypeVec.{?u.4} 0 → Sort u_1
f : β Fin2.elim0
v : TypeVec.{?u.4} 0
i : Fin2 0
⊢ i.elim0 = v i
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:
;

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
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✝

Tactic:
;

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
α β : 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:
;

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.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'
i : Fin2 0
⊢ v i = i.elim0

Tactic:
;

Goal state after:
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'
i : Fin2 0
⊢ v i = i.elim0
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 ω✝
f✝ : ω✝ → m r
⊢ (callCC fun f ↦ cmd✝ >>= next✝ f).run f✝ =
    (do
          let x ← cmd✝
          callCC fun f ↦ next✝ f x).run
      f✝

Tactic:
;

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.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
i : Fin2 0
⊢ v' i = i.elim0

Tactic:
;

Goal state after:
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
i : Fin2 0
⊢ v' i = i.elim0
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:
;

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.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
i : Fin2 0
⊢ fs i = nilFun i

Tactic:
;

Goal state after:
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
i : Fin2 0
⊢ fs i = nilFun i
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 α✝
f✝ : α✝ → m r
⊢ (callCC fun f ↦ goto f x✝ >>= dead✝ f).run f✝ = (pure x✝).run f✝

Tactic:
;

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.Data.TypeVec

Goal state before:
pp: case refl
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.7} 0
eq₂ : v' = Fin2.elim0
fs : Fin2.elim0 ⟹ v'
eq₃ : fs = nilFun
⊢ β Fin2.elim0 Fin2.elim0 nilFun = β Fin2.elim0 v' fs

Tactic:
;

Goal state after:
case refl
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.7} 0
eq₂ : v' = Fin2.elim0
fs : Fin2.elim0 ⟹ v'
eq₃ : fs = nilFun
⊢ β Fin2.elim0 Fin2.elim0 nilFun = β Fin2.elim0 v' fs
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:
;

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: 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✝

Tactic:
;

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.Data.TypeVec

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

Tactic:
;

Goal state after:
case refl.refl
n : ℕ
β : (v : TypeVec.{?u.4} 0) → (v' : TypeVec.{?u.7} 0) → v ⟹ v' → Sort u_1
f : β Fin2.elim0 Fin2.elim0 nilFun
fs : Fin2.elim0 ⟹ Fin2.elim0
eq₃ : fs = nilFun
⊢ β Fin2.elim0 Fin2.elim0 nilFun = β Fin2.elim0 Fin2.elim0 fs
Module: Mathlib.Data.TypeVec

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

Tactic:
;

Goal state after:
case refl.refl.refl
n : ℕ
β : (v : TypeVec.{?u.4} 0) → (v' : TypeVec.{?u.7} 0) → v ⟹ v' → Sort u_1
f : β Fin2.elim0 Fin2.elim0 nilFun
⊢ β Fin2.elim0 Fin2.elim0 nilFun = β Fin2.elim0 Fin2.elim0 nilFun
Module: Mathlib.Control.Monad.Cont

Goal state before:
pp: case mk
m : Type u → Type v
inst✝ : Monad m
α β ε : Type u
i : α
apply✝ : Except ε α → m β
⊢ goto (mkLabel { apply := apply✝ }) i = mk (Except.ok <$> goto { apply := apply✝ } (Except.ok i))

Tactic:
;

Goal state after:
case mk
m : Type u → Type v
inst✝ : Monad m
α β ε : Type u
i : α
apply✝ : Except ε α → m β
⊢ goto (mkLabel { apply := apply✝ }) i = mk (Except.ok <$> goto { apply := apply✝ } (Except.ok i))
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:
;

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
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:
;

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)) =
    do
    let x ← cmd✝
    ExceptT.mk (callCC fun x_1 ↦ (next✝ (ExceptT.mkLabel x_1) 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
x✝ : α✝
dead✝ : Label α✝ (ExceptT ε m) β✝ → β✝ → ExceptT ε m α✝
⊢ (ExceptT.mk (pure (Except.ok x✝))).run = (pure x✝).run

Tactic:
;

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 α✝
⊢ (callCC fun x ↦ dummy✝) = dummy✝

Tactic:
;

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
ε : Type u
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ β✝ : Type u
dummy✝ : ExceptT ε m α✝
⊢ ExceptT.mk dummy✝.run = dummy✝

Tactic:
;

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 = 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
dummy✝ : ExceptT ε m α✝
⊢ (ExceptT.mk dummy✝.run).run = dummy✝.run

Tactic:
;

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
dummy✝ : OptionT m α✝
⊢ (callCC fun x ↦ dummy✝) = dummy✝

Tactic:
;

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
inst✝² : Monad m
inst✝¹ : MonadCont m
inst✝ : LawfulMonadCont m
α✝ β✝ : Type u
dummy✝ : OptionT m α✝
⊢ (callCC fun x ↦ dummy✝).run = dummy✝.run

Tactic:
;

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: case mk
m : Type u → Type v
inst✝¹ : Monad m
α : Type u_1
β ω : Type u
inst✝ : EmptyCollection ω
i : α
apply✝ : α × ω → m β
⊢ goto (mkLabel { apply := apply✝ }) i = monadLift (goto { apply := apply✝ } (i, ∅))

Tactic:
;

Goal state after:
case mk
m : Type u → Type v
inst✝¹ : Monad m
α : Type u_1
β ω : Type u
inst✝ : EmptyCollection ω
i : α
apply✝ : α × ω → m β
⊢ goto (mkLabel { apply := apply✝ }) i = monadLift (goto { apply := apply✝ } (i, ∅))
Module: Mathlib.Control.Monad.Cont

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

Tactic:
;

Goal state after:
case mk
m : Type u → Type v
inst✝¹ : Monad m
α : Type u_1
β ω : Type u
inst✝ : Monoid ω
i : α
apply✝ : α × ω → m β
⊢ goto (mkLabel' { apply := apply✝ }) i = monadLift (goto { apply := apply✝ } (i, 1))
Module: Mathlib.Data.TypeVec

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

Tactic:
;

Goal state after:
β : Type u_1
γ : Type u_2
x : γ
n : ℕ
α : TypeVec.{u_1} n
i : Fin2 (n + 1)
⊢ TypeVec.const x (α ::: β) i = (TypeVec.const x α ::: fun x_1 ↦ x) i
Module: Mathlib.Control.Monad.Cont

Goal state before:
pp: case mk
m : Type u → Type v
α β σ : Type u
i : α
apply✝ : α × σ → m (β × σ)
⊢ goto (mkLabel { apply := apply✝ }) i = mk fun s ↦ goto { apply := apply✝ } (i, s)

Tactic:
;

Goal state after:
case mk
m : Type u → Type v
α β σ : Type u
i : α
apply✝ : α × σ → m (β × σ)
⊢ goto (mkLabel { apply := apply✝ }) i = mk fun s ↦ goto { apply := apply✝ } (i, 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✝ : 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:
;

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 ω✝
⊢ (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
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 ω✝
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✝

Tactic:
;

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:
;

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 α✝
⊢ (StateT.mk fun r ↦ pure (x✝, r)) = pure x✝
Module: Mathlib.Data.TypeVec

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

Tactic:
;

Goal state after:
α : TypeVec.{u_1} 0
β : TypeVec.{u_2} 0
f : α ⟹ β
x : Fin2 0
x✝ : α x
⊢ f x x✝ = nilFun x 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
x✝ : α✝
dead✝ : Label α✝ (StateT σ m) β✝ → β✝ → StateT σ m α✝
s✝ : σ
⊢ (StateT.mk fun r ↦ pure (x✝, r)).run s✝ = (pure x✝).run s✝

Tactic:
;

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.Data.TypeVec

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

Tactic:
;

Goal state after:
α : TypeVec.{u_1} 0
x : Fin2 0
x✝ : α x
⊢ id x x✝ = nilFun x 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:
by
    intros
    simp only [callCC, StateT.callCC, StateT.goto_mkLabel, StateT.run_bind, StateT.run_mk,
      callCC_bind_left]; ext; rfl

Goal state after:
Module: Mathlib.Data.TypeVec

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

Tactic:
;

Goal state after:
β : Type u_1
x : β
α : TypeVec.{u_2} 0
i : Fin2 0
⊢ TypeVec.const x α i = nilFun i
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 α✝
s✝ : σ
⊢ (StateT.mk fun r ↦ dummy✝.run r).run s✝ = dummy✝.run s✝

Tactic:
;

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✝