mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: case cons.cons.nil
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
y : List α
hy : y.length = 2
head✝¹ head✝ : α
hx : [head✝¹, head✝].length = 2
h : (Vector.Perm.isSetoid α 2) ⟨[head✝¹, head✝], hx⟩ ⟨y, hy⟩
⊢ Rel α (fromVector ⟨[head✝¹, head✝], hx⟩) (fromVector ⟨y, hy⟩)

pp: case cons.cons.cons
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
y : List α
hy : y.length = 2
head✝² head✝¹ head✝ : α
x : List α
hx : (head✝² :: head✝¹ :: head✝ :: x).length = 2
h : (Vector.Perm.isSetoid α 2) ⟨head✝² :: head✝¹ :: head✝ :: x, hx⟩ ⟨y, hy⟩
⊢ Rel α (fromVector ⟨head✝² :: head✝¹ :: head✝ :: x, hx⟩) (fromVector ⟨y, hy⟩)

Tactic:
;

Goal state after:
case cons.cons.nil
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
y : List α
hy : y.length = 2
head✝¹ head✝ : α
hx : [head✝¹, head✝].length = 2
h : (Vector.Perm.isSetoid α 2) ⟨[head✝¹, head✝], hx⟩ ⟨y, hy⟩
⊢ Rel α (fromVector ⟨[head✝¹, head✝], hx⟩) (fromVector ⟨y, hy⟩)

case cons.cons.cons
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
y : List α
hy : y.length = 2
head✝² head✝¹ head✝ : α
x : List α
hx : (head✝² :: head✝¹ :: head✝ :: x).length = 2
h : (Vector.Perm.isSetoid α 2) ⟨head✝² :: head✝¹ :: head✝ :: x, hx⟩ ⟨y, hy⟩
⊢ Rel α (fromVector ⟨head✝² :: head✝¹ :: head✝ :: x, hx⟩) (fromVector ⟨y, hy⟩)
Module: Mathlib.CategoryTheory.Category.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : Epi (f ≫ g)
⊢ Epi g

Tactic:
;

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : Epi (f ≫ g)
⊢ Epi g
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: case cons.cons.nil.nil
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
head✝¹ head✝ : α
hx : [head✝¹, head✝].length = 2
hy : [].length = 2
h : (Vector.Perm.isSetoid α 2) ⟨[head✝¹, head✝], hx⟩ ⟨[], hy⟩
⊢ Rel α (fromVector ⟨[head✝¹, head✝], hx⟩) (fromVector ⟨[], hy⟩)

pp: case cons.cons.nil.cons
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
head✝² head✝¹ : α
hx : [head✝², head✝¹].length = 2
head✝ : α
y : List α
hy : (head✝ :: y).length = 2
h : (Vector.Perm.isSetoid α 2) ⟨[head✝², head✝¹], hx⟩ ⟨head✝ :: y, hy⟩
⊢ Rel α (fromVector ⟨[head✝², head✝¹], hx⟩) (fromVector ⟨head✝ :: y, hy⟩)

Tactic:
;

Goal state after:
case cons.cons.nil.nil
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
head✝¹ head✝ : α
hx : [head✝¹, head✝].length = 2
hy : [].length = 2
h : (Vector.Perm.isSetoid α 2) ⟨[head✝¹, head✝], hx⟩ ⟨[], hy⟩
⊢ Rel α (fromVector ⟨[head✝¹, head✝], hx⟩) (fromVector ⟨[], hy⟩)

case cons.cons.nil.cons
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
head✝² head✝¹ : α
hx : [head✝², head✝¹].length = 2
head✝ : α
y : List α
hy : (head✝ :: y).length = 2
h : (Vector.Perm.isSetoid α 2) ⟨[head✝², head✝¹], hx⟩ ⟨head✝ :: y, hy⟩
⊢ Rel α (fromVector ⟨[head✝², head✝¹], hx⟩) (fromVector ⟨head✝ :: y, hy⟩)
Module: Mathlib.Combinatorics.Quiver.Prefunctor

Goal state before:
pp: case refl
U : Type u_1
V : Type u_2
inst✝¹ : Quiver U
inst✝ : Quiver V
F : U ⥤q V
X : U
⊢ F.obj X = F.obj X

Tactic:
;

Goal state after:
case refl
U : Type u_1
V : Type u_2
inst✝¹ : Quiver U
inst✝ : Quiver V
F : U ⥤q V
X : U
⊢ F.obj X = F.obj X
Module: Mathlib.Combinatorics.Quiver.Prefunctor

Goal state before:
pp: U : Type u_1
V : Type u_2
inst✝¹ : Quiver U
inst✝ : Quiver V
F : U ⥤q V
X Y : U
f : X ⟶ Y
⊢ F.map (Quiver.homOfEq f ⋯ ⋯) = Quiver.homOfEq (F.map f) ⋯ ⋯

Tactic:
;

Goal state after:
U : Type u_1
V : Type u_2
inst✝¹ : Quiver U
inst✝ : Quiver V
F : U ⥤q V
X Y : U
f : X ⟶ Y
⊢ F.map (Quiver.homOfEq f ⋯ ⋯) = Quiver.homOfEq (F.map f) ⋯ ⋯
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: case cons.cons.nil.cons.nil
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
head✝² head✝¹ : α
hx : [head✝², head✝¹].length = 2
head✝ : α
hy : [head✝].length = 2
h : (Vector.Perm.isSetoid α 2) ⟨[head✝², head✝¹], hx⟩ ⟨[head✝], hy⟩
⊢ Rel α (fromVector ⟨[head✝², head✝¹], hx⟩) (fromVector ⟨[head✝], hy⟩)

pp: case cons.cons.nil.cons.cons
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
head✝³ head✝² : α
hx : [head✝³, head✝²].length = 2
head✝¹ head✝ : α
y : List α
hy : (head✝¹ :: head✝ :: y).length = 2
h : (Vector.Perm.isSetoid α 2) ⟨[head✝³, head✝²], hx⟩ ⟨head✝¹ :: head✝ :: y, hy⟩
⊢ Rel α (fromVector ⟨[head✝³, head✝²], hx⟩) (fromVector ⟨head✝¹ :: head✝ :: y, hy⟩)

Tactic:
;

Goal state after:
case cons.cons.nil.cons.nil
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
head✝² head✝¹ : α
hx : [head✝², head✝¹].length = 2
head✝ : α
hy : [head✝].length = 2
h : (Vector.Perm.isSetoid α 2) ⟨[head✝², head✝¹], hx⟩ ⟨[head✝], hy⟩
⊢ Rel α (fromVector ⟨[head✝², head✝¹], hx⟩) (fromVector ⟨[head✝], hy⟩)

case cons.cons.nil.cons.cons
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
head✝³ head✝² : α
hx : [head✝³, head✝²].length = 2
head✝¹ head✝ : α
y : List α
hy : (head✝¹ :: head✝ :: y).length = 2
h : (Vector.Perm.isSetoid α 2) ⟨[head✝³, head✝²], hx⟩ ⟨head✝¹ :: head✝ :: y, hy⟩
⊢ Rel α (fromVector ⟨[head✝³, head✝²], hx⟩) (fromVector ⟨head✝¹ :: head✝ :: y, hy⟩)
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: case cons.cons.nil.cons.cons.nil
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
head✝³ head✝² : α
hx : [head✝³, head✝²].length = 2
head✝¹ head✝ : α
hy : [head✝¹, head✝].length = 2
h : (Vector.Perm.isSetoid α 2) ⟨[head✝³, head✝²], hx⟩ ⟨[head✝¹, head✝], hy⟩
⊢ Rel α (fromVector ⟨[head✝³, head✝²], hx⟩) (fromVector ⟨[head✝¹, head✝], hy⟩)

pp: case cons.cons.nil.cons.cons.cons
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
head✝⁴ head✝³ : α
hx : [head✝⁴, head✝³].length = 2
head✝² head✝¹ head✝ : α
y : List α
hy : (head✝² :: head✝¹ :: head✝ :: y).length = 2
h : (Vector.Perm.isSetoid α 2) ⟨[head✝⁴, head✝³], hx⟩ ⟨head✝² :: head✝¹ :: head✝ :: y, hy⟩
⊢ Rel α (fromVector ⟨[head✝⁴, head✝³], hx⟩) (fromVector ⟨head✝² :: head✝¹ :: head✝ :: y, hy⟩)

Tactic:
;

Goal state after:
case cons.cons.nil.cons.cons.nil
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
head✝³ head✝² : α
hx : [head✝³, head✝²].length = 2
head✝¹ head✝ : α
hy : [head✝¹, head✝].length = 2
h : (Vector.Perm.isSetoid α 2) ⟨[head✝³, head✝²], hx⟩ ⟨[head✝¹, head✝], hy⟩
⊢ Rel α (fromVector ⟨[head✝³, head✝²], hx⟩) (fromVector ⟨[head✝¹, head✝], hy⟩)

case cons.cons.nil.cons.cons.cons
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
head✝⁴ head✝³ : α
hx : [head✝⁴, head✝³].length = 2
head✝² head✝¹ head✝ : α
y : List α
hy : (head✝² :: head✝¹ :: head✝ :: y).length = 2
h : (Vector.Perm.isSetoid α 2) ⟨[head✝⁴, head✝³], hx⟩ ⟨head✝² :: head✝¹ :: head✝ :: y, hy⟩
⊢ Rel α (fromVector ⟨[head✝⁴, head✝³], hx⟩) (fromVector ⟨head✝² :: head✝¹ :: head✝ :: y, hy⟩)
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
⊢ ∀ (x y : α), Quot.map fromVector ⋯ (Quot.map (fun x ↦ ⟨[x.1, x.2], ⋯⟩) ⋯ s(x, y)) = s(x, y)

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
⊢ ∀ (x y : α), Quot.map fromVector ⋯ (Quot.map (fun x ↦ ⟨[x.1, x.2], ⋯⟩) ⋯ s(x, y)) = s(x, y)
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
inst✝ : DecidableEq α
a b c d e : α
h✝ : Rel α (b, c) (d, e)
hy : a ∈ s(d, e)
h : a ∈ s(b, c)
⊢ Eq.ndrec (motive := fun x ↦ a ∈ x → α) (fun x ↦ if a = b then c else b) ⋯ h = if a = b then c else b

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
z : Sym2 α
f : α → β
inst✝ : DecidableEq α
a b c d e : α
h✝ : Rel α (b, c) (d, e)
hy : a ∈ s(d, e)
h : a ∈ s(b, c)
⊢ Eq.ndrec (motive := fun x ↦ a ∈ x → α) (fun x ↦ if a = b then c else b) ⋯ h = if a = b then c else b
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: case mk
α : Type u_1
s : Set α
x✝ : Sym2 α
x y : α
⊢ Quot.mk (Rel α) (x, y) ∈ s.sym2 ↔ Quot.mk (Rel α) (x, y) ∈ uncurry Sym2.mk '' s ×ˢ s

Tactic:
;

Goal state after:
case mk
α : Type u_1
s : Set α
x✝ : Sym2 α
x y : α
⊢ Quot.mk (Rel α) (x, y) ∈ s.sym2 ↔ Quot.mk (Rel α) (x, y) ∈ uncurry Sym2.mk '' s ×ˢ s
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: case mk
α : Type u_1
x✝ : Sym2 α
x y : α
⊢ Quot.mk (Rel α) (x, y) ∈ ∅.sym2 ↔ Quot.mk (Rel α) (x, y) ∈ ∅

Tactic:
;

Goal state after:
case mk
α : Type u_1
x✝ : Sym2 α
x y : α
⊢ Quot.mk (Rel α) (x, y) ∈ ∅.sym2 ↔ Quot.mk (Rel α) (x, y) ∈ ∅
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: case mk
α : Type u_1
x✝ : Sym2 α
x y : α
⊢ Quot.mk (Rel α) (x, y) ∈ univ.sym2 ↔ Quot.mk (Rel α) (x, y) ∈ univ

Tactic:
;

Goal state after:
case mk
α : Type u_1
x✝ : Sym2 α
x y : α
⊢ Quot.mk (Rel α) (x, y) ∈ univ.sym2 ↔ Quot.mk (Rel α) (x, y) ∈ univ
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: case mk
α : Type u_1
a : α
x✝ : Sym2 α
x y : α
⊢ Quot.mk (Rel α) (x, y) ∈ {a}.sym2 ↔ Quot.mk (Rel α) (x, y) ∈ {s(a, a)}

Tactic:
;

Goal state after:
case mk
α : Type u_1
a : α
x✝ : Sym2 α
x y : α
⊢ Quot.mk (Rel α) (x, y) ∈ {a}.sym2 ↔ Quot.mk (Rel α) (x, y) ∈ {s(a, a)}
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: case mk
α : Type u_1
a : α
s : Set α
x✝ : Sym2 α
x y : α
⊢ Quot.mk (Rel α) (x, y) ∈ (insert a s).sym2 ↔ Quot.mk (Rel α) (x, y) ∈ (fun b ↦ s(a, b)) '' insert a s ∪ s.sym2

Tactic:
;

Goal state after:
case mk
α : Type u_1
a : α
s : Set α
x✝ : Sym2 α
x y : α
⊢ Quot.mk (Rel α) (x, y) ∈ (insert a s).sym2 ↔ Quot.mk (Rel α) (x, y) ∈ (fun b ↦ s(a, b)) '' insert a s ∪ s.sym2
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: case mk
α : Type u_1
ι : Type u_4
f : ι → Set α
x✝ : Sym2 α
x y : α
⊢ Quot.mk (Rel α) (x, y) ∈ (⋂ i, f i).sym2 ↔ Quot.mk (Rel α) (x, y) ∈ ⋂ i, (f i).sym2

Tactic:
;

Goal state after:
case mk
α : Type u_1
ι : Type u_4
f : ι → Set α
x✝ : Sym2 α
x y : α
⊢ Quot.mk (Rel α) (x, y) ∈ (⋂ i, f i).sym2 ↔ Quot.mk (Rel α) (x, y) ∈ ⋂ i, (f i).sym2
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
ι : Type u_4
f : ι → Set α
⊢ (⋂ i, f i).sym2 = ⋂ i, (f i).sym2

Tactic:
ext ⟨x, y⟩; simp [forall_and]

Goal state after:
Module: Mathlib.CategoryTheory.Iso

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z Z' : C
α : X ≅ Y
β : Y ≅ Z
γ : Z ≅ Z'
⊢ ((α ≪≫ β) ≪≫ γ).hom = (α ≪≫ β ≪≫ γ).hom

Tactic:
;

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y Z Z' : C
α : X ≅ Y
β : Y ≅ Z
γ : Z ≅ Z'
⊢ ((α ≪≫ β) ≪≫ γ).hom = (α ≪≫ β ≪≫ γ).hom
Module: Mathlib.CategoryTheory.Iso

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
α : X ≅ Y
⊢ (refl X ≪≫ α).hom = α.hom

Tactic:
;

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y : C
α : X ≅ Y
⊢ (refl X ≪≫ α).hom = α.hom
Module: Mathlib.CategoryTheory.Iso

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
α : X ≅ Y
⊢ (α ≪≫ refl Y).hom = α.hom

Tactic:
;

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y : C
α : X ≅ Y
⊢ (α ≪≫ refl Y).hom = α.hom
Module: Mathlib.CategoryTheory.Iso

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
i : X ≅ Y
j : Y ≅ Z
⊢ (F.mapIso (i ≪≫ j)).hom = (F.mapIso i ≪≫ F.mapIso j).hom

Tactic:
;

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
i : X ≅ Y
j : Y ≅ Z
⊢ (F.mapIso (i ≪≫ j)).hom = (F.mapIso i ≪≫ F.mapIso j).hom
Module: Mathlib.CategoryTheory.ObjectProperty.Basic

Goal state before:
pp: C : Type u
inst✝ : CategoryStruct.{v, u} C
ι : Type u'
X : ι → C
P : ObjectProperty C
h : ∀ (i : ι), P (X i)
i : ι
⊢ P (X i)

Tactic:
;

Goal state after:
C : Type u
inst✝ : CategoryStruct.{v, u} C
ι : Type u'
X : ι → C
P : ObjectProperty C
h : ∀ (i : ι), P (X i)
i : ι
⊢ P (X i)
Module: Mathlib.CategoryTheory.ObjectProperty.Basic

Goal state before:
pp: C : Type u
inst✝ : CategoryStruct.{v, u} C
P : ObjectProperty C
X : C
hX : P X
⊢ P ↑⟨X, hX⟩

Tactic:
;

Goal state after:
C : Type u
inst✝ : CategoryStruct.{v, u} C
P : ObjectProperty C
X : C
hX : P X
⊢ P ↑⟨X, hX⟩
Module: Mathlib.CategoryTheory.ObjectProperty.Basic

Goal state before:
pp: case mpr.inl
C : Type u
inst✝ : CategoryStruct.{v, u} C
X Y : C
⊢ pair X Y X

pp: case mpr.inr
C : Type u
inst✝ : CategoryStruct.{v, u} C
X Y : C
⊢ pair X Y Y

Tactic:
;

Goal state after:
case mpr.inl
C : Type u
inst✝ : CategoryStruct.{v, u} C
X Y : C
⊢ pair X Y X

case mpr.inr
C : Type u
inst✝ : CategoryStruct.{v, u} C
X Y : C
⊢ pair X Y Y
Module: Mathlib.CategoryTheory.ObjectProperty.Basic

Goal state before:
pp: C : Type u
D : Type u'
inst✝¹ : Category.{v, u} C
inst✝ : Category.{v', u'} D
P : ObjectProperty C
F : C ⥤ D
X : C
hX : P X
⊢ ∃ X_1, P X_1 ∧ F.obj X_1 = F.obj X

Tactic:
;

Goal state after:
C : Type u
D : Type u'
inst✝¹ : Category.{v, u} C
inst✝ : Category.{v', u'} D
P : ObjectProperty C
F : C ⥤ D
X : C
hX : P X
⊢ ∃ X_1, P X_1 ∧ F.obj X_1 = F.obj X
Module: Mathlib.CategoryTheory.ObjectProperty.Basic

Goal state before:
pp: C : Type u
D : Type u'
inst✝¹ : Category.{v, u} C
inst✝ : Category.{v', u'} D
P : ObjectProperty C
F : C ⥤ D
X : C
hX : P X
⊢ P.strictMap F (F.obj X)

Tactic:
;

Goal state after:
C : Type u
D : Type u'
inst✝¹ : Category.{v, u} C
inst✝ : Category.{v', u'} D
P : ObjectProperty C
F : C ⥤ D
X : C
hX : P X
⊢ P.strictMap F (F.obj X)
Module: Mathlib.CategoryTheory.Functor.Category

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F G : C ⥤ D
H I : D ⥤ E
α : G ⟶ F
β : I ⟶ H
x : C
⊢ { app := fun X ↦ β.app (G.obj X) ≫ H.map (α.app X), naturality := ⋯ }.app x =
    (mk' (fun X ↦ I.map (α.app X) ≫ β.app (F.obj X)) ⋯).app x

Tactic:
;

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F G : C ⥤ D
H I : D ⥤ E
α : G ⟶ F
β : I ⟶ H
x : C
⊢ { app := fun X ↦ β.app (G.obj X) ≫ H.map (α.app X), naturality := ⋯ }.app x =
    (mk' (fun X ↦ I.map (α.app X) ≫ β.app (F.obj X)) ⋯).app x
Module: Mathlib.CategoryTheory.Functor.FullyFaithful

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
G : D ⥤ E
inst✝¹ : G.Faithful
obj : C → D
map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)
F_obj : C → E
map✝ : {X Y : C} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
map_id✝ : ∀ (X : C), map✝ (𝟙 X) = 𝟙 (F_obj X)
map_comp✝ : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), map✝ (f ≫ g) = map✝ f ≫ map✝ g
inst✝ : { obj := F_obj, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.Faithful
h_obj : ∀ (X : C), G.obj (obj X) = { obj := F_obj, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.obj X
h_map :
  ∀ {X Y : C} {f : X ⟶ Y}, G.map (map f) ≍ { obj := F_obj, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.map f
⊢ Faithful.div { obj := F_obj, map := map✝, map_id := map_id✝, map_comp := map_comp✝ } G obj h_obj map h_map ⋙ G =
    { obj := F_obj, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }

Tactic:
;

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
G : D ⥤ E
inst✝¹ : G.Faithful
obj : C → D
map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)
F_obj : C → E
map✝ : {X Y : C} → (X ⟶ Y) → (F_obj X ⟶ F_obj Y)
map_id✝ : ∀ (X : C), map✝ (𝟙 X) = 𝟙 (F_obj X)
map_comp✝ : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), map✝ (f ≫ g) = map✝ f ≫ map✝ g
inst✝ : { obj := F_obj, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.Faithful
h_obj : ∀ (X : C), G.obj (obj X) = { obj := F_obj, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.obj X
h_map :
  ∀ {X Y : C} {f : X ⟶ Y}, G.map (map f) ≍ { obj := F_obj, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.map f
⊢ Faithful.div { obj := F_obj, map := map✝, map_id := map_id✝, map_comp := map_comp✝ } G obj h_obj map h_map ⋙ G =
    { obj := F_obj, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }
Module: Mathlib.CategoryTheory.ConcreteCategory.Basic

Goal state before:
pp: C✝ : Type u
inst✝⁵ : Category.{v, u} C✝
FC : C✝ → C✝ → Type u_1
CC : C✝ → Type w
inst✝⁴ : (X Y : C✝) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory C✝ FC
C : Type u
D : Type u'
inst✝² : Category.{v', u'} D
FD : D → D → Type u_2
CD : D → Type w
inst✝¹ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝ : ConcreteCategory D FD
f : C → D
X✝ Y✝ : InducedCategory D f
x✝ : X✝ ⟶ Y✝
⊢ hom (homMk (ofHom (hom x✝.hom))).hom = hom x✝.hom

Tactic:
;

Goal state after:
C✝ : Type u
inst✝⁵ : Category.{v, u} C✝
FC : C✝ → C✝ → Type u_1
CC : C✝ → Type w
inst✝⁴ : (X Y : C✝) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory C✝ FC
C : Type u
D : Type u'
inst✝² : Category.{v', u'} D
FD : D → D → Type u_2
CD : D → Type w
inst✝¹ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝ : ConcreteCategory D FD
f : C → D
X✝ Y✝ : InducedCategory D f
x✝ : X✝ ⟶ Y✝
⊢ hom (homMk (ofHom (hom x✝.hom))).hom = hom x✝.hom
Module: Mathlib.CategoryTheory.ConcreteCategory.Basic

Goal state before:
pp: C✝ : Type u
inst✝⁵ : Category.{v, u} C✝
FC✝ : C✝ → C✝ → Type u_1
CC✝ : C✝ → Type w
inst✝⁴ : (X Y : C✝) → FunLike (FC✝ X Y) (CC✝ X) (CC✝ Y)
inst✝³ : ConcreteCategory C✝ FC✝
C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_2
CC : C → Type w
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
P : ObjectProperty C
X✝ Y✝ : P.FullSubcategory
x✝ : X✝ ⟶ Y✝
⊢ hom (homMk (ofHom (hom x✝.hom))).hom = hom x✝.hom

Tactic:
;

Goal state after:
C✝ : Type u
inst✝⁵ : Category.{v, u} C✝
FC✝ : C✝ → C✝ → Type u_1
CC✝ : C✝ → Type w
inst✝⁴ : (X Y : C✝) → FunLike (FC✝ X Y) (CC✝ X) (CC✝ Y)
inst✝³ : ConcreteCategory C✝ FC✝
C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_2
CC : C → Type w
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
P : ObjectProperty C
X✝ Y✝ : P.FullSubcategory
x✝ : X✝ ⟶ Y✝
⊢ hom (homMk (ofHom (hom x✝.hom))).hom = hom x✝.hom
Module: Mathlib.Logic.Lemmas

Goal state before:
pp: f : Prop → Prop
h₁ : f True
h₀ : f False
p : Prop
⊢ f p

Tactic:
;

Goal state after:
f : Prop → Prop
h₁ : f True
h₀ : f False
p : Prop
⊢ f p
Module: Mathlib.Combinatorics.Quiver.Path

Goal state before:
pp: V : Type u
inst✝ : Quiver V
a b c : V
p₁ : Path a b
q₁ : Path b c
hq : q₁.length = q₁.length
⊢ p₁.comp q₁ = p₁.comp q₁

Tactic:
;

Goal state after:
V : Type u
inst✝ : Quiver V
a b c : V
p₁ : Path a b
q₁ : Path b c
hq : q₁.length = q₁.length
⊢ p₁.comp q₁ = p₁.comp q₁
Module: Mathlib.Combinatorics.Quiver.Path

Goal state before:
pp: V : Type u
inst✝ : Quiver V
a b c : V
p₁ : Path a b
q₁ : Path b c
h : p₁.length = p₁.length
⊢ p₁.comp q₁ = p₁.comp q₁

Tactic:
;

Goal state after:
V : Type u
inst✝ : Quiver V
a b c : V
p₁ : Path a b
q₁ : Path b c
h : p₁.length = p₁.length
⊢ p₁.comp q₁ = p₁.comp q₁
Module: Mathlib.Combinatorics.Quiver.Symmetric

Goal state before:
pp: V : Type u_2
inst✝¹ : Quiver V
V' : Type u_4
inst✝ : Quiver V'
h : HasInvolutiveReverse V'
φ : V ⥤q V'
X Y : Symmetrify V
f : X ⟶ Y
⊢ (match Sum.swap f with
    | Sum.inl g => φ.map g
    | Sum.inr g => reverse (φ.map g)) =
    reverse
      (match f with
      | Sum.inl g => φ.map g
      | Sum.inr g => reverse (φ.map g))

Tactic:
;

Goal state after:
V : Type u_2
inst✝¹ : Quiver V
V' : Type u_4
inst✝ : Quiver V'
h : HasInvolutiveReverse V'
φ : V ⥤q V'
X Y : Symmetrify V
f : X ⟶ Y
⊢ (match Sum.swap f with
    | Sum.inl g => φ.map g
    | Sum.inr g => reverse (φ.map g)) =
    reverse
      (match f with
      | Sum.inl g => φ.map g
      | Sum.inr g => reverse (φ.map g))
Module: Mathlib.Combinatorics.Quiver.Path

Goal state before:
pp: V✝ : Type u
inst✝² : Quiver V✝
a b c d : V✝
inst✝¹ : ∀ (a b : V✝), Subsingleton (a ⟶ b)
V : Type u_1
inst✝ : Quiver V
n : ℕ
h₁ : DecidableEq V
h₂ : (v w : V) → DecidableEq (v ⟶ w)
h₃ : (v w : V) → DecidableEq (BoundedPaths v w n)
v w : V
p q : Path v w
a✝¹ x✝² v' v'' : V
x✝¹ x✝ : BoundedPaths a✝¹ x✝² (n + 1)
a✝ : V
p' : Path a✝¹ a✝
α : a✝ ⟶ x✝²
q' : Path a✝¹ a✝
β : a✝ ⟶ x✝²
hq : (q'.cons β).length ≤ n + 1
h : α = β
hp : p'.length ≤ n
⊢ p'.length ≤ n

Tactic:
;

Goal state after:
V✝ : Type u
inst✝² : Quiver V✝
a b c d : V✝
inst✝¹ : ∀ (a b : V✝), Subsingleton (a ⟶ b)
V : Type u_1
inst✝ : Quiver V
n : ℕ
h₁ : DecidableEq V
h₂ : (v w : V) → DecidableEq (v ⟶ w)
h₃ : (v w : V) → DecidableEq (BoundedPaths v w n)
v w : V
p q : Path v w
a✝¹ x✝² v' v'' : V
x✝¹ x✝ : BoundedPaths a✝¹ x✝² (n + 1)
a✝ : V
p' : Path a✝¹ a✝
α : a✝ ⟶ x✝²
q' : Path a✝¹ a✝
β : a✝ ⟶ x✝²
hq : (q'.cons β).length ≤ n + 1
h : α = β
hp : p'.length ≤ n
⊢ p'.length ≤ n
Module: Mathlib.Combinatorics.Quiver.Path

Goal state before:
pp: V✝ : Type u
inst✝² : Quiver V✝
a b c d : V✝
inst✝¹ : ∀ (a b : V✝), Subsingleton (a ⟶ b)
V : Type u_1
inst✝ : Quiver V
n : ℕ
h₁ : DecidableEq V
h₂ : (v w : V) → DecidableEq (v ⟶ w)
h₃ : (v w : V) → DecidableEq (BoundedPaths v w n)
v w : V
p q : Path v w
a✝¹ x✝² v' v'' : V
x✝¹ x✝ : BoundedPaths a✝¹ x✝² (n + 1)
a✝ : V
p' : Path a✝¹ a✝
α : a✝ ⟶ x✝²
q' : Path a✝¹ a✝
β : a✝ ⟶ x✝²
hp : (p'.cons α).length ≤ n + 1
h : α = β
hp' : p'.length ≤ n
hq : q'.length ≤ n
⊢ q'.length ≤ n

Tactic:
;

Goal state after:
V✝ : Type u
inst✝² : Quiver V✝
a b c d : V✝
inst✝¹ : ∀ (a b : V✝), Subsingleton (a ⟶ b)
V : Type u_1
inst✝ : Quiver V
n : ℕ
h₁ : DecidableEq V
h₂ : (v w : V) → DecidableEq (v ⟶ w)
h₃ : (v w : V) → DecidableEq (BoundedPaths v w n)
v w : V
p q : Path v w
a✝¹ x✝² v' v'' : V
x✝¹ x✝ : BoundedPaths a✝¹ x✝² (n + 1)
a✝ : V
p' : Path a✝¹ a✝
α : a✝ ⟶ x✝²
q' : Path a✝¹ a✝
β : a✝ ⟶ x✝²
hp : (p'.cons α).length ≤ n + 1
h : α = β
hp' : p'.length ≤ n
hq : q'.length ≤ n
⊢ q'.length ≤ n
Module: Mathlib.Combinatorics.Quiver.Symmetric

Goal state before:
pp: U : Type u_1
V : Type u_2
W : Type u_3
inst✝² : Quiver U
inst✝¹ : Quiver V
inst✝ : Quiver W
V' : Type u_4
σ : V → V'
h : HasInvolutiveReverse V
a✝ b✝ : Push σ
X✝ Y✝ : V
f : X✝ ⟶ Y✝
⊢ PushQuiver.arrow (HasReverse.reverse' (HasReverse.reverse' f)) = PushQuiver.arrow f

Tactic:
;

Goal state after:
U : Type u_1
V : Type u_2
W : Type u_3
inst✝² : Quiver U
inst✝¹ : Quiver V
inst✝ : Quiver W
V' : Type u_4
σ : V → V'
h : HasInvolutiveReverse V
a✝ b✝ : Push σ
X✝ Y✝ : V
f : X✝ ⟶ Y✝
⊢ PushQuiver.arrow (HasReverse.reverse' (HasReverse.reverse' f)) = PushQuiver.arrow f
Module: Mathlib.Combinatorics.Quiver.Symmetric

Goal state before:
pp: U : Type u_1
V : Type u_2
W : Type u_3
inst✝² : Quiver U
inst✝¹ : Quiver V
inst✝ : Quiver W
V' : Type u_4
σ : V → V'
h : HasInvolutiveReverse V
a✝ b✝ : Push σ
X✝ Y✝ : V
f : X✝ ⟶ Y✝
⊢ HasReverse.reverse' (HasReverse.reverse' f) = f

Tactic:
;

Goal state after:
U : Type u_1
V : Type u_2
W : Type u_3
inst✝² : Quiver U
inst✝¹ : Quiver V
inst✝ : Quiver W
V' : Type u_4
σ : V → V'
h : HasInvolutiveReverse V
a✝ b✝ : Push σ
X✝ Y✝ : V
f : X✝ ⟶ Y✝
⊢ HasReverse.reverse' (HasReverse.reverse' f) = f
Module: Mathlib.Combinatorics.Quiver.Path

Goal state before:
pp: V : Type u₁
inst✝¹ : Quiver V
W : Type u₂
inst✝ : Quiver W
F : V ⥤q W
a b : V
p : Path a b
c b✝ : V
q : Path b b✝
e : b✝ ⟶ c
⊢ (F.mapPath (p.comp q)).cons (F.map e) = ((F.mapPath p).comp (F.mapPath q)).cons (F.map e)

Tactic:
;

Goal state after:
V : Type u₁
inst✝¹ : Quiver V
W : Type u₂
inst✝ : Quiver W
F : V ⥤q W
a b : V
p : Path a b
c b✝ : V
q : Path b b✝
e : b✝ ⟶ c
⊢ (F.mapPath (p.comp q)).cons (F.map e) = ((F.mapPath p).comp (F.mapPath q)).cons (F.map e)
Module: Mathlib.Combinatorics.Quiver.Path

Goal state before:
pp: V : Type u₁
inst✝ : Quiver V
a b✝¹ b b✝ : V
q : Path a b✝
e : b✝ ⟶ b
⊢ ((𝟭q V).mapPath q).cons e = q.cons e

Tactic:
;

Goal state after:
V : Type u₁
inst✝ : Quiver V
a b✝¹ b b✝ : V
q : Path a b✝
e : b✝ ⟶ b
⊢ ((𝟭q V).mapPath q).cons e = q.cons e
Module: Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : ObjectProperty C
h : P.isoClosure = P
⊢ P.isoClosure.IsClosedUnderIsomorphisms

Tactic:
;

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
P : ObjectProperty C
h : P.isoClosure = P
⊢ P.isoClosure.IsClosedUnderIsomorphisms
Module: Mathlib.CategoryTheory.EqToHom

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
⊢ eqToHom ⋯ ≍ 𝟙 X

Tactic:
;

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
⊢ eqToHom ⋯ ≍ 𝟙 X