mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Fin.Fin2

Goal state before:
pp: case zero
⊢ last.rev = fz

pp: case succ
n✝ : ℕ
a✝ : last.rev = fz
⊢ last.rev = fz

Tactic:
<;>

Goal state after:
case zero
⊢ last.rev = fz

case succ
n✝ : ℕ
a✝ : last.rev = fz
⊢ last.rev = fz
Module: Mathlib.Data.Fin.Fin2

Goal state before:
pp: case fz
n n✝ : ℕ
⊢ fz.castSucc.rev = fz.rev.fs

pp: case fs
n n✝ : ℕ
a✝ : Fin2 n✝
a_ih✝ : a✝.castSucc.rev = a✝.rev.fs
⊢ a✝.fs.castSucc.rev = a✝.fs.rev.fs

Tactic:
<;>

Goal state after:
case fz
n n✝ : ℕ
⊢ fz.castSucc.rev = fz.rev.fs

case fs
n n✝ : ℕ
a✝ : Fin2 n✝
a_ih✝ : a✝.castSucc.rev = a✝.rev.fs
⊢ a✝.fs.castSucc.rev = a✝.fs.rev.fs
Module: Mathlib.Data.Fin.Fin2

Goal state before:
pp: case fz
n n✝ : ℕ
⊢ fz.rev.rev = fz

pp: case fs
n n✝ : ℕ
a✝ : Fin2 n✝
a_ih✝ : a✝.rev.rev = a✝
⊢ a✝.fs.rev.rev = a✝.fs

Tactic:
<;>

Goal state after:
case fz
n n✝ : ℕ
⊢ fz.rev.rev = fz

case fs
n n✝ : ℕ
a✝ : Fin2 n✝
a_ih✝ : a✝.rev.rev = a✝
⊢ a✝.fs.rev.rev = a✝.fs
Module: Mathlib.Data.Fin.Fin2

Goal state before:
pp: case fz
n : ℕ
elems : Finset (Fin2 n)
compl : ∀ (x : Fin2 n), x ∈ elems
⊢ fz ∈ Finset.cons fz (Finset.map { toFun := fs, inj' := ⋯ } elems) ⋯

pp: case fs
n : ℕ
elems : Finset (Fin2 n)
compl : ∀ (x : Fin2 n), x ∈ elems
i : Fin2 n
⊢ i.fs ∈ Finset.cons fz (Finset.map { toFun := fs, inj' := ⋯ } elems) ⋯

Tactic:
<;>

Goal state after:
case fz
n : ℕ
elems : Finset (Fin2 n)
compl : ∀ (x : Fin2 n), x ∈ elems
⊢ fz ∈ Finset.cons fz (Finset.map { toFun := fs, inj' := ⋯ } elems) ⋯

case fs
n : ℕ
elems : Finset (Fin2 n)
compl : ∀ (x : Fin2 n), x ∈ elems
i : Fin2 n
⊢ i.fs ∈ Finset.cons fz (Finset.map { toFun := fs, inj' := ⋯ } elems) ⋯
Module: Mathlib.Control.Functor.Multivariate

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

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

Tactic:
<;>

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.Functor.Multivariate

Goal state before:
pp: case h₀.fz
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec.{u} n
β : Type u
P : β → Prop
x✝ : F (α ::: β)
x : (α ::: β) Fin2.fz
property✝ : α.PredLast P x
⊢ ↑((f P n α ⊚ g P n α) Fin2.fz ⟨x, property✝⟩) = ↑(TypeVec.id Fin2.fz ⟨x, property✝⟩)

pp: case h₀.fs
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec.{u} n
β : Type u
P : β → Prop
x✝ : F (α ::: β)
a✝ : Fin2 n
x : (α ::: β) a✝.fs
property✝ : α.PredLast P x
⊢ ↑((f P n α ⊚ g P n α) a✝.fs ⟨x, property✝⟩) = ↑(TypeVec.id a✝.fs ⟨x, property✝⟩)

Tactic:
<;>

Goal state after:
case h₀.fz
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec.{u} n
β : Type u
P : β → Prop
x✝ : F (α ::: β)
x : (α ::: β) Fin2.fz
property✝ : α.PredLast P x
⊢ ↑((f P n α ⊚ g P n α) Fin2.fz ⟨x, property✝⟩) = ↑(TypeVec.id Fin2.fz ⟨x, property✝⟩)

case h₀.fs
n : ℕ
F : TypeVec.{u} (n + 1) → Type u_1
inst✝¹ : MvFunctor F
inst✝ : LawfulMvFunctor F
α : TypeVec.{u} n
β : Type u
P : β → Prop
x✝ : F (α ::: β)
a✝ : Fin2 n
x : (α ::: β) a✝.fs
property✝ : α.PredLast P x
⊢ ↑((f P n α ⊚ g P n α) a✝.fs ⟨x, property✝⟩) = ↑(TypeVec.id a✝.fs ⟨x, property✝⟩)
Module: Mathlib.Control.Functor.Multivariate

Goal state before:
pp: case h₁.fz
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) }
x : (α ::: β) Fin2.fz
property✝ : ofRepeat (α.PredLast' P Fin2.fz x)
⊢ ↑⟨x, property✝⟩ = ↑(f P n α Fin2.fz ⟨x, property✝⟩)

pp: case h₁.fs
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) }
a✝ : Fin2 n
x : (α ::: β) a✝.fs
property✝ : ofRepeat (α.PredLast' P a✝.fs x)
⊢ ↑⟨x, property✝⟩ = ↑(f P n α a✝.fs ⟨x, property✝⟩)

Tactic:
<;>

Goal state after:
case h₁.fz
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) }
x : (α ::: β) Fin2.fz
property✝ : ofRepeat (α.PredLast' P Fin2.fz x)
⊢ ↑⟨x, property✝⟩ = ↑(f P n α Fin2.fz ⟨x, property✝⟩)

case h₁.fs
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) }
a✝ : Fin2 n
x : (α ::: β) a✝.fs
property✝ : ofRepeat (α.PredLast' P a✝.fs x)
⊢ ↑⟨x, property✝⟩ = ↑(f P n α a✝.fs ⟨x, property✝⟩)
Module: Mathlib.Control.Functor.Multivariate

Goal state before:
pp: case h₀.fz
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 (α ::: β)
x : (α ::: β) Fin2.fz × (α ::: β) Fin2.fz
property✝ : α.RelLast rr x.1 x.2
⊢ (f' rr n α ⊚ g' rr n α) Fin2.fz ⟨x, property✝⟩ = TypeVec.id Fin2.fz ⟨x, property✝⟩

pp: case h₀.fs
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 (α ::: β)
a✝ : Fin2 n
x : (α ::: β) a✝.fs × (α ::: β) a✝.fs
property✝ : α.RelLast rr x.1 x.2
⊢ (f' rr n α ⊚ g' rr n α) a✝.fs ⟨x, property✝⟩ = TypeVec.id a✝.fs ⟨x, property✝⟩

Tactic:
<;>

Goal state after:
case h₀.fz
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 (α ::: β)
x : (α ::: β) Fin2.fz × (α ::: β) Fin2.fz
property✝ : α.RelLast rr x.1 x.2
⊢ (f' rr n α ⊚ g' rr n α) Fin2.fz ⟨x, property✝⟩ = TypeVec.id Fin2.fz ⟨x, property✝⟩

case h₀.fs
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 (α ::: β)
a✝ : Fin2 n
x : (α ::: β) a✝.fs × (α ::: β) a✝.fs
property✝ : α.RelLast rr x.1 x.2
⊢ (f' rr n α ⊚ g' rr n α) a✝.fs ⟨x, property✝⟩ = TypeVec.id a✝.fs ⟨x, property✝⟩
Module: Mathlib.Control.Functor.Multivariate

Goal state before:
pp: case h₁.e_a.e_a.e_a
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) = fun i x ↦ (↑(f' rr n α i x)).1

pp: case h₁.e_b.e_a.e_a
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).2) = fun i x ↦ (↑(f' rr n α i x)).2

Tactic:
<;>

Goal state after:
case h₁.e_a.e_a.e_a
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) = fun i x ↦ (↑(f' rr n α i x)).1

case h₁.e_b.e_a.e_a
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).2) = fun i x ↦ (↑(f' rr n α i x)).2
Module: Mathlib.Control.Functor.Multivariate

Goal state before:
pp: case h₁.e_a.e_a.e_a
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)) }
i : Fin2 (n + 1)
x : (α ::: β) i × (α ::: β) i
property✝ : ofRepeat (α.RelLast' rr i (prod.mk i x.1 x.2))
⊢ (↑⟨x, property✝⟩).1 = (↑(f' rr n α i ⟨x, property✝⟩)).1

pp: case h₁.e_b.e_a.e_a
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)) }
i : Fin2 (n + 1)
x : (α ::: β) i × (α ::: β) i
property✝ : ofRepeat (α.RelLast' rr i (prod.mk i x.1 x.2))
⊢ (↑⟨x, property✝⟩).2 = (↑(f' rr n α i ⟨x, property✝⟩)).2

Tactic:
<;>

Goal state after:
case h₁.e_a.e_a.e_a
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)) }
i : Fin2 (n + 1)
x : (α ::: β) i × (α ::: β) i
property✝ : ofRepeat (α.RelLast' rr i (prod.mk i x.1 x.2))
⊢ (↑⟨x, property✝⟩).1 = (↑(f' rr n α i ⟨x, property✝⟩)).1

case h₁.e_b.e_a.e_a
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)) }
i : Fin2 (n + 1)
x : (α ::: β) i × (α ::: β) i
property✝ : ofRepeat (α.RelLast' rr i (prod.mk i x.1 x.2))
⊢ (↑⟨x, property✝⟩).2 = (↑(f' rr n α i ⟨x, property✝⟩)).2
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
⊢ 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
⊢ (∃ i, b ∈ approx (⇑f) i a) → b ∈ approx (⇑f) (Nat.find h₀).succ a

Tactic:
<;>

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

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

pp: case fs
n : ℕ
α : TypeVec.{u_1} (n + 1)
a✝ : Fin2 n
⊢ (α.drop ::: α.last) a✝.fs = α a✝.fs

Tactic:
<;>

Goal state after:
case fz
n : ℕ
α : TypeVec.{u_1} (n + 1)
⊢ (α.drop ::: α.last) Fin2.fz = α Fin2.fz

case fs
n : ℕ
α : TypeVec.{u_1} (n + 1)
a✝ : Fin2 n
⊢ (α.drop ::: α.last) a✝.fs = α a✝.fs
Module: Mathlib.Control.LawfulFix

Goal state before:
pp: case pos.mpr.inr.inl
α : 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 : ℕ
h₁ : y ∈ approx (⇑f) j a
this :
  ∀ {α : Type u_1} {β : α → Type u_2} (f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)) (a : α) (b : β a),
    (∃ i, (approx (⇑f) i a).Dom) →
      ∀ (y : β a) (i : ℕ), b ∈ approx (⇑f) i a → ∀ (j : ℕ), y ∈ approx (⇑f) j a → i ≤ j → y = b
case : ¬i ≤ j
H : i ≤ j
⊢ y = b

pp: case pos.mpr.inr.inr
α : 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 : ℕ
h₁ : y ∈ approx (⇑f) j a
this :
  ∀ {α : Type u_1} {β : α → Type u_2} (f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)) (a : α) (b : β a),
    (∃ i, (approx (⇑f) i a).Dom) →
      ∀ (y : β a) (i : ℕ), b ∈ approx (⇑f) i a → ∀ (j : ℕ), y ∈ approx (⇑f) j a → i ≤ j → y = b
case : ¬i ≤ j
H : j ≤ i
⊢ b = y

Tactic:
<;>

Goal state after:
case pos.mpr.inr.inl
α : 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 : ℕ
h₁ : y ∈ approx (⇑f) j a
this :
  ∀ {α : Type u_1} {β : α → Type u_2} (f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)) (a : α) (b : β a),
    (∃ i, (approx (⇑f) i a).Dom) →
      ∀ (y : β a) (i : ℕ), b ∈ approx (⇑f) i a → ∀ (j : ℕ), y ∈ approx (⇑f) j a → i ≤ j → y = b
case : ¬i ≤ j
H : i ≤ j
⊢ y = b

case pos.mpr.inr.inr
α : 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 : ℕ
h₁ : y ∈ approx (⇑f) j a
this :
  ∀ {α : Type u_1} {β : α → Type u_2} (f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)) (a : α) (b : β a),
    (∃ i, (approx (⇑f) i a).Dom) →
      ∀ (y : β a) (i : ℕ), b ∈ approx (⇑f) i a → ∀ (j : ℕ), y ∈ approx (⇑f) j a → i ≤ j → y = b
case : ¬i ≤ j
H : j ≤ i
⊢ b = y
Module: Mathlib.Control.Monad.Cont

Goal state before:
pp: case e_a.error
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 ω✝
a✝ : ε
⊢ (callCC fun f ↦
      match Except.error a✝ with
      | Except.ok x => (next✝ (ExceptT.mkLabel f) x).run
      | Except.error e => pure (Except.error e)) =
    match Except.error a✝ with
    | Except.ok x => callCC fun x_1 ↦ (next✝ (ExceptT.mkLabel x_1) x).run
    | Except.error e => pure (Except.error e)

pp: case e_a.ok
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 ω✝
a✝ : α✝
⊢ (callCC fun f ↦
      match Except.ok a✝ with
      | Except.ok x => (next✝ (ExceptT.mkLabel f) x).run
      | Except.error e => pure (Except.error e)) =
    match Except.ok a✝ with
    | Except.ok x => callCC fun x_1 ↦ (next✝ (ExceptT.mkLabel x_1) x).run
    | Except.error e => pure (Except.error e)

Tactic:
<;>

Goal state after:
case e_a.error
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 ω✝
a✝ : ε
⊢ (callCC fun f ↦
      match Except.error a✝ with
      | Except.ok x => (next✝ (ExceptT.mkLabel f) x).run
      | Except.error e => pure (Except.error e)) =
    match Except.error a✝ with
    | Except.ok x => callCC fun x_1 ↦ (next✝ (ExceptT.mkLabel x_1) x).run
    | Except.error e => pure (Except.error e)

case e_a.ok
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 ω✝
a✝ : α✝
⊢ (callCC fun f ↦
      match Except.ok a✝ with
      | Except.ok x => (next✝ (ExceptT.mkLabel f) x).run
      | Except.error e => pure (Except.error e)) =
    match Except.ok a✝ with
    | Except.ok x => callCC fun x_1 ↦ (next✝ (ExceptT.mkLabel x_1) x).run
    | Except.error e => pure (Except.error e)
Module: Mathlib.Data.TypeVec

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

pp: case fs
β : Type u_1
γ : Type u_2
x : γ
n : ℕ
α : TypeVec.{u_1} n
a✝ : Fin2 n
⊢ TypeVec.const x (α ::: β) a✝.fs = (TypeVec.const x α ::: fun x_1 ↦ x) a✝.fs

Tactic:
<;>

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

case fs
β : Type u_1
γ : Type u_2
x : γ
n : ℕ
α : TypeVec.{u_1} n
a✝ : Fin2 n
⊢ TypeVec.const x (α ::: β) a✝.fs = (TypeVec.const x α ::: fun x_1 ↦ x) a✝.fs
Module: Mathlib.Data.TypeVec

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

pp: case succ
β : Type u_1
n✝ : ℕ
a✝ : ∀ (α : TypeVec.{u_1} n✝), (α ::: β).repeatEq = splitFun α.repeatEq (uncurry Eq)
α : TypeVec.{u_1} (n✝ + 1)
⊢ (α ::: β).repeatEq = splitFun α.repeatEq (uncurry Eq)

Tactic:
<;>

Goal state after:
case zero
β : Type u_1
α : TypeVec.{u_1} 0
⊢ (α ::: β).repeatEq = splitFun α.repeatEq (uncurry Eq)

case succ
β : Type u_1
n✝ : ℕ
a✝ : ∀ (α : TypeVec.{u_1} n✝), (α ::: β).repeatEq = splitFun α.repeatEq (uncurry Eq)
α : TypeVec.{u_1} (n✝ + 1)
⊢ (α ::: β).repeatEq = splitFun α.repeatEq (uncurry Eq)
Module: Mathlib.Control.ULiftable

Goal state before:
pp: case error
s : Type u₀
s' : Type u₁
r : Type u_1
r' : Type u_2
w : Type u_3
w' : Type u_4
ε : Type u₀
α✝ : Type v₁
β✝ : Type v₂
e : α✝ ≃ β✝
a✝ : ε
⊢ Except.map (⇑e.symm) (Except.map (⇑e) (error a✝)) = error a✝

pp: case ok
s : Type u₀
s' : Type u₁
r : Type u_1
r' : Type u_2
w : Type u_3
w' : Type u_4
ε : Type u₀
α✝ : Type v₁
β✝ : Type v₂
e : α✝ ≃ β✝
a✝ : α✝
⊢ Except.map (⇑e.symm) (Except.map (⇑e) (ok a✝)) = ok a✝

Tactic:
<;>

Goal state after:
case error
s : Type u₀
s' : Type u₁
r : Type u_1
r' : Type u_2
w : Type u_3
w' : Type u_4
ε : Type u₀
α✝ : Type v₁
β✝ : Type v₂
e : α✝ ≃ β✝
a✝ : ε
⊢ Except.map (⇑e.symm) (Except.map (⇑e) (error a✝)) = error a✝

case ok
s : Type u₀
s' : Type u₁
r : Type u_1
r' : Type u_2
w : Type u_3
w' : Type u_4
ε : Type u₀
α✝ : Type v₁
β✝ : Type v₂
e : α✝ ≃ β✝
a✝ : α✝
⊢ Except.map (⇑e.symm) (Except.map (⇑e) (ok a✝)) = ok a✝
Module: Mathlib.Control.ULiftable

Goal state before:
pp: case error
s : Type u₀
s' : Type u₁
r : Type u_1
r' : Type u_2
w : Type u_3
w' : Type u_4
ε : Type u₀
α✝ : Type v₁
β✝ : Type v₂
e : α✝ ≃ β✝
a✝ : ε
⊢ Except.map (⇑e) (Except.map (⇑e.symm) (error a✝)) = error a✝

pp: case ok
s : Type u₀
s' : Type u₁
r : Type u_1
r' : Type u_2
w : Type u_3
w' : Type u_4
ε : Type u₀
α✝ : Type v₁
β✝ : Type v₂
e : α✝ ≃ β✝
a✝ : β✝
⊢ Except.map (⇑e) (Except.map (⇑e.symm) (ok a✝)) = ok a✝

Tactic:
<;>

Goal state after:
case error
s : Type u₀
s' : Type u₁
r : Type u_1
r' : Type u_2
w : Type u_3
w' : Type u_4
ε : Type u₀
α✝ : Type v₁
β✝ : Type v₂
e : α✝ ≃ β✝
a✝ : ε
⊢ Except.map (⇑e) (Except.map (⇑e.symm) (error a✝)) = error a✝

case ok
s : Type u₀
s' : Type u₁
r : Type u_1
r' : Type u_2
w : Type u_3
w' : Type u_4
ε : Type u₀
α✝ : Type v₁
β✝ : Type v₂
e : α✝ ≃ β✝
a✝ : β✝
⊢ Except.map (⇑e) (Except.map (⇑e.symm) (ok a✝)) = ok a✝
Module: Mathlib.Control.ULiftable

Goal state before:
pp: case none
s : Type u₀
s' : Type u₁
r : Type u_1
r' : Type u_2
w : Type u_3
w' : Type u_4
α✝ : Type u₀
β✝ : Type u₁
e : α✝ ≃ β✝
⊢ Option.map (⇑e.symm) (Option.map (⇑e) none) = none

pp: case some
s : Type u₀
s' : Type u₁
r : Type u_1
r' : Type u_2
w : Type u_3
w' : Type u_4
α✝ : Type u₀
β✝ : Type u₁
e : α✝ ≃ β✝
val✝ : α✝
⊢ Option.map (⇑e.symm) (Option.map (⇑e) (some val✝)) = some val✝

Tactic:
<;>

Goal state after:
case none
s : Type u₀
s' : Type u₁
r : Type u_1
r' : Type u_2
w : Type u_3
w' : Type u_4
α✝ : Type u₀
β✝ : Type u₁
e : α✝ ≃ β✝
⊢ Option.map (⇑e.symm) (Option.map (⇑e) none) = none

case some
s : Type u₀
s' : Type u₁
r : Type u_1
r' : Type u_2
w : Type u_3
w' : Type u_4
α✝ : Type u₀
β✝ : Type u₁
e : α✝ ≃ β✝
val✝ : α✝
⊢ Option.map (⇑e.symm) (Option.map (⇑e) (some val✝)) = some val✝
Module: Mathlib.Control.ULiftable

Goal state before:
pp: case none
s : Type u₀
s' : Type u₁
r : Type u_1
r' : Type u_2
w : Type u_3
w' : Type u_4
α✝ : Type u₀
β✝ : Type u₁
e : α✝ ≃ β✝
⊢ Option.map (⇑e) (Option.map (⇑e.symm) none) = none

pp: case some
s : Type u₀
s' : Type u₁
r : Type u_1
r' : Type u_2
w : Type u_3
w' : Type u_4
α✝ : Type u₀
β✝ : Type u₁
e : α✝ ≃ β✝
val✝ : β✝
⊢ Option.map (⇑e) (Option.map (⇑e.symm) (some val✝)) = some val✝

Tactic:
<;>

Goal state after:
case none
s : Type u₀
s' : Type u₁
r : Type u_1
r' : Type u_2
w : Type u_3
w' : Type u_4
α✝ : Type u₀
β✝ : Type u₁
e : α✝ ≃ β✝
⊢ Option.map (⇑e) (Option.map (⇑e.symm) none) = none

case some
s : Type u₀
s' : Type u₁
r : Type u_1
r' : Type u_2
w : Type u_3
w' : Type u_4
α✝ : Type u₀
β✝ : Type u₁
e : α✝ ≃ β✝
val✝ : β✝
⊢ Option.map (⇑e) (Option.map (⇑e.symm) (some val✝)) = some val✝
Module: Mathlib.Data.TypeVec

Goal state before:
pp: case fz
n n✝ : ℕ
α : TypeVec.{u_1} (n✝ + 1)
p : α ⟹ «repeat» (n✝ + 1) Prop
x : Subtype_ p Fin2.fz
⊢ (toSubtype p ⊚ ofSubtype p) Fin2.fz x = id Fin2.fz x

pp: case fs
n n✝ : ℕ
a✝ : Fin2 n✝
a_ih✝ :
  ∀ {α : TypeVec.{u_1} n✝} (p : α ⟹ «repeat» n✝ Prop) (x : Subtype_ p a✝), (toSubtype p ⊚ ofSubtype p) a✝ x = id a✝ x
α : TypeVec.{u_1} (n✝ + 1)
p : α ⟹ «repeat» (n✝ + 1) Prop
x : Subtype_ p a✝.fs
⊢ (toSubtype p ⊚ ofSubtype p) a✝.fs x = id a✝.fs x

Tactic:
<;>

Goal state after:
case fz
n n✝ : ℕ
α : TypeVec.{u_1} (n✝ + 1)
p : α ⟹ «repeat» (n✝ + 1) Prop
x : Subtype_ p Fin2.fz
⊢ (toSubtype p ⊚ ofSubtype p) Fin2.fz x = id Fin2.fz x

case fs
n n✝ : ℕ
a✝ : Fin2 n✝
a_ih✝ :
  ∀ {α : TypeVec.{u_1} n✝} (p : α ⟹ «repeat» n✝ Prop) (x : Subtype_ p a✝), (toSubtype p ⊚ ofSubtype p) a✝ x = id a✝ x
α : TypeVec.{u_1} (n✝ + 1)
p : α ⟹ «repeat» (n✝ + 1) Prop
x : Subtype_ p a✝.fs
⊢ (toSubtype p ⊚ ofSubtype p) a✝.fs x = id a✝.fs x
Module: Mathlib.Data.TypeVec

Goal state before:
pp: case fz
n n✝ : ℕ
α : TypeVec.{u_1} (n✝ + 1)
p : α ⟹ «repeat» (n✝ + 1) Prop
x : { x // ofRepeat (p Fin2.fz x) }
⊢ (subtypeVal p ⊚ toSubtype p) Fin2.fz x = ↑x

pp: case fs
n n✝ : ℕ
a✝ : Fin2 n✝
a_ih✝ :
  ∀ {α : TypeVec.{u_1} n✝} (p : α ⟹ «repeat» n✝ Prop) (x : (fun i ↦ { x // ofRepeat (p i x) }) a✝),
    (subtypeVal p ⊚ toSubtype p) a✝ x = ↑x
α : TypeVec.{u_1} (n✝ + 1)
p : α ⟹ «repeat» (n✝ + 1) Prop
x : { x // ofRepeat (p a✝.fs x) }
⊢ (subtypeVal p ⊚ toSubtype p) a✝.fs x = ↑x

Tactic:
<;>

Goal state after:
case fz
n n✝ : ℕ
α : TypeVec.{u_1} (n✝ + 1)
p : α ⟹ «repeat» (n✝ + 1) Prop
x : { x // ofRepeat (p Fin2.fz x) }
⊢ (subtypeVal p ⊚ toSubtype p) Fin2.fz x = ↑x

case fs
n n✝ : ℕ
a✝ : Fin2 n✝
a_ih✝ :
  ∀ {α : TypeVec.{u_1} n✝} (p : α ⟹ «repeat» n✝ Prop) (x : (fun i ↦ { x // ofRepeat (p i x) }) a✝),
    (subtypeVal p ⊚ toSubtype p) a✝ x = ↑x
α : TypeVec.{u_1} (n✝ + 1)
p : α ⟹ «repeat» (n✝ + 1) Prop
x : { x // ofRepeat (p a✝.fs x) }
⊢ (subtypeVal p ⊚ toSubtype p) a✝.fs x = ↑x
Module: Mathlib.Control.Traversable.Equiv

Goal state before:
pp: case mk.e_map
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst✝¹ : Functor t
inst✝ : LawfulFunctor t
map✝ : {α β : Type u} → (α → β) → t' α → t' β
mapConst✝ : {α β : Type u} → α → t' β → t' α
h₀ : ∀ {α β : Type u} (f : α → β), map f = Equiv.map eqv f
h₁ : ∀ {α β : Type u} (f : β), mapConst f = (Equiv.map eqv ∘ Function.const α) f
⊢ map✝ = fun {α β} ↦ Equiv.map eqv

pp: case mk.e_mapConst
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst✝¹ : Functor t
inst✝ : LawfulFunctor t
map✝ : {α β : Type u} → (α → β) → t' α → t' β
mapConst✝ : {α β : Type u} → α → t' β → t' α
h₀ : ∀ {α β : Type u} (f : α → β), map f = Equiv.map eqv f
h₁ : ∀ {α β : Type u} (f : β), mapConst f = (Equiv.map eqv ∘ Function.const α) f
⊢ mapConst✝ = fun {α β} ↦ Equiv.map eqv ∘ Function.const β

Tactic:
<;>

Goal state after:
case mk.e_map
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst✝¹ : Functor t
inst✝ : LawfulFunctor t
map✝ : {α β : Type u} → (α → β) → t' α → t' β
mapConst✝ : {α β : Type u} → α → t' β → t' α
h₀ : ∀ {α β : Type u} (f : α → β), map f = Equiv.map eqv f
h₁ : ∀ {α β : Type u} (f : β), mapConst f = (Equiv.map eqv ∘ Function.const α) f
⊢ map✝ = fun {α β} ↦ Equiv.map eqv

case mk.e_mapConst
t t' : Type u → Type u
eqv : (α : Type u) → t α ≃ t' α
inst✝¹ : Functor t
inst✝ : LawfulFunctor t
map✝ : {α β : Type u} → (α → β) → t' α → t' β
mapConst✝ : {α β : Type u} → α → t' β → t' α
h₀ : ∀ {α β : Type u} (f : α → β), map f = Equiv.map eqv f
h₁ : ∀ {α β : Type u} (f : β), mapConst f = (Equiv.map eqv ∘ Function.const α) f
⊢ mapConst✝ = fun {α β} ↦ Equiv.map eqv ∘ Function.const β