awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Category.Quiv
Goal:
w :
  ∀ (V : Quiv),
    Cat.Hom.toFunctor
        (NatTrans.app
          (Functor.whiskerRight
              { app := fun (x : Quiv) ↦ Paths.of (↑(Functor.obj (𝟭 Quiv) x) : Type u_2), naturality := adj._proof_1 }
              Cat.free ≫
            (Cat.free.associator forget Cat.free).hom ≫
              Cat.free.whiskerLeft
                { app := fun (C : Cat) ↦ Functor.toCatHom (pathComposition (↑C : Type u_2)), naturality := ⋯ :
                  NatTrans (forget ⋙ Cat.free) (𝟭 Cat) })
          V) =
      ((NatTrans.id (𝟭 Quiv ⋙ Cat.free)).app V).toFunctor
⊢ Functor.whiskerRight
        { app := fun (x : Quiv) ↦ Paths.of (↑(Functor.obj (𝟭 Quiv) x) : Type u_2), naturality := adj._proof_1 }
        Cat.free ≫
      (Cat.free.associator forget Cat.free).hom ≫
        Cat.free.whiskerLeft
          { app := fun (C : Cat) ↦ Functor.toCatHom (pathComposition (↑C : Type u_2)), naturality := ⋯ :
            NatTrans (forget ⋙ Cat.free) (𝟭 Cat) } =
    NatTrans.id (𝟭 Quiv ⋙ Cat.free)

Tactic:
ext V
-- Module: Mathlib.CategoryTheory.Category.Quiv
Goal:
V : Quiv
⊢ Cat.Hom.toFunctor
      (NatTrans.app
        (Functor.whiskerRight
            { app := fun (x : Quiv) ↦ Paths.of (↑(Functor.obj (𝟭 Quiv) x) : Type u_2), naturality := adj._proof_1 }
            Cat.free ≫
          (Cat.free.associator forget Cat.free).hom ≫
            Cat.free.whiskerLeft
              { app := fun (C : Cat) ↦ Functor.toCatHom (pathComposition (↑C : Type u_2)), naturality := ⋯ :
                NatTrans (forget ⋙ Cat.free) (𝟭 Cat) })
        V) =
    ((NatTrans.id (𝟭 Quiv ⋙ Cat.free)).app V).toFunctor

Tactic:
freeMap_pathsOf_pathComposition V

Premises used: CategoryTheory.Paths, CategoryTheory.Functor.comp, CategoryTheory.Functor.id, CategoryTheory.Quiv.freeMap_pathsOf_pathComposition, CategoryTheory.Bundled.α, CategoryTheory.Quiv, CategoryTheory.Prefunctor.ofQuivHom, CategoryTheory.Paths.of
-- Module: Mathlib.CategoryTheory.Category.Quiv
Goal:
V : Quiv
⊢ Cat.Hom.toFunctor
      (NatTrans.app
        (Functor.whiskerRight
            { app := fun (x : Quiv) ↦ Paths.of (↑(Functor.obj (𝟭 Quiv) x) : Type u_2), naturality := adj._proof_1 }
            Cat.free ≫
          (Cat.free.associator forget Cat.free).hom ≫
            Cat.free.whiskerLeft
              { app := fun (C : Cat) ↦ Functor.toCatHom (pathComposition (↑C : Type u_2)), naturality := ⋯ :
                NatTrans (forget ⋙ Cat.free) (𝟭 Cat) })
        V) =
    ((NatTrans.id (𝟭 Quiv ⋙ Cat.free)).app V).toFunctor

Tactic:
exact freeMap_pathsOf_pathComposition V

Premises used: CategoryTheory.Quiv.freeMap_pathsOf_pathComposition, CategoryTheory.Bundled.α
-- Module: Mathlib.CategoryTheory.Category.Quiv
Goal:
w :
  ∀ (C : Cat),
    NatTrans.app
        (forget.whiskerLeft
            { app := fun (x : Quiv) ↦ Paths.of (↑(Functor.obj (𝟭 Quiv) x) : Type u_2), naturality := adj._proof_1 } ≫
          (forget.associator Cat.free forget).inv ≫
            Functor.whiskerRight
              { app := fun (C : Cat) ↦ Functor.toCatHom (pathComposition (↑C : Type u_2)), naturality := ⋯ :
                NatTrans (forget ⋙ Cat.free) (𝟭 Cat) }
              forget)
        C =
      (NatTrans.id (forget ⋙ 𝟭 Quiv)).app C
⊢ forget.whiskerLeft
        { app := fun (x : Quiv) ↦ Paths.of (↑(Functor.obj (𝟭 Quiv) x) : Type u_2), naturality := adj._proof_1 } ≫
      (forget.associator Cat.free forget).inv ≫
        Functor.whiskerRight
          { app := fun (C : Cat) ↦ Functor.toCatHom (pathComposition (↑C : Type u_2)), naturality := ⋯ :
            NatTrans (forget ⋙ Cat.free) (𝟭 Cat) }
          forget =
    NatTrans.id (forget ⋙ 𝟭 Quiv)

Tactic:
ext C
-- Module: Mathlib.CategoryTheory.Category.Quiv
Goal:
C : Cat
⊢ NatTrans.app
      (forget.whiskerLeft
          { app := fun (x : Quiv) ↦ Paths.of (↑(Functor.obj (𝟭 Quiv) x) : Type u_2), naturality := adj._proof_1 } ≫
        (forget.associator Cat.free forget).inv ≫
          Functor.whiskerRight
            { app := fun (C : Cat) ↦ Functor.toCatHom (pathComposition (↑C : Type u_2)), naturality := ⋯ :
              NatTrans (forget ⋙ Cat.free) (𝟭 Cat) }
            forget)
      C =
    (NatTrans.id (forget ⋙ 𝟭 Quiv)).app C

Tactic:
pathsOf_pathComposition_toPrefunctor C

Premises used: CategoryTheory.composePath, CategoryTheory.Quiv.pathsOf_pathComposition_toPrefunctor, Prefunctor.id, Prefunctor.comp, CategoryTheory.Cat, CategoryTheory.Bundled.α, Quiver.Hom.toPath
-- Module: Mathlib.CategoryTheory.Category.Quiv
Goal:
C : Cat
⊢ NatTrans.app
      (forget.whiskerLeft
          { app := fun (x : Quiv) ↦ Paths.of (↑(Functor.obj (𝟭 Quiv) x) : Type u_2), naturality := adj._proof_1 } ≫
        (forget.associator Cat.free forget).inv ≫
          Functor.whiskerRight
            { app := fun (C : Cat) ↦ Functor.toCatHom (pathComposition (↑C : Type u_2)), naturality := ⋯ :
              NatTrans (forget ⋙ Cat.free) (𝟭 Cat) }
            forget)
      C =
    (NatTrans.id (forget ⋙ 𝟭 Quiv)).app C

Tactic:
exact pathsOf_pathComposition_toPrefunctor C

Premises used: CategoryTheory.Quiv.pathsOf_pathComposition_toPrefunctor, CategoryTheory.Bundled.α
-- Module: Mathlib.CategoryTheory.Category.Quiv
Goal:
V : Type u
C : Type u₁
inst : Quiver.{v, u} V
inst_1 : Category.{v₁, u₁} C
F : Paths V ⥤ C
rw : (Cat.freeMap (Paths.of V) ⋙ Cat.freeMap F.toPrefunctor) ⋙ pathComposition C = F
rw₁ : Cat.freeMap (Paths.of V) ⋙ Cat.freeMap F.toPrefunctor ⋙ pathComposition C = F
rw₂ : Cat.freeMap (Paths.of V) ⋙ pathComposition (Paths V) ⋙ F = F
rw₃ : (Cat.freeMap (Paths.of V) ⋙ pathComposition (Paths V)) ⋙ F = F
rw₄ : 𝟭 (Paths V) ⋙ F = F
rw₅ rw₆ : F = F
⊢ Cat.freeMap (Paths.of V ⋙q F.toPrefunctor) ⋙ pathComposition C = F

Tactic:
rw [Cat.freeMap_comp, Functor.assoc, pathComposition_naturality, ← Functor.assoc,
      freeMap_pathsOf_pathComposition, Functor.id_comp]

Premises used: CategoryTheory.Functor.assoc, CategoryTheory.Cat.freeMap_comp, CategoryTheory.Quiv.pathComposition_naturality, CategoryTheory.Quiv.freeMap_pathsOf_pathComposition, CategoryTheory.Functor.id_comp
-- Module: Mathlib.CategoryTheory.Category.Quiv
Goal:
V : Type u
C : Type u₁
inst : Quiver.{v, u} V
inst_1 : Category.{v₁, u₁} C
G : Prefunctor.{v, v₁, u, u₁} V C
rw : Paths.of V ⋙q ((Cat.freeMap G).toPrefunctor ⋙q Functor.toPrefunctor (pathComposition C)) = G
rw₁ : Paths.of V ⋙q (Cat.freeMap G).toPrefunctor ⋙q Functor.toPrefunctor (pathComposition C) = G
rw₂ : G ⋙q Paths.of C ⋙q Functor.toPrefunctor (pathComposition C) = G
rw₃ : G ⋙q (Paths.of C ⋙q Functor.toPrefunctor (pathComposition C)) = G
rw₄ : G ⋙q 𝟭q C = G
rw₅ rw₆ : G = G
⊢ Paths.of V ⋙q (Cat.freeMap G ⋙ pathComposition C).toPrefunctor = G

Tactic:
rw [← Functor.toPrefunctor_comp, ← Prefunctor.comp_assoc,
      pathsOf_freeMap_toPrefunctor, Prefunctor.comp_assoc,
      pathsOf_pathComposition_toPrefunctor, Prefunctor.comp_id]

Premises used: CategoryTheory.Quiv.pathsOf_pathComposition_toPrefunctor, Prefunctor.comp_assoc, CategoryTheory.Functor.toPrefunctor_comp, Prefunctor.comp_id, CategoryTheory.Quiv.pathsOf_freeMap_toPrefunctor
-- Module: Mathlib.CategoryTheory.Category.Quiv
Goal:
V C : Type u
inst : Quiver V
inst_1 : Category.{max u v, u} C
⊢ Eq (α := (Cat.free.obj (of V) ⟶ Cat.of C) ≃ (of V ⟶ forget.obj (Cat.of C))) (adj.homEquiv (of V) (Cat.of C))
    (Equiv.trans (Cat.Hom.equivFunctor (Cat.of (Paths V)) (Cat.of C)) pathsEquiv)

Tactic:
rfl

Premises used: Equiv.trans, CategoryTheory.Paths, CategoryTheory.Functor.toCatHom, CategoryTheory.Functor.comp, CategoryTheory.Cat.of, Prefunctor.comp, CategoryTheory.Bundled.of, CategoryTheory.Prefunctor.ofQuivHom, rfl
-- Module: Mathlib.CategoryTheory.Category.ReflQuiv
Goal:
C : Type u
inst : ReflQuiver.{u_1, u} C
⊢ (↑(of C) : Type u) = C

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Category.ReflQuiv
Goal:
X : ReflQuiv
⊢ 𝟙 X = 𝟭rq (↑X : Type u_2)

Tactic:
rfl

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

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Category.ReflQuiv
Goal:
X : ReflQuiv
x : (↑X : Type u_2)
⊢ (ReflPrefunctor.toPrefunctor (𝟙 X)).obj x = x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Category.ReflQuiv
Goal:
X : ReflQuiv
x y : (↑X : Type u_2)
f : x ⟶ y
⊢ (ReflPrefunctor.toPrefunctor (𝟙 X)).map f = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Category.ReflQuiv
Goal:
X Y Z : ReflQuiv
f : X ⟶ Y
g : Y ⟶ Z
x : (↑X : Type u_2)
⊢ (f ≫ g).obj x = g.obj (f.obj x)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Category.ReflQuiv
Goal:
X Y Z : ReflQuiv
f : X ⟶ Y
g : Y ⟶ Z
x y : (↑X : Type u_2)
a : x ⟶ y
⊢ (f ≫ g).map a = g.map (f.map a)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Category.ReflQuiv
Goal:
C D : Cat
F G : Functor.{v, v, u, u} (↑C : Type u) (↑D : Type u)
hyp : forget.map F.toCatHom = forget.map G.toCatHom
mk :
  ∀ (obj : (↑C : Type u) → (↑D : Type u)) (map : {X Y : (↑C : Type u)} → (X ⟶ Y) → (obj X ⟶ obj Y))
    (map_id : ∀ (X : (↑C : Type u)), map (𝟙 X) = 𝟙 (obj X))
    (map_comp : ∀ {X Y Z : (↑C : Type u)} (f : X ⟶ Y) (g : Y ⟶ Z), map (f ≫ g) = map f ≫ map g)
    (hyp :
      forget.map
          { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp :
              Functor.{v, v, u, u} (↑C : Type u) (↑D : Type u) }.toCatHom =
        forget.map G.toCatHom),
    { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp :
        Functor.{v, v, u, u} (↑C : Type u) (↑D : Type u) } =
      G
⊢ F = G

Tactic:
cases F
-- Module: Mathlib.CategoryTheory.Category.ReflQuiv
Goal:
C D : Cat
G : Functor.{v, v, u, u} (↑C : Type u) (↑D : Type u)
obj : (↑C : Type u) → (↑D : Type u)
map : {X Y : (↑C : Type u)} → (X ⟶ Y) → (obj X ⟶ obj Y)
map_id : ∀ (X : (↑C : Type u)), map (𝟙 X) = 𝟙 (obj X)
map_comp : ∀ {X Y Z : (↑C : Type u)} (f : X ⟶ Y) (g : Y ⟶ Z), map (f ≫ g) = map f ≫ map g
hyp :
  forget.map
      { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp :
          Functor.{v, v, u, u} (↑C : Type u) (↑D : Type u) }.toCatHom =
    forget.map G.toCatHom
mk :
  ∀ (obj_1 : (↑C : Type u) → (↑D : Type u)) (map_1 : {X Y : (↑C : Type u)} → (X ⟶ Y) → (obj_1 X ⟶ obj_1 Y))
    (map_id_1 : ∀ (X : (↑C : Type u)), map_1 (𝟙 X) = 𝟙 (obj_1 X))
    (map_comp_1 : ∀ {X Y Z : (↑C : Type u)} (f : X ⟶ Y) (g : Y ⟶ Z), map_1 (f ≫ g) = map_1 f ≫ map_1 g)
    (hyp :
      forget.map
          { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp :
              Functor.{v, v, u, u} (↑C : Type u) (↑D : Type u) }.toCatHom =
        forget.map { obj := obj_1, map := @map_1, map_id := map_id_1, map_comp := @map_comp_1 }.toCatHom),
    { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp :
        Functor.{v, v, u, u} (↑C : Type u) (↑D : Type u) } =
      { obj := obj_1, map := @map_1, map_id := map_id_1, map_comp := @map_comp_1 }
⊢ { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp :
      Functor.{v, v, u, u} (↑C : Type u) (↑D : Type u) } =
    G

Tactic:
cases G
-- Module: Mathlib.CategoryTheory.Category.ReflQuiv
Goal:
C D : Cat
obj : (↑C : Type u) → (↑D : Type u)
map : {X Y : (↑C : Type u)} → (X ⟶ Y) → (obj X ⟶ obj Y)
map_id : ∀ (X : (↑C : Type u)), map (𝟙 X) = 𝟙 (obj X)
map_comp : ∀ {X Y Z : (↑C : Type u)} (f : X ⟶ Y) (g : Y ⟶ Z), map (f ≫ g) = map f ≫ map g
obj_1 : (↑C : Type u) → (↑D : Type u)
map_1 : {X Y : (↑C : Type u)} → (X ⟶ Y) → (obj_1 X ⟶ obj_1 Y)
map_id_1 : ∀ (X : (↑C : Type u)), map_1 (𝟙 X) = 𝟙 (obj_1 X)
map_comp_1 : ∀ {X Y Z : (↑C : Type u)} (f : X ⟶ Y) (g : Y ⟶ Z), map_1 (f ≫ g) = map_1 f ≫ map_1 g
hyp :
  forget.map
      { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp :
          Functor.{v, v, u, u} (↑C : Type u) (↑D : Type u) }.toCatHom =
    forget.map { obj := obj_1, map := @map_1, map_id := map_id_1, map_comp := @map_comp_1 }.toCatHom
mk :
  ∀ (map_id_2 : ∀ (X : (↑C : Type u)), map (𝟙 X) = 𝟙 (obj X))
    (map_comp_2 : ∀ {X Y Z : (↑C : Type u)} (f : X ⟶ Y) (g : Y ⟶ Z), map (f ≫ g) = map f ≫ map g),
    { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp :
        Functor.{v, v, u, u} (↑C : Type u) (↑D : Type u) } =
      { obj := obj, map := @map, map_id := map_id_2, map_comp := @map_comp_2 }
⊢ { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp :
      Functor.{v, v, u, u} (↑C : Type u) (↑D : Type u) } =
    { obj := obj_1, map := @map_1, map_id := map_id_1, map_comp := @map_comp_1 }

Tactic:
cases hyp
-- Module: Mathlib.CategoryTheory.Category.ReflQuiv
Goal:
C D : Cat
obj : (↑C : Type u) → (↑D : Type u)
map : {X Y : (↑C : Type u)} → (X ⟶ Y) → (obj X ⟶ obj Y)
map_id : ∀ (X : (↑C : Type u)), map (𝟙 X) = 𝟙 (obj X)
map_comp : ∀ {X Y Z : (↑C : Type u)} (f : X ⟶ Y) (g : Y ⟶ Z), map (f ≫ g) = map f ≫ map g
map_id_1 : ∀ (X : (↑C : Type u)), map (𝟙 X) = 𝟙 (obj X)
map_comp_1 : ∀ {X Y Z : (↑C : Type u)} (f : X ⟶ Y) (g : Y ⟶ Z), map (f ≫ g) = map f ≫ map g
⊢ { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp :
      Functor.{v, v, u, u} (↑C : Type u) (↑D : Type u) } =
    { obj := obj, map := @map, map_id := map_id_1, map_comp := @map_comp_1 }

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Category.ReflQuiv
Goal:
V W : ReflQuiv
F G : ReflPrefunctor.{u_1, u_1, u_2, u_2} (↑V : Type u_2) (↑W : Type u_2)
hyp : forgetToQuiv.map F = forgetToQuiv.map G
mk :
  ∀ (toPrefunctor : Prefunctor.{u_1, u_1, u_2, u_2} (↑V : Type u_2) (↑W : Type u_2))
    (map_id : ∀ (X : (↑V : Type u_2)), toPrefunctor.map (𝟙rq X) = 𝟙rq (toPrefunctor.obj X))
    (hyp :
      forgetToQuiv.map
          { toPrefunctor := toPrefunctor, map_id := map_id :
            ReflPrefunctor.{u_1, u_1, u_2, u_2} (↑V : Type u_2) (↑W : Type u_2) } =
        forgetToQuiv.map G),
    { toPrefunctor := toPrefunctor, map_id := map_id :
        ReflPrefunctor.{u_1, u_1, u_2, u_2} (↑V : Type u_2) (↑W : Type u_2) } =
      G
⊢ F = G

Tactic:
cases F
-- Module: Mathlib.CategoryTheory.Category.ReflQuiv
Goal:
V W : ReflQuiv
G : ReflPrefunctor.{u_1, u_1, u_2, u_2} (↑V : Type u_2) (↑W : Type u_2)
toPrefunctor : Prefunctor.{u_1, u_1, u_2, u_2} (↑V : Type u_2) (↑W : Type u_2)
map_id : ∀ (X : (↑V : Type u_2)), toPrefunctor.map (𝟙rq X) = 𝟙rq (toPrefunctor.obj X)
hyp :
  forgetToQuiv.map
      { toPrefunctor := toPrefunctor, map_id := map_id :
        ReflPrefunctor.{u_1, u_1, u_2, u_2} (↑V : Type u_2) (↑W : Type u_2) } =
    forgetToQuiv.map G
mk :
  ∀ (toPrefunctor_1 : Prefunctor.{u_1, u_1, u_2, u_2} (↑V : Type u_2) (↑W : Type u_2))
    (map_id_1 : ∀ (X : (↑V : Type u_2)), toPrefunctor_1.map (𝟙rq X) = 𝟙rq (toPrefunctor_1.obj X))
    (hyp :
      forgetToQuiv.map
          { toPrefunctor := toPrefunctor, map_id := map_id :
            ReflPrefunctor.{u_1, u_1, u_2, u_2} (↑V : Type u_2) (↑W : Type u_2) } =
        forgetToQuiv.map { toPrefunctor := toPrefunctor_1, map_id := map_id_1 }),
    { toPrefunctor := toPrefunctor, map_id := map_id :
        ReflPrefunctor.{u_1, u_1, u_2, u_2} (↑V : Type u_2) (↑W : Type u_2) } =
      { toPrefunctor := toPrefunctor_1, map_id := map_id_1 }
⊢ { toPrefunctor := toPrefunctor, map_id := map_id :
      ReflPrefunctor.{u_1, u_1, u_2, u_2} (↑V : Type u_2) (↑W : Type u_2) } =
    G

Tactic:
cases G
-- Module: Mathlib.CategoryTheory.Category.ReflQuiv
Goal:
V W : ReflQuiv
toPrefunctor : Prefunctor.{u_1, u_1, u_2, u_2} (↑V : Type u_2) (↑W : Type u_2)
map_id : ∀ (X : (↑V : Type u_2)), toPrefunctor.map (𝟙rq X) = 𝟙rq (toPrefunctor.obj X)
toPrefunctor_1 : Prefunctor.{u_1, u_1, u_2, u_2} (↑V : Type u_2) (↑W : Type u_2)
map_id_1 : ∀ (X : (↑V : Type u_2)), toPrefunctor_1.map (𝟙rq X) = 𝟙rq (toPrefunctor_1.obj X)
hyp :
  forgetToQuiv.map
      { toPrefunctor := toPrefunctor, map_id := map_id :
        ReflPrefunctor.{u_1, u_1, u_2, u_2} (↑V : Type u_2) (↑W : Type u_2) } =
    forgetToQuiv.map { toPrefunctor := toPrefunctor_1, map_id := map_id_1 }
mk :
  ∀ (map_id_2 : ∀ (X : (↑V : Type u_2)), toPrefunctor.map (𝟙rq X) = 𝟙rq (toPrefunctor.obj X)),
    { toPrefunctor := toPrefunctor, map_id := map_id :
        ReflPrefunctor.{u_1, u_1, u_2, u_2} (↑V : Type u_2) (↑W : Type u_2) } =
      { toPrefunctor := toPrefunctor, map_id := map_id_2 }
⊢ { toPrefunctor := toPrefunctor, map_id := map_id :
      ReflPrefunctor.{u_1, u_1, u_2, u_2} (↑V : Type u_2) (↑W : Type u_2) } =
    { toPrefunctor := toPrefunctor_1, map_id := map_id_1 }

Tactic:
cases hyp
-- Module: Mathlib.CategoryTheory.Category.ReflQuiv
Goal:
V W : ReflQuiv
toPrefunctor : Prefunctor.{u_1, u_1, u_2, u_2} (↑V : Type u_2) (↑W : Type u_2)
map_id map_id_1 : ∀ (X : (↑V : Type u_2)), toPrefunctor.map (𝟙rq X) = 𝟙rq (toPrefunctor.obj X)
⊢ { toPrefunctor := toPrefunctor, map_id := map_id :
      ReflPrefunctor.{u_1, u_1, u_2, u_2} (↑V : Type u_2) (↑W : Type u_2) } =
    { toPrefunctor := toPrefunctor, map_id := map_id_1 }

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Category.ReflQuiv
Goal:
⊢ forget ⋙ forgetToQuiv = Quiv.forget

Tactic:
rfl

Premises used: CategoryTheory.Quiv.of, CategoryTheory.Quiv.forget, CategoryTheory.Functor.comp, CategoryTheory.Cat, CategoryTheory.Bundled.of, CategoryTheory.Functor.toPrefunctor, rfl
-- Module: Mathlib.CategoryTheory.Category.ReflQuiv
Goal:
V W : Type u
inst : ReflQuiver.{u_1, u} V
inst_1 : ReflQuiver.{u_1, u} W
e : Quiv.of V ≅ Quiv.of W
h_id : ∀ (X : V), e.hom.map (𝟙rq X) = 𝟙rq (e.hom.obj X)
Y : (↑(of W) : Type u)
⊢ Eq (α := e.hom.obj (e.inv.obj Y) ⟶ e.hom.obj (e.inv.obj Y))
    ((Quiv.homEquivOfIso e : (a : e.inv.obj Y ⟶ e.inv.obj Y) → e.hom.obj (e.inv.obj Y) ⟶ e.hom.obj (e.inv.obj Y))
        (e.inv.map (𝟙rq Y)) :
      e.hom.obj (e.inv.obj Y) ⟶ e.hom.obj (e.inv.obj Y))
    ((Quiv.homEquivOfIso e : (a : e.inv.obj Y ⟶ e.inv.obj Y) → e.hom.obj (e.inv.obj Y) ⟶ e.hom.obj (e.inv.obj Y))
        (𝟙rq (e.inv.obj Y)) :
      e.hom.obj (e.inv.obj Y) ⟶ e.hom.obj (e.inv.obj Y))

Tactic:
simp [Quiv.hom_map_inv_map_of_iso, h_id]

Premises used: CategoryTheory.Quiv.hom_map_inv_map_of_iso
-- Module: Mathlib.CategoryTheory.Category.ReflQuiv
Goal:
V W : Type u
inst : ReflQuiver.{u_1, u} V
inst_1 : ReflQuiver.{u_1, u} W
e : Quiv.of V ≅ Quiv.of W
h_id : ∀ (X : V), e.hom.map (𝟙rq X) = 𝟙rq (e.hom.obj X)
a :
  forgetToQuiv.map
      ({ toPrefunctor := e.hom, map_id := h_id :
          ReflPrefunctor.{u_1, u_1, u, u} (↑(of V) : Type u) (↑(of W) : Type u) } ≫
        { toPrefunctor := e.inv, map_id := ⋯ }) =
    forgetToQuiv.map (𝟙 (of V))
⊢ { toPrefunctor := e.hom, map_id := h_id : ReflPrefunctor.{u_1, u_1, u, u} (↑(of V) : Type u) (↑(of W) : Type u) } ≫
      { toPrefunctor := e.inv, map_id := ⋯ } =
    𝟙 (of V)

Tactic:
apply forgetToQuiv.map_injective

Premises used: CategoryTheory.ReflQuiv.forgetToQuiv, CategoryTheory.Functor.map_injective
-- Module: Mathlib.CategoryTheory.Category.ReflQuiv
Goal:
V W : Type u
inst : ReflQuiver.{u_1, u} V
inst_1 : ReflQuiver.{u_1, u} W
e : Quiv.of V ≅ Quiv.of W
h_id : ∀ (X : V), e.hom.map (𝟙rq X) = 𝟙rq (e.hom.obj X)
⊢ forgetToQuiv.map
      ({ toPrefunctor := e.hom, map_id := h_id :
          ReflPrefunctor.{u_1, u_1, u, u} (↑(of V) : Type u) (↑(of W) : Type u) } ≫
        { toPrefunctor := e.inv, map_id := ⋯ }) =
    forgetToQuiv.map (𝟙 (of V))

Tactic:
e.hom_inv_id

Premises used: CategoryTheory.Quiv.of, CategoryTheory.Iso.hom_inv_id, CategoryTheory.Bundled.of
-- Module: Mathlib.CategoryTheory.Category.ReflQuiv
Goal:
V W : Type u
inst : ReflQuiver.{u_1, u} V
inst_1 : ReflQuiver.{u_1, u} W
e : Quiv.of V ≅ Quiv.of W
h_id : ∀ (X : V), e.hom.map (𝟙rq X) = 𝟙rq (e.hom.obj X)
⊢ forgetToQuiv.map
      ({ toPrefunctor := e.hom, map_id := h_id :
          ReflPrefunctor.{u_1, u_1, u, u} (↑(of V) : Type u) (↑(of W) : Type u) } ≫
        { toPrefunctor := e.inv, map_id := ⋯ }) =
    forgetToQuiv.map (𝟙 (of V))

Tactic:
exact e.hom_inv_id

Premises used: CategoryTheory.Iso.hom_inv_id
-- Module: Mathlib.CategoryTheory.Category.ReflQuiv
Goal:
V W : Type u
inst : ReflQuiver.{u_1, u} V
inst_1 : ReflQuiver.{u_1, u} W
e : Quiv.of V ≅ Quiv.of W
h_id : ∀ (X : V), e.hom.map (𝟙rq X) = 𝟙rq (e.hom.obj X)
a :
  forgetToQuiv.map
      ({ toPrefunctor := e.inv, map_id := ⋯ : ReflPrefunctor.{u_1, u_1, u, u} (↑(of W) : Type u) (↑(of V) : Type u) } ≫
        { toPrefunctor := e.hom, map_id := h_id }) =
    forgetToQuiv.map (𝟙 (of W))
⊢ { toPrefunctor := e.inv, map_id := ⋯ : ReflPrefunctor.{u_1, u_1, u, u} (↑(of W) : Type u) (↑(of V) : Type u) } ≫
      { toPrefunctor := e.hom, map_id := h_id } =
    𝟙 (of W)

Tactic:
apply forgetToQuiv.map_injective

Premises used: CategoryTheory.ReflQuiv.forgetToQuiv, CategoryTheory.Functor.map_injective
-- Module: Mathlib.CategoryTheory.Category.ReflQuiv
Goal:
V W : Type u
inst : ReflQuiver.{u_1, u} V
inst_1 : ReflQuiver.{u_1, u} W
e : Quiv.of V ≅ Quiv.of W
h_id : ∀ (X : V), e.hom.map (𝟙rq X) = 𝟙rq (e.hom.obj X)
⊢ forgetToQuiv.map
      ({ toPrefunctor := e.inv, map_id := ⋯ : ReflPrefunctor.{u_1, u_1, u, u} (↑(of W) : Type u) (↑(of V) : Type u) } ≫
        { toPrefunctor := e.hom, map_id := h_id }) =
    forgetToQuiv.map (𝟙 (of W))

Tactic:
e.inv_hom_id

Premises used: CategoryTheory.Iso.inv_hom_id, CategoryTheory.Quiv.of, CategoryTheory.Bundled.of
-- Module: Mathlib.CategoryTheory.Category.ReflQuiv
Goal:
V W : Type u
inst : ReflQuiver.{u_1, u} V
inst_1 : ReflQuiver.{u_1, u} W
e : Quiv.of V ≅ Quiv.of W
h_id : ∀ (X : V), e.hom.map (𝟙rq X) = 𝟙rq (e.hom.obj X)
⊢ forgetToQuiv.map
      ({ toPrefunctor := e.inv, map_id := ⋯ : ReflPrefunctor.{u_1, u_1, u, u} (↑(of W) : Type u) (↑(of V) : Type u) } ≫
        { toPrefunctor := e.hom, map_id := h_id }) =
    forgetToQuiv.map (𝟙 (of W))

Tactic:
exact e.inv_hom_id

Premises used: CategoryTheory.Iso.inv_hom_id
-- Module: Mathlib.CategoryTheory.Category.ReflQuiv
Goal:
V : Type u_1
inst : ReflQuiver.{u_2, u_1} V
⊢ Functor.Full (quotientFunctor V)

Tactic:
Quotient.full_functor _

Premises used: CategoryTheory.Quotient.full_functor, CategoryTheory.Cat.FreeRefl.quotientFunctor, CategoryTheory.Cat.FreeRefl
-- Module: Mathlib.CategoryTheory.Category.ReflQuiv
Goal:
V : Type u_1
inst : ReflQuiver.{u_2, u_1} V
v : V
⊢ Eq (α := Quiver.Hom (V := FreeRefl.{u_1, u_2} V) (mk v) (mk v)) (homMk (𝟙rq v)) (𝟙 (mk v))

Tactic:
Quotient.sound _ ⟨⟩

Premises used: CategoryTheory.Cat.FreeRefl.mk, CategoryTheory.Cat.FreeReflRel.mk, CategoryTheory.Cat.FreeRefl.homMk, CategoryTheory.Quotient.sound
-- Module: Mathlib.CategoryTheory.Category.ReflQuiv
Goal:
V : Type u_1
inst : ReflQuiver.{u_2, u_1} V
x : Paths V
⊢ Eq (α :=
    Quiver.Hom (V := FreeRefl.{u_1, u_2} V) (Functor.obj (quotientFunctor V) x) (Functor.obj (quotientFunctor V) x))
    (Functor.map (quotientFunctor V) Quiver.Path.nil) (𝟙 (Functor.obj (quotientFunctor V) x))

Tactic:
Functor.map_id _ _

Premises used: CategoryTheory.Functor.map_id
-- Module: Mathlib.CategoryTheory.Category.ReflQuiv
Goal:
V : Type u_1
inst : ReflQuiver.{u_2, u_1} V
x y z : Paths V
p : x ⟶ y
q : y ⟶ z
⊢ Functor.map (quotientFunctor V) (Quiver.Path.cons p q) = Functor.map (quotientFunctor V) p ≫ homMk q

Tactic:
rfl

Premises used: Quiver.Hom.toPath, CategoryTheory.Quotient.comp, Quiver.Path.comp, rfl
-- Module: Mathlib.CategoryTheory.Category.ReflQuiv
Goal:
V : Type u_1
inst : ReflQuiver.{u_2, u_1} V
x y : V
e : x ⟶ y
rw :
  ∃ (i : (x : V) × (y : V) × (x ⟶ y)),
    Arrow.mk (homMk e) =
      Arrow.mk
        (homMk
          (i.snd (β := fun (x : V) ↦ (y : V) × (x ⟶ y)).snd (β := fun (y : V) ↦
            i.fst (β := fun (x : V) ↦ (y : V) × (x ⟶ y)) ⟶ y)))
⊢ MorphismProperty.ofHoms (X := fun (e : (x : V) × (y : V) × (x ⟶ y)) ↦
    mk (e.fst (β := fun (x : V) ↦ (y : V) × (x ⟶ y)))) (Y := fun (e : (x : V) × (y : V) × (x ⟶ y)) ↦
    mk
      (e.snd (β := fun (x : V) ↦ (y : V) × (x ⟶ y)).fst (β := fun (y : V) ↦
        e.fst (β := fun (x : V) ↦ (y : V) × (x ⟶ y)) ⟶ y)))
    (fun (e : (x : V) × (y : V) × (x ⟶ y)) ↦
      homMk
        (e.snd (β := fun (x : V) ↦ (y : V) × (x ⟶ y)).snd (β := fun (y : V) ↦
          e.fst (β := fun (x : V) ↦ (y : V) × (x ⟶ y)) ⟶ y)))
    (homMk e)

Tactic:
rw [MorphismProperty.ofHoms_iff]

Premises used: CategoryTheory.MorphismProperty.ofHoms_iff