awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Category.Preorder
Goal:
X : Type u
inst : PartialOrder X
x y : X
f : x ≅ y
⊢ x = y

Tactic:
le_antisymm f.hom.le f.inv.le

Premises used: Quiver.Hom.le, le_antisymm, CategoryTheory.Iso.hom, CategoryTheory.Iso.inv
-- Module: Mathlib.CategoryTheory.Category.Preorder
Goal:
X : Type u
Y : Type v
inst : PartialOrder X
inst_1 : PartialOrder Y
e : X ≌ Y
x : X
⊢ (e.toOrderIso : (a : X) → Y) x = e.functor.obj x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Category.Preorder
Goal:
X : Type u
Y : Type v
inst : PartialOrder X
inst_1 : PartialOrder Y
e : X ≌ Y
y : Y
⊢ (e.toOrderIso.symm : (a : Y) → X) y = e.inverse.obj y

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Category.Preorder
Goal:
X : Type u
inst : PartialOrder X
a b : X
f : a ⟶ b
mp : IsIso f → a = b
mpr : a = b → IsIso f
⊢ IsIso f ↔ a = b

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Category.Preorder
Goal:
X : Type u
inst : PartialOrder X
a b : X
f : a ⟶ b
h : IsIso f
⊢ a = b

Tactic:
(asIso f).to_eq

Premises used: CategoryTheory.Iso.to_eq, CategoryTheory.asIso
-- Module: Mathlib.CategoryTheory.Category.Preorder
Goal:
X : Type u
inst : PartialOrder X
a b : X
f : a ⟶ b
h : IsIso f
⊢ a = b

Tactic:
exact (asIso f).to_eq

Premises used: CategoryTheory.Iso.to_eq, CategoryTheory.asIso
-- Module: Mathlib.CategoryTheory.Category.Preorder
Goal:
X : Type u
inst : PartialOrder X
a : X
f : a ⟶ a
mpr : IsIso (𝟙 a)
⊢ IsIso f

Tactic:
rw [Subsingleton.elim f (𝟙 _)]

Premises used: CategoryTheory.CategoryStruct.id, Subsingleton.elim
-- Module: Mathlib.CategoryTheory.Category.Preorder
Goal:
X : Type u
inst : PartialOrder X
a : X
f : a ⟶ a
⊢ IsIso (𝟙 a)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Category.Quiv
Goal:
X : Quiv
⊢ 𝟙 X = 𝟭q (↑X : Type u_2)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Category.Quiv
Goal:
X Y Z : Quiv
F : X ⟶ Y
G : Y ⟶ Z
⊢ F ≫ G = F ⋙q G

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Category.Quiv
Goal:
C D : Quiv
F : C ⟶ D
⊢ toQuivHom (ofQuivHom F) = F

Tactic:
rfl

Premises used: CategoryTheory.Prefunctor.ofQuivHom, CategoryTheory.Prefunctor.toQuivHom, rfl
-- Module: Mathlib.CategoryTheory.Category.Quiv
Goal:
C D : Type
inst : Quiver C
inst_1 : Quiver D
F : C ⥤q D
⊢ ofQuivHom (toQuivHom F) = F

Tactic:
rfl

Premises used: CategoryTheory.Prefunctor.ofQuivHom, CategoryTheory.Prefunctor.toQuivHom, rfl
-- Module: Mathlib.CategoryTheory.Category.Quiv
Goal:
V : Type u_1
inst : Quiver.{u_2, u_1} V
⊢ Eq (α := Paths V ⥤ Paths V) (freeMap (𝟭q V)) (𝟭 (Paths V))

Tactic:
Functor.ext_of_iso (freeMapIdIso V) (fun _ ↦ rfl)

Premises used: CategoryTheory.Cat.freeMapIdIso, CategoryTheory.Functor.ext_of_iso, rfl
-- Module: Mathlib.CategoryTheory.Category.Quiv
Goal:
V₁ : Type u₁
V₂ : Type u₂
V₃ : Type u₃
inst : Quiver.{v₁, u₁} V₁
inst_1 : Quiver.{v₂, u₂} V₂
inst_2 : Quiver.{v₃, u₃} V₃
F : Prefunctor.{v₁, v₂, u₁, u₂} V₁ V₂
G : Prefunctor.{v₂, v₃, u₂, u₃} V₂ V₃
X Y : Paths V₁
f : X ⟶ Y
dsimp :
  Eq (α := G.obj (F.obj X) ⟶ G.obj (F.obj Y)) ((F ⋙q G).mapPath f ≫ 𝟙 (G.obj (F.obj Y)))
    (𝟙 (G.obj (F.obj X)) ≫ G.mapPath (F.mapPath f))
⊢ (freeMap (F ⋙q G)).map f ≫
      Iso.hom
        ((fun (x : Paths V₁) ↦
            (Iso.refl ((freeMap (F ⋙q G)).obj x) : (freeMap (F ⋙q G)).obj x ≅ (freeMap (F ⋙q G)).obj x))
          Y) =
    Iso.hom
        ((fun (x : Paths V₁) ↦
            (Iso.refl ((freeMap (F ⋙q G)).obj x) : (freeMap (F ⋙q G)).obj x ≅ (freeMap (F ⋙q G)).obj x))
          X) ≫
      (freeMap F ⋙ freeMap G).map f

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Category.Quiv
Goal:
V₁ : Type u₁
V₂ : Type u₂
V₃ : Type u₃
inst : Quiver.{v₁, u₁} V₁
inst_1 : Quiver.{v₂, u₂} V₂
inst_2 : Quiver.{v₃, u₃} V₃
F : Prefunctor.{v₁, v₂, u₁, u₂} V₁ V₂
G : Prefunctor.{v₂, v₃, u₂, u₃} V₂ V₃
X Y : Paths V₁
f : X ⟶ Y
⊢ Eq (α := G.obj (F.obj X) ⟶ G.obj (F.obj Y)) ((F ⋙q G).mapPath f ≫ 𝟙 (G.obj (F.obj Y)))
    (𝟙 (G.obj (F.obj X)) ≫ G.mapPath (F.mapPath f))

Tactic:
simp only [Category.comp_id, Category.id_comp, Prefunctor.mapPath_comp_apply]

Premises used: CategoryTheory.Category.comp_id, Prefunctor.mapPath_comp_apply, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Category.Quiv
Goal:
V₁ : Type u₁
V₂ : Type u₂
V₃ : Type u₃
inst : Quiver.{v₁, u₁} V₁
inst_1 : Quiver.{v₂, u₂} V₂
inst_2 : Quiver.{v₃, u₃} V₃
F : Prefunctor.{v₁, v₂, u₁, u₂} V₁ V₂
G : Prefunctor.{v₂, v₃, u₂, u₃} V₂ V₃
⊢ freeMap (F ⋙q G) = freeMap F ⋙ freeMap G

Tactic:
Functor.ext_of_iso (freeMapCompIso F G) (fun _ ↦ rfl)

Premises used: CategoryTheory.Cat.freeMapCompIso, CategoryTheory.Functor.ext_of_iso, rfl
-- Module: Mathlib.CategoryTheory.Category.Quiv
Goal:
V W : Quiv
e : V ≅ W
X : (↑V : Type u_1)
⊢ e.inv.obj (e.hom.obj X) = X

Tactic:
(equivOfIso e).left_inv X

Premises used: CategoryTheory.Quiv.equivOfIso, Equiv.left_inv
-- Module: Mathlib.CategoryTheory.Category.Quiv
Goal:
V W : Quiv
e : V ≅ W
Y : (↑W : Type u_1)
⊢ e.hom.obj (e.inv.obj Y) = Y

Tactic:
(equivOfIso e).right_inv Y

Premises used: Equiv.right_inv, CategoryTheory.Quiv.equivOfIso
-- Module: Mathlib.CategoryTheory.Category.Quiv
Goal:
V_1 W_1 : Quiv
e_1 : V_1 ≅ W_1
V W : Quiv
e : V ≅ W
X Y : (↑W : Type u_2)
f : X ⟶ Y
⊢ X = e.hom.obj (e.inv.obj X)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Category.Quiv
Goal:
V_1 W_1 : Quiv
e_1 : V_1 ≅ W_1
V W : Quiv
e : V ≅ W
X Y : (↑W : Type u_2)
f : X ⟶ Y
⊢ Y = e.hom.obj (e.inv.obj Y)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Category.Quiv
Goal:
V W : Quiv
e : V ≅ W
X Y : (↑W : Type u_2)
f : X ⟶ Y
rw : (e.inv ⋙q e.hom).map f = Quiver.homOfEq f ⋯ ⋯
⊢ e.hom.map (e.inv.map f) = Quiver.homOfEq f ⋯ ⋯

Tactic:
rw [← Prefunctor.comp_map]

Premises used: Prefunctor.comp_map
-- Module: Mathlib.CategoryTheory.Category.Quiv
Goal:
V W : Quiv
e : V ≅ W
X Y : (↑W : Type u_2)
f : X ⟶ Y
⊢ (e.inv ⋙q e.hom).map f = Quiver.homOfEq f ⋯ ⋯

Tactic:
(Prefunctor.congr_hom e.inv_hom_id.symm f).symm

Premises used: CategoryTheory.Iso.inv_hom_id, Prefunctor.congr_hom, Eq.symm
-- Module: Mathlib.CategoryTheory.Category.Quiv
Goal:
V W : Quiv
e : V ≅ W
X Y : (↑W : Type u_2)
f : X ⟶ Y
⊢ (e.inv ⋙q e.hom).map f = Quiver.homOfEq f ⋯ ⋯

Tactic:
exact (Prefunctor.congr_hom e.inv_hom_id.symm f).symm

Premises used: CategoryTheory.Iso.inv_hom_id, Prefunctor.congr_hom, Eq.symm
-- Module: Mathlib.CategoryTheory.Category.Quiv
Goal:
V_1 W_1 : Quiv
e_1 : V_1 ≅ W_1
V W : Quiv
e : V ≅ W
X Y : (↑V : Type u_2)
f : X ⟶ Y
⊢ X = e.inv.obj (e.hom.obj X)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Category.Quiv
Goal:
V_1 W_1 : Quiv
e_1 : V_1 ≅ W_1
V W : Quiv
e : V ≅ W
X Y : (↑V : Type u_2)
f : X ⟶ Y
⊢ Y = e.inv.obj (e.hom.obj Y)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Category.Quiv
Goal:
V W : Quiv
e : V ≅ W
X Y : (↑V : Type u_2)
f : X ⟶ Y
⊢ e.inv.map (e.hom.map f) = Quiver.homOfEq f ⋯ ⋯

Tactic:
hom_map_inv_map_of_iso e.symm f

Premises used: CategoryTheory.Quiv.hom_map_inv_map_of_iso, CategoryTheory.Iso.symm
-- Module: Mathlib.CategoryTheory.Category.Quiv
Goal:
V_1 W_1 : Quiv
e_1 : V_1 ≅ W_1
V W : Quiv
e : V ≅ W
X Y : (↑V : Type u_2)
g : e.hom.obj X ⟶ e.hom.obj Y
⊢ e.inv.obj (e.hom.obj X) = X

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Category.Quiv
Goal:
V_1 W_1 : Quiv
e_1 : V_1 ≅ W_1
V W : Quiv
e : V ≅ W
X Y : (↑V : Type u_2)
g : e.hom.obj X ⟶ e.hom.obj Y
⊢ e.inv.obj (e.hom.obj Y) = Y

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Category.Quiv
Goal:
V_1 W_1 : Quiv
e_1 : V_1 ≅ W_1
V W : Quiv
e : V ≅ W
X Y : (↑V : Type u_2)
f : X ⟶ Y
⊢ (fun (g : e.hom.obj X ⟶ e.hom.obj Y) ↦ Quiver.homOfEq (e.inv.map g) ⋯ ⋯) ((fun (f : X ⟶ Y) ↦ e.hom.map f) f) = f

Tactic:
simp [inv_map_hom_map_of_iso]

Premises used: CategoryTheory.Quiv.inv_map_hom_map_of_iso
-- Module: Mathlib.CategoryTheory.Category.Quiv
Goal:
V_1 W_1 : Quiv
e_1 : V_1 ≅ W_1
V W : Quiv
e : V ≅ W
X Y : (↑V : Type u_2)
g : e.hom.obj X ⟶ e.hom.obj Y
⊢ (fun (f : X ⟶ Y) ↦ e.hom.map f) ((fun (g : e.hom.obj X ⟶ e.hom.obj Y) ↦ Quiver.homOfEq (e.inv.map g) ⋯ ⋯) g) = g

Tactic:
simp [hom_map_inv_map_of_iso]

Premises used: CategoryTheory.Quiv.hom_map_inv_map_of_iso
-- Module: Mathlib.CategoryTheory.Category.Quiv
Goal:
V W : Type u
inst : Quiver.{u_1, u} V
inst_1 : Quiver.{u_2, u} W
e : V ≃ W
he :
  (X Y : V) → Equiv.{u_1 + 1, u_2 + 1} (X ⟶ Y) (Quiver.Hom (V := W) ((e : (a : V) → W) X : W) ((e : (a : V) → W) Y : W))
X Y : V
f : X ⟶ Y
X' Y' : V
hX : X = X'
hY : Y = Y'
X'' Y'' : W
hX' : (e : (a : V) → W) X' = X''
hY' : (e : (a : V) → W) Y' = Y''
rw : (e : (a : V) → W) X' = X''
rw₁ rw₂ : X'' = X''
⊢ (e : (a : V) → W) X = X''

Tactic:
rw [hX, hX']
-- Module: Mathlib.CategoryTheory.Category.Quiv
Goal:
V W : Type u
inst : Quiver.{u_1, u} V
inst_1 : Quiver.{u_2, u} W
e : V ≃ W
he :
  (X Y : V) → Equiv.{u_1 + 1, u_2 + 1} (X ⟶ Y) (Quiver.Hom (V := W) ((e : (a : V) → W) X : W) ((e : (a : V) → W) Y : W))
X Y : V
f : X ⟶ Y
X' Y' : V
hX : X = X'
hY : Y = Y'
X'' Y'' : W
hX' : (e : (a : V) → W) X' = X''
hY' rw : (e : (a : V) → W) Y' = Y''
rw₁ rw₂ : Y'' = Y''
⊢ (e : (a : V) → W) Y = Y''

Tactic:
rw [hY, hY']
-- Module: Mathlib.CategoryTheory.Category.Quiv
Goal:
V W : Type u
inst : Quiver.{u_1, u} V
inst_1 : Quiver.{u_2, u} W
e : V ≃ W
he :
  (X Y : V) → Equiv.{u_1 + 1, u_2 + 1} (X ⟶ Y) (Quiver.Hom (V := W) ((e : (a : V) → W) X : W) ((e : (a : V) → W) Y : W))
X Y : V
f : X ⟶ Y
X' Y' : V
hX : X = X'
hY : Y = Y'
X'' Y'' : W
hX' : (e : (a : V) → W) X' = X''
hY' : (e : (a : V) → W) Y' = Y''
subst :
  Eq.{u_2 + 1} (α := Quiver.Hom (V := W) ((e : (a : V) → W) X : W) ((e : (a : V) → W) Y : W))
    (Quiver.homOfEq (X := (e : (a : V) → W) X) (Y := (e : (a : V) → W) Y)
        ((he X Y : (a : X ⟶ Y) → (e : (a : V) → W) X ⟶ (e : (a : V) → W) Y) (Quiver.homOfEq f ⋯ ⋯)) ⋯ ⋯ :
      Quiver.Hom (V := W) ((e : (a : V) → W) X : W) ((e : (a : V) → W) Y : W))
    (Quiver.homOfEq ((he X Y : (a : X ⟶ Y) → (e : (a : V) → W) X ⟶ (e : (a : V) → W) Y) f) ⋯ ⋯ :
      Quiver.Hom (V := W) ((e : (a : V) → W) X : W) ((e : (a : V) → W) Y : W))
⊢ Eq.{u_2 + 1} (α := X'' ⟶ Y'')
    (Quiver.homOfEq ((he X' Y' : (a : X' ⟶ Y') → (e : (a : V) → W) X' ⟶ (e : (a : V) → W) Y') (Quiver.homOfEq f hX hY))
        hX' hY' :
      X'' ⟶ Y'')
    (Quiver.homOfEq ((he X Y : (a : X ⟶ Y) → (e : (a : V) → W) X ⟶ (e : (a : V) → W) Y) f) ⋯ ⋯ : X'' ⟶ Y'')

Tactic:
subst hX hY hX' hY'
-- Module: Mathlib.CategoryTheory.Category.Quiv
Goal:
V W : Type u
inst : Quiver.{u_1, u} V
inst_1 : Quiver.{u_2, u} W
e : V ≃ W
he :
  (X Y : V) → Equiv.{u_1 + 1, u_2 + 1} (X ⟶ Y) (Quiver.Hom (V := W) ((e : (a : V) → W) X : W) ((e : (a : V) → W) Y : W))
X Y : V
f : X ⟶ Y
⊢ Eq.{u_2 + 1} (α := Quiver.Hom (V := W) ((e : (a : V) → W) X : W) ((e : (a : V) → W) Y : W))
    (Quiver.homOfEq (X := (e : (a : V) → W) X) (Y := (e : (a : V) → W) Y)
        ((he X Y : (a : X ⟶ Y) → (e : (a : V) → W) X ⟶ (e : (a : V) → W) Y) (Quiver.homOfEq f ⋯ ⋯)) ⋯ ⋯ :
      Quiver.Hom (V := W) ((e : (a : V) → W) X : W) ((e : (a : V) → W) Y : W))
    (Quiver.homOfEq ((he X Y : (a : X ⟶ Y) → (e : (a : V) → W) X ⟶ (e : (a : V) → W) Y) f) ⋯ ⋯ :
      Quiver.Hom (V := W) ((e : (a : V) → W) X : W) ((e : (a : V) → W) Y : W))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Category.Quiv
Goal:
V W : Type u
inst : Quiver.{u_1, u} V
inst_1 : Quiver.{u_1, u} W
e : V ≃ W
he : (X Y : V) → (X ⟶ Y) ≃ Quiver.Hom (V := W) ((e : (a : V) → W) X : W) ((e : (a : V) → W) Y : W)
X Y : (↑(of W) : Type u)
f : X ⟶ Y
⊢ X = (e : (a : V) → W) ((e.symm : (a : W) → V) X : V)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Category.Quiv
Goal:
V W : Type u
inst : Quiver.{u_1, u} V
inst_1 : Quiver.{u_1, u} W
e : V ≃ W
he : (X Y : V) → (X ⟶ Y) ≃ Quiver.Hom (V := W) ((e : (a : V) → W) X : W) ((e : (a : V) → W) Y : W)
X Y : (↑(of W) : Type u)
f : X ⟶ Y
⊢ Y = (e : (a : V) → W) ((e.symm : (a : W) → V) Y : V)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Category.Quiv
Goal:
V W : Type u
inst : Quiver.{u_1, u} V
inst_1 : Quiver.{u_1, u} W
e : V ≃ W
he : (X Y : V) → (X ⟶ Y) ≃ Quiver.Hom (V := W) ((e : (a : V) → W) X : W) ((e : (a : V) → W) Y : W)
X Y : (↑(of V) : Type u)
f : X ⟶ Y
dsimp :
  (Equiv.symm
          (he ((e.symm : (a : W) → V) ((e : (a : V) → W) X : W)) ((e.symm : (a : W) → V) ((e : (a : V) → W) Y : W))) :
        (a :
            (e : (a : V) → W) ((e.symm : (a : W) → V) ((e : (a : V) → W) X)) ⟶
              (e : (a : V) → W) ((e.symm : (a : W) → V) ((e : (a : V) → W) Y))) →
          (e.symm : (a : W) → V) ((e : (a : V) → W) X) ⟶ (e.symm : (a : W) → V) ((e : (a : V) → W) Y))
      (Quiver.homOfEq ((he X Y : (a : X ⟶ Y) → (e : (a : V) → W) X ⟶ (e : (a : V) → W) Y) f) ⋯ ⋯ :
        Quiver.Hom (V := W) ((e : (a : V) → W) ((e.symm : (a : W) → V) ((e : (a : V) → W) X : W) : V) : W)
          ((e : (a : V) → W) ((e.symm : (a : W) → V) ((e : (a : V) → W) Y : W) : V) : W)) =
    Quiver.homOfEq f ⋯ ⋯
⊢ Prefunctor.map
      (CategoryStruct.comp (Y := of W)
        { obj := (⇑e : (a : V) → W),
          map := fun {X Y : (↑(of V) : Type u)} ↦
            (⇑(he X Y) : (a : X ⟶ Y) → (e : (a : V) → W) X ⟶ (e : (a : V) → W) Y) }
        { obj := (⇑e.symm : (a : W) → V),
          map := fun {X Y : (↑(of W) : Type u)} (f : X ⟶ Y) ↦
            (Equiv.symm (he ((e.symm : (a : W) → V) X) ((e.symm : (a : W) → V) Y)) :
                (a : (e : (a : V) → W) ((e.symm : (a : W) → V) X) ⟶ (e : (a : V) → W) ((e.symm : (a : W) → V) Y)) →
                  (e.symm : (a : W) → V) X ⟶ (e.symm : (a : W) → V) Y)
              (Quiver.homOfEq f ⋯ ⋯) })
      f =
    Quiver.homOfEq (Prefunctor.map (𝟙 (of V)) f) ⋯ ⋯

Tactic:
dsimp [Quiv.id_eq_id, Quiv.comp_eq_comp]

Premises used: CategoryTheory.Quiv.comp_eq_comp, CategoryTheory.Quiv.id_eq_id
-- Module: Mathlib.CategoryTheory.Category.Quiv
Goal:
V W : Type u
inst : Quiver.{u_1, u} V
inst_1 : Quiver.{u_1, u} W
e : V ≃ W
he : (X Y : V) → (X ⟶ Y) ≃ Quiver.Hom (V := W) ((e : (a : V) → W) X : W) ((e : (a : V) → W) Y : W)
X Y : (↑(of V) : Type u)
f : X ⟶ Y
⊢ Eq (α := W) ((e : (a : V) → W) ((e.symm : (a : W) → V) ((e : (a : V) → W) X : W) : V) : W) ((e : (a : V) → W) X : W)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Category.Quiv
Goal:
V W : Type u
inst : Quiver.{u_1, u} V
inst_1 : Quiver.{u_1, u} W
e : V ≃ W
he : (X Y : V) → (X ⟶ Y) ≃ Quiver.Hom (V := W) ((e : (a : V) → W) X : W) ((e : (a : V) → W) Y : W)
X Y : (↑(of V) : Type u)
f : X ⟶ Y
⊢ Eq (α := W) ((e : (a : V) → W) ((e.symm : (a : W) → V) ((e : (a : V) → W) Y : W) : V) : W) ((e : (a : V) → W) Y : W)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Category.Quiv
Goal:
V W : Type u
inst : Quiver.{u_1, u} V
inst_1 : Quiver.{u_1, u} W
e : V ≃ W
he : (X Y : V) → (X ⟶ Y) ≃ Quiver.Hom (V := W) ((e : (a : V) → W) X : W) ((e : (a : V) → W) Y : W)
X Y : (↑(of V) : Type u)
f : X ⟶ Y
⊢ Eq (α := Quiver.Hom (V := W) ((e : (a : V) → W) X : W) ((e : (a : V) → W) Y : W))
    (Quiver.homOfEq (X := (e : (a : V) → W) ((e.symm : (a : W) → V) ((e : (a : V) → W) X : W) : V)) (Y :=
        (e : (a : V) → W) ((e.symm : (a : W) → V) ((e : (a : V) → W) Y : W) : V))
        ((he ((e.symm : (a : W) → V) ((e : (a : V) → W) X : W)) ((e.symm : (a : W) → V) ((e : (a : V) → W) Y : W)) :
            (a : (e.symm : (a : W) → V) ((e : (a : V) → W) X) ⟶ (e.symm : (a : W) → V) ((e : (a : V) → W) Y)) →
              (e : (a : V) → W) ((e.symm : (a : W) → V) ((e : (a : V) → W) X)) ⟶
                (e : (a : V) → W) ((e.symm : (a : W) → V) ((e : (a : V) → W) Y)))
          ((Equiv.symm
                  (he ((e.symm : (a : W) → V) ((e : (a : V) → W) X : W))
                    ((e.symm : (a : W) → V) ((e : (a : V) → W) Y : W))) :
                (a :
                    (e : (a : V) → W) ((e.symm : (a : W) → V) ((e : (a : V) → W) X)) ⟶
                      (e : (a : V) → W) ((e.symm : (a : W) → V) ((e : (a : V) → W) Y))) →
                  (e.symm : (a : W) → V) ((e : (a : V) → W) X) ⟶ (e.symm : (a : W) → V) ((e : (a : V) → W) Y))
              (Quiver.homOfEq ((he X Y : (a : X ⟶ Y) → (e : (a : V) → W) X ⟶ (e : (a : V) → W) Y) f) ⋯ ⋯ :
                Quiver.Hom (V := W) ((e : (a : V) → W) ((e.symm : (a : W) → V) ((e : (a : V) → W) X : W) : V) : W)
                  ((e : (a : V) → W) ((e.symm : (a : W) → V) ((e : (a : V) → W) Y : W) : V) : W)) :
            Quiver.Hom (V := V) ((e.symm : (a : W) → V) ((e : (a : V) → W) X : W) : V)
              ((e.symm : (a : W) → V) ((e : (a : V) → W) Y : W) : V)))
        ⋯ ⋯ :
      Quiver.Hom (V := W) ((e : (a : V) → W) X : W) ((e : (a : V) → W) Y : W))
    (Quiver.homOfEq (X := (e : (a : V) → W) ((e.symm : (a : W) → V) ((e : (a : V) → W) X : W) : V)) (Y :=
        (e : (a : V) → W) ((e.symm : (a : W) → V) ((e : (a : V) → W) Y : W) : V))
        ((he ((e.symm : (a : W) → V) ((e : (a : V) → W) X : W)) ((e.symm : (a : W) → V) ((e : (a : V) → W) Y : W)) :
            (a : (e.symm : (a : W) → V) ((e : (a : V) → W) X) ⟶ (e.symm : (a : W) → V) ((e : (a : V) → W) Y)) →
              (e : (a : V) → W) ((e.symm : (a : W) → V) ((e : (a : V) → W) X)) ⟶
                (e : (a : V) → W) ((e.symm : (a : W) → V) ((e : (a : V) → W) Y)))
          (Quiver.homOfEq f ⋯ ⋯))
        ⋯ ⋯ :
      Quiver.Hom (V := W) ((e : (a : V) → W) X : W) ((e : (a : V) → W) Y : W))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Category.Quiv
Goal:
V W : Type u
inst : Quiver.{u_1, u} V
inst_1 : Quiver.{u_1, u} W
e : V ≃ W
he : (X Y : V) → (X ⟶ Y) ≃ Quiver.Hom (V := W) ((e : (a : V) → W) X : W) ((e : (a : V) → W) Y : W)
⊢ ∀ (X Y : (↑(of W) : Type u)) (f : X ⟶ Y),
    Prefunctor.map
        (CategoryStruct.comp (Y := of V)
          { obj := (⇑e.symm : (a : W) → V),
            map := fun {X Y : (↑(of W) : Type u)} (f : X ⟶ Y) ↦
              (Equiv.symm (he ((e.symm : (a : W) → V) X) ((e.symm : (a : W) → V) Y)) :
                  (a : (e : (a : V) → W) ((e.symm : (a : W) → V) X) ⟶ (e : (a : V) → W) ((e.symm : (a : W) → V) Y)) →
                    (e.symm : (a : W) → V) X ⟶ (e.symm : (a : W) → V) Y)
                (Quiver.homOfEq f ⋯ ⋯) }
          { obj := (⇑e : (a : V) → W),
            map := fun {X Y : (↑(of V) : Type u)} ↦
              (⇑(he X Y) : (a : X ⟶ Y) → (e : (a : V) → W) X ⟶ (e : (a : V) → W) Y) })
        f =
      Quiver.homOfEq (Prefunctor.map (𝟙 (of W)) f) ⋯ ⋯

Tactic:
simp [Quiv.id_eq_id, Quiv.comp_eq_comp]

Premises used: CategoryTheory.Quiv.comp_eq_comp, CategoryTheory.Quiv.id_eq_id
-- Module: Mathlib.CategoryTheory.Category.Quiv
Goal:
C : Type u
D : Type u₁
inst : Category.{v, u} C
inst_1 : Category.{v₁, u₁} D
F : Functor.{v, v₁, u, u₁} C D
⊢ ∀ {X Y : C} (f : X ⟶ Y),
    (Cat.freeMap F.toPrefunctor ⋙ pathComposition D).map f.toPath ≫
        Iso.hom
          ((fun (x : C) ↦
              (Iso.refl ((Cat.freeMap F.toPrefunctor ⋙ pathComposition D).obj x) :
                (Cat.freeMap F.toPrefunctor ⋙ pathComposition D).obj x ≅
                  (Cat.freeMap F.toPrefunctor ⋙ pathComposition D).obj x))
            Y) =
      Iso.hom
          ((fun (x : C) ↦
              (Iso.refl ((Cat.freeMap F.toPrefunctor ⋙ pathComposition D).obj x) :
                (Cat.freeMap F.toPrefunctor ⋙ pathComposition D).obj x ≅
                  (Cat.freeMap F.toPrefunctor ⋙ pathComposition D).obj x))
            X) ≫
        (pathComposition C ⋙ F).map f.toPath

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Category.Quiv
Goal:
C : Type u
D : Type u₁
inst : Category.{v, u} C
inst_1 : Category.{v₁, u₁} D
F : Functor.{v, v₁, u, u₁} C D
⊢ ∀ (a b : C) (e : a ⟶ b),
    (Cat.freeMap F.toPrefunctor ⋙ pathComposition D).map e.toPath =
      eqToHom ⋯ ≫ (pathComposition C ⋙ F).map e.toPath ≫ eqToHom ⋯

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Category.Quiv
Goal:
V : Type u
W : Type u₁
inst : Quiver.{v, u} V
inst_1 : Quiver.{v₁, u₁} W
F : Prefunctor.{v, v₁, u, u₁} V W
⊢ Paths.of V ⋙q (Cat.freeMap F).toPrefunctor = F ⋙q Paths.of W

Tactic:
rfl

Premises used: CategoryTheory.Paths, Prefunctor.comp, Quiver.Hom.toPath, CategoryTheory.Paths.of, Prefunctor.mapPath, rfl
-- Module: Mathlib.CategoryTheory.Category.Quiv
Goal:
V : Type u
inst : Quiver.{v, u} V
⊢ ∀ {X Y : V} (f : X ⟶ Y),
    Eq (α := Functor.obj (Cat.freeMap (Paths.of V) ⋙ pathComposition (Paths V)) X ⟶ Functor.obj (𝟭 (Paths V)) Y)
      (Functor.map (Cat.freeMap (Paths.of V) ⋙ pathComposition (Paths V)) f.toPath ≫
        Iso.hom
          ((fun (v : V) ↦
              (Iso.refl (Functor.obj (Cat.freeMap (Paths.of V) ⋙ pathComposition (Paths V)) v) :
                Functor.obj (Cat.freeMap (Paths.of V) ⋙ pathComposition (Paths V)) v ≅
                  Functor.obj (Cat.freeMap (Paths.of V) ⋙ pathComposition (Paths V)) v))
            Y))
      (CategoryStruct.comp (Y := Functor.obj (𝟭 (Paths V)) X)
        (Iso.hom
          ((fun (v : V) ↦
              (Iso.refl (Functor.obj (Cat.freeMap (Paths.of V) ⋙ pathComposition (Paths V)) v) :
                Functor.obj (Cat.freeMap (Paths.of V) ⋙ pathComposition (Paths V)) v ≅
                  Functor.obj (Cat.freeMap (Paths.of V) ⋙ pathComposition (Paths V)) v))
            X))
        (Functor.map (𝟭 (Paths V)) f.toPath))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Category.Quiv
Goal:
V : Type u
inst : Quiver.{v, u} V
⊢ ∀ (a b : V) (e : a ⟶ b),
    Eq (α :=
      Functor.obj (Cat.freeMap (Paths.of V) ⋙ pathComposition (Paths V)) a ⟶
        Functor.obj (Cat.freeMap (Paths.of V) ⋙ pathComposition (Paths V)) b)
      (Functor.map (Cat.freeMap (Paths.of V) ⋙ pathComposition (Paths V)) e.toPath)
      (eqToHom ⋯ ≫ Functor.map (𝟭 (Paths V)) e.toPath ≫ eqToHom ⋯)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Category.Quiv
Goal:
C : Type u
inst : Category.{v, u} C
e_map :
  Eq (α :=
    {X Y : C} →
      (X ⟶ Y) →
        (Prefunctor.obj (Functor.toPrefunctor (pathComposition C)) (Prefunctor.obj (Paths.of C) X) ⟶
          Prefunctor.obj (Functor.toPrefunctor (pathComposition C)) (Prefunctor.obj (Paths.of C) Y)))
    (fun {X Y : C} (f : X ⟶ Y) ↦
      Prefunctor.map (Functor.toPrefunctor (pathComposition C)) (Prefunctor.map (Paths.of C) f))
    fun {X Y : C} (f : X ⟶ Y) ↦ f
⊢ Eq (α := Prefunctor.{v, v, u, u} C C)
    { obj := fun (X : C) ↦ Prefunctor.obj (Functor.toPrefunctor (pathComposition C)) (Prefunctor.obj (Paths.of C) X),
      map := fun {X Y : C} (f : X ⟶ Y) ↦
        Prefunctor.map (Functor.toPrefunctor (pathComposition C)) (Prefunctor.map (Paths.of C) f) }
    (𝟭q C)

Tactic:
congr
-- Module: Mathlib.CategoryTheory.Category.Quiv
Goal:
C : Type u
inst : Category.{v, u} C
e_map :
  ∀ (X Y : C) (f : X ⟶ Y), Prefunctor.map (Functor.toPrefunctor (pathComposition C)) (Prefunctor.map (Paths.of C) f) = f
⊢ Eq (α :=
    {X Y : C} →
      (X ⟶ Y) →
        (Prefunctor.obj (Functor.toPrefunctor (pathComposition C)) (Prefunctor.obj (Paths.of C) X) ⟶
          Prefunctor.obj (Functor.toPrefunctor (pathComposition C)) (Prefunctor.obj (Paths.of C) Y)))
    (fun {X Y : C} (f : X ⟶ Y) ↦
      Prefunctor.map (Functor.toPrefunctor (pathComposition C)) (Prefunctor.map (Paths.of C) f))
    fun {X Y : C} (f : X ⟶ Y) ↦ f

Tactic:
funext X Y f
-- Module: Mathlib.CategoryTheory.Category.Quiv
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
⊢ Prefunctor.map (Functor.toPrefunctor (pathComposition C)) (Prefunctor.map (Paths.of C) f) = f

Tactic:
Category.id_comp _

Premises used: CategoryTheory.composePath, Quiver.Hom.toPath, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Category.Quiv
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
⊢ Prefunctor.map (Functor.toPrefunctor (pathComposition C)) (Prefunctor.map (Paths.of C) f) = f

Tactic:
exact Category.id_comp _

Premises used: CategoryTheory.Category.id_comp