awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.ShrinkYoneda
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
X Y : C
f : X ⟶ Y
⊢ Eq.{w + 1} (α := Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} Y) (op X))
    ((shrinkYonedaEquiv :
          (a : shrinkYoneda.{w, v, u}.obj X ⟶ shrinkYoneda.{w, v, u}.obj Y) → (shrinkYoneda.{w, v, u}.obj Y).obj (op X))
        (Functor.map shrinkYoneda.{w, v, u} f) :
      Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} Y) (op X))
    ((Equiv.symm shrinkYonedaObjObjEquiv : (a : unop (op X) ⟶ Y) → (shrinkYoneda.{w, v, u}.obj Y).obj (op X)) f :
      Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} Y) (op X))

Tactic:
simp [shrinkYonedaEquiv, shrinkYoneda, shrinkYonedaObjObjEquiv]

Premises used: CategoryTheory.shrinkYoneda, CategoryTheory.shrinkYonedaEquiv, CategoryTheory.shrinkYonedaObjObjEquiv
-- Module: Mathlib.CategoryTheory.ShrinkYoneda
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
X : C
P Q : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
α : Functor.obj shrinkYoneda.{w, v, u} X ⟶ P
β : P ⟶ Q
⊢ Eq.{w + 1} (α := Q.obj (op X))
    ((shrinkYonedaEquiv : (a : shrinkYoneda.{w, v, u}.obj X ⟶ Q) → Q.obj (op X)) (α ≫ β) : Q.obj (op X))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (β.app (op X)) :
          (a : (fun (X : Type w) ↦ X) (P.obj (op X))) → (fun (X : Type w) ↦ X) (Q.obj (op X)))
        ((shrinkYonedaEquiv : (a : shrinkYoneda.{w, v, u}.obj X ⟶ P) → P.obj (op X)) α : P.obj (op X)) :
      (fun (X : Type w) ↦ X) (Q.obj (op X)))

Tactic:
simp [shrinkYonedaEquiv]

Premises used: CategoryTheory.shrinkYonedaEquiv
-- Module: Mathlib.CategoryTheory.ShrinkYoneda
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
X Y : C
P : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
f : Functor.obj shrinkYoneda.{w, v, u} X ⟶ P
g : Y ⟶ X
⊢ Eq (α := (fun (X : Type w) ↦ X) (P.obj (op Y)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map g.op) :
          (a : (fun (X : Type w) ↦ X) (P.obj (op X))) → (fun (X : Type w) ↦ X) (P.obj (op Y)))
        ((shrinkYonedaEquiv : (a : shrinkYoneda.{w, v, u}.obj X ⟶ P) → P.obj (op X)) f : P.obj (op X)) :
      (fun (X : Type w) ↦ X) (P.obj (op Y)))
    ((shrinkYonedaEquiv : (a : shrinkYoneda.{w, v, u}.obj Y ⟶ P) → P.obj (op Y))
        (Functor.map shrinkYoneda.{w, v, u} g ≫ f) :
      P.obj (op Y))

Tactic:
simpa [shrinkYonedaEquiv, shrinkYoneda]
    using (f.naturality_apply g.op ((equivShrink _) (𝟙 _))).symm

Premises used: CategoryTheory.NatTrans.naturality_apply, Quiver.Hom.op, CategoryTheory.shrinkYoneda, CategoryTheory.shrinkYonedaEquiv, Eq.symm
-- Module: Mathlib.CategoryTheory.ShrinkYoneda
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
X Y : Cᵒᵖ
f : X ⟶ Y
P : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
t : P.obj X
obtain :
  ∀ (t : Functor.obj shrinkYoneda.{w, v, u} (unop X) ⟶ P),
    Eq.{w + 1} (α := P.obj (op (unop Y)))
      ((shrinkYonedaEquiv : (a : shrinkYoneda.{w, v, u}.obj (unop Y) ⟶ P) → P.obj (op (unop Y)))
          ((Equiv.symm shrinkYonedaEquiv : (a : P.obj (op (unop Y))) → shrinkYoneda.{w, v, u}.obj (unop Y) ⟶ P)
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map f) :
                (a : (fun (X : Type w) ↦ X) (P.obj X)) → (fun (X : Type w) ↦ X) (P.obj Y))
              ((shrinkYonedaEquiv : (a : shrinkYoneda.{w, v, u}.obj (unop X) ⟶ P) → P.obj (op (unop X))) t :
                P.obj (op (unop X))))) :
        P.obj (op (unop Y)))
      ((shrinkYonedaEquiv : (a : shrinkYoneda.{w, v, u}.obj (unop Y) ⟶ P) → P.obj (op (unop Y)))
          (Functor.map shrinkYoneda.{w, v, u} f.unop ≫
            (Equiv.symm shrinkYonedaEquiv : (a : P.obj (op (unop X))) → shrinkYoneda.{w, v, u}.obj (unop X) ⟶ P)
              ((shrinkYonedaEquiv : (a : shrinkYoneda.{w, v, u}.obj (unop X) ⟶ P) → P.obj (op (unop X))) t)) :
        P.obj (op (unop Y)))
⊢ Eq.{w + 1} (α := P.obj (op (unop Y)))
    ((shrinkYonedaEquiv : (a : shrinkYoneda.{w, v, u}.obj (unop Y) ⟶ P) → P.obj (op (unop Y)))
        ((Equiv.symm shrinkYonedaEquiv : (a : P.obj (op (unop Y))) → shrinkYoneda.{w, v, u}.obj (unop Y) ⟶ P)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map f) :
              (a : (fun (X : Type w) ↦ X) (P.obj X)) → (fun (X : Type w) ↦ X) (P.obj Y))
            t)) :
      P.obj (op (unop Y)))
    ((shrinkYonedaEquiv : (a : shrinkYoneda.{w, v, u}.obj (unop Y) ⟶ P) → P.obj (op (unop Y)))
        (Functor.map shrinkYoneda.{w, v, u} f.unop ≫
          (Equiv.symm shrinkYonedaEquiv : (a : P.obj (op (unop X))) → shrinkYoneda.{w, v, u}.obj (unop X) ⟶ P) t) :
      P.obj (op (unop Y)))

Tactic:
obtain ⟨t, rfl⟩ := shrinkYonedaEquiv.surjective t

Premises used: CategoryTheory.shrinkYonedaEquiv, Equiv.surjective, rfl
-- Module: Mathlib.CategoryTheory.ShrinkYoneda
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
X Y : Cᵒᵖ
f : X ⟶ Y
P : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
t : Functor.obj shrinkYoneda.{w, v, u} (unop X) ⟶ P
rw :
  Eq (α := P.obj (op (unop Y)))
    ((shrinkYonedaEquiv : (a : shrinkYoneda.{w, v, u}.obj (unop Y) ⟶ P) → P.obj (op (unop Y)))
        ((Equiv.symm shrinkYonedaEquiv : (a : P.obj (op (unop Y))) → shrinkYoneda.{w, v, u}.obj (unop Y) ⟶ P)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map f) :
              (a : (fun (X : Type w) ↦ X) (P.obj X)) → (fun (X : Type w) ↦ X) (P.obj Y))
            ((shrinkYonedaEquiv : (a : shrinkYoneda.{w, v, u}.obj (unop X) ⟶ P) → P.obj (op (unop X))) t :
              P.obj (op (unop X))))) :
      P.obj (op (unop Y)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map f.unop.op) :
          (a : (fun (X : Type w) ↦ X) (P.obj (op (unop X)))) → (fun (X : Type w) ↦ X) (P.obj (op (unop Y))))
        ((shrinkYonedaEquiv : (a : shrinkYoneda.{w, v, u}.obj (unop X) ⟶ P) → P.obj (op (unop X)))
            ((Equiv.symm shrinkYonedaEquiv : (a : P.obj (op (unop X))) → shrinkYoneda.{w, v, u}.obj (unop X) ⟶ P)
              ((shrinkYonedaEquiv : (a : shrinkYoneda.{w, v, u}.obj (unop X) ⟶ P) → P.obj (op (unop X))) t)) :
          P.obj (op (unop X))) :
      (fun (X : Type w) ↦ X) (P.obj (op (unop Y))))
⊢ Eq.{w + 1} (α := P.obj (op (unop Y)))
    ((shrinkYonedaEquiv : (a : shrinkYoneda.{w, v, u}.obj (unop Y) ⟶ P) → P.obj (op (unop Y)))
        ((Equiv.symm shrinkYonedaEquiv : (a : P.obj (op (unop Y))) → shrinkYoneda.{w, v, u}.obj (unop Y) ⟶ P)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map f) :
              (a : (fun (X : Type w) ↦ X) (P.obj X)) → (fun (X : Type w) ↦ X) (P.obj Y))
            ((shrinkYonedaEquiv : (a : shrinkYoneda.{w, v, u}.obj (unop X) ⟶ P) → P.obj (op (unop X))) t :
              P.obj (op (unop X))))) :
      P.obj (op (unop Y)))
    ((shrinkYonedaEquiv : (a : shrinkYoneda.{w, v, u}.obj (unop Y) ⟶ P) → P.obj (op (unop Y)))
        (Functor.map shrinkYoneda.{w, v, u} f.unop ≫
          (Equiv.symm shrinkYonedaEquiv : (a : P.obj (op (unop X))) → shrinkYoneda.{w, v, u}.obj (unop X) ⟶ P)
            ((shrinkYonedaEquiv : (a : shrinkYoneda.{w, v, u}.obj (unop X) ⟶ P) → P.obj (op (unop X))) t)) :
      P.obj (op (unop Y)))

Tactic:
rw [← shrinkYonedaEquiv_naturality]

Premises used: CategoryTheory.shrinkYonedaEquiv_naturality
-- Module: Mathlib.CategoryTheory.ShrinkYoneda
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
X Y : Cᵒᵖ
f : X ⟶ Y
P : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
t : Functor.obj shrinkYoneda.{w, v, u} (unop X) ⟶ P
⊢ Eq (α := P.obj (op (unop Y)))
    ((shrinkYonedaEquiv : (a : shrinkYoneda.{w, v, u}.obj (unop Y) ⟶ P) → P.obj (op (unop Y)))
        ((Equiv.symm shrinkYonedaEquiv : (a : P.obj (op (unop Y))) → shrinkYoneda.{w, v, u}.obj (unop Y) ⟶ P)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map f) :
              (a : (fun (X : Type w) ↦ X) (P.obj X)) → (fun (X : Type w) ↦ X) (P.obj Y))
            ((shrinkYonedaEquiv : (a : shrinkYoneda.{w, v, u}.obj (unop X) ⟶ P) → P.obj (op (unop X))) t :
              P.obj (op (unop X))))) :
      P.obj (op (unop Y)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map f.unop.op) :
          (a : (fun (X : Type w) ↦ X) (P.obj (op (unop X)))) → (fun (X : Type w) ↦ X) (P.obj (op (unop Y))))
        ((shrinkYonedaEquiv : (a : shrinkYoneda.{w, v, u}.obj (unop X) ⟶ P) → P.obj (op (unop X)))
            ((Equiv.symm shrinkYonedaEquiv : (a : P.obj (op (unop X))) → shrinkYoneda.{w, v, u}.obj (unop X) ⟶ P)
              ((shrinkYonedaEquiv : (a : shrinkYoneda.{w, v, u}.obj (unop X) ⟶ P) → P.obj (op (unop X))) t)) :
          P.obj (op (unop X))) :
      (fun (X : Type w) ↦ X) (P.obj (op (unop Y))))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.ShrinkYoneda
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
X : C
P : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
s : P.obj (op X)
Y : C
f : Y ⟶ X
obtain :
  ∀ (g : Functor.obj shrinkYoneda.{w, v, u} X ⟶ P),
    Eq (α := (fun (X : Type w) ↦ X) (P.obj (op Y)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (NatTrans.app
                ((Equiv.symm shrinkYonedaEquiv : (a : P.obj (op X)) → shrinkYoneda.{w, v, u}.obj X ⟶ P)
                  ((shrinkYonedaEquiv : (a : shrinkYoneda.{w, v, u}.obj X ⟶ P) → P.obj (op X)) g))
                (op Y)) :
            (a : (fun (X : Type w) ↦ X) ((shrinkYoneda.{w, v, u}.obj X).obj (op Y))) →
              (fun (X : Type w) ↦ X) (P.obj (op Y)))
          ((Equiv.symm shrinkYonedaObjObjEquiv : (a : unop (op Y) ⟶ X) → (shrinkYoneda.{w, v, u}.obj X).obj (op Y)) f :
            Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} X) (op Y)) :
        (fun (X : Type w) ↦ X) (P.obj (op Y)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map f.op) :
            (a : (fun (X : Type w) ↦ X) (P.obj (op X))) → (fun (X : Type w) ↦ X) (P.obj (op Y)))
          ((shrinkYonedaEquiv : (a : shrinkYoneda.{w, v, u}.obj X ⟶ P) → P.obj (op X)) g : P.obj (op X)) :
        (fun (X : Type w) ↦ X) (P.obj (op Y)))
⊢ Eq (α := (fun (X : Type w) ↦ X) (P.obj (op Y)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (NatTrans.app ((Equiv.symm shrinkYonedaEquiv : (a : P.obj (op X)) → shrinkYoneda.{w, v, u}.obj X ⟶ P) s)
              (op Y)) :
          (a : (fun (X : Type w) ↦ X) ((shrinkYoneda.{w, v, u}.obj X).obj (op Y))) →
            (fun (X : Type w) ↦ X) (P.obj (op Y)))
        ((Equiv.symm shrinkYonedaObjObjEquiv : (a : unop (op Y) ⟶ X) → (shrinkYoneda.{w, v, u}.obj X).obj (op Y)) f :
          Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} X) (op Y)) :
      (fun (X : Type w) ↦ X) (P.obj (op Y)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map f.op) :
          (a : (fun (X : Type w) ↦ X) (P.obj (op X))) → (fun (X : Type w) ↦ X) (P.obj (op Y)))
        s :
      (fun (X : Type w) ↦ X) (P.obj (op Y)))

Tactic:
obtain ⟨g, rfl⟩ := shrinkYonedaEquiv.surjective s

Premises used: CategoryTheory.shrinkYonedaEquiv, Equiv.surjective, rfl
-- Module: Mathlib.CategoryTheory.ShrinkYoneda
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
X : C
P : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
Y : C
f : Y ⟶ X
g : Functor.obj shrinkYoneda.{w, v, u} X ⟶ P
⊢ Eq (α := (fun (X : Type w) ↦ X) (P.obj (op Y)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (NatTrans.app
              ((Equiv.symm shrinkYonedaEquiv : (a : P.obj (op X)) → shrinkYoneda.{w, v, u}.obj X ⟶ P)
                ((shrinkYonedaEquiv : (a : shrinkYoneda.{w, v, u}.obj X ⟶ P) → P.obj (op X)) g))
              (op Y)) :
          (a : (fun (X : Type w) ↦ X) ((shrinkYoneda.{w, v, u}.obj X).obj (op Y))) →
            (fun (X : Type w) ↦ X) (P.obj (op Y)))
        ((Equiv.symm shrinkYonedaObjObjEquiv : (a : unop (op Y) ⟶ X) → (shrinkYoneda.{w, v, u}.obj X).obj (op Y)) f :
          Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} X) (op Y)) :
      (fun (X : Type w) ↦ X) (P.obj (op Y)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.map f.op) :
          (a : (fun (X : Type w) ↦ X) (P.obj (op X))) → (fun (X : Type w) ↦ X) (P.obj (op Y)))
        ((shrinkYonedaEquiv : (a : shrinkYoneda.{w, v, u}.obj X ⟶ P) → P.obj (op X)) g : P.obj (op X)) :
      (fun (X : Type w) ↦ X) (P.obj (op Y)))

Tactic:
simp [map_shrinkYonedaEquiv]

Premises used: CategoryTheory.map_shrinkYonedaEquiv
-- Module: Mathlib.CategoryTheory.ShrinkYoneda
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
X Y : C
f :
  Quiver.Hom (V := Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)) (Functor.obj shrinkYoneda.{w, v, u} X)
    (Functor.obj shrinkYoneda.{w, v, u} Y)
obtain :
  ∀ (f : Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} Y) (op X)),
    Eq (α :=
      Quiver.Hom (V := Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)) (Functor.obj shrinkYoneda.{w, v, u} X)
        (Functor.obj shrinkYoneda.{w, v, u} Y))
      (Functor.map shrinkYoneda.{w, v, u}
          ((shrinkYonedaObjObjEquiv : (a : (shrinkYoneda.{w, v, u}.obj Y).obj (op X)) → unop (op X) ⟶ Y)
            ((shrinkYonedaEquiv :
                (a : shrinkYoneda.{w, v, u}.obj X ⟶ shrinkYoneda.{w, v, u}.obj Y) →
                  (shrinkYoneda.{w, v, u}.obj Y).obj (op X))
              ((Equiv.symm shrinkYonedaEquiv :
                  (a : (shrinkYoneda.{w, v, u}.obj Y).obj (op X)) →
                    shrinkYoneda.{w, v, u}.obj X ⟶ shrinkYoneda.{w, v, u}.obj Y)
                f))) :
        Quiver.Hom (V := Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)) (Functor.obj shrinkYoneda.{w, v, u} X)
          (Functor.obj shrinkYoneda.{w, v, u} Y))
      ((Equiv.symm shrinkYonedaEquiv :
            (a : (shrinkYoneda.{w, v, u}.obj Y).obj (op X)) →
              shrinkYoneda.{w, v, u}.obj X ⟶ shrinkYoneda.{w, v, u}.obj Y)
          f :
        Quiver.Hom (V := Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)) (Functor.obj shrinkYoneda.{w, v, u} X)
          (Functor.obj shrinkYoneda.{w, v, u} Y))
⊢ Functor.map shrinkYoneda.{w, v, u}
      ((shrinkYonedaObjObjEquiv : (a : (shrinkYoneda.{w, v, u}.obj Y).obj (op X)) → unop (op X) ⟶ Y)
        ((shrinkYonedaEquiv :
            (a : shrinkYoneda.{w, v, u}.obj X ⟶ shrinkYoneda.{w, v, u}.obj Y) →
              (shrinkYoneda.{w, v, u}.obj Y).obj (op X))
          f)) =
    f

Tactic:
obtain ⟨f, rfl⟩ := shrinkYonedaEquiv.symm.surjective f

Premises used: CategoryTheory.shrinkYonedaEquiv, Equiv.surjective, Equiv.symm, rfl
-- Module: Mathlib.CategoryTheory.ShrinkYoneda
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
X Y : C
f : X ⟶ Y
⊢ (shrinkYonedaObjObjEquiv : (a : (shrinkYoneda.{w, v, u}.obj Y).obj (op X)) → unop (op X) ⟶ Y)
      ((shrinkYonedaEquiv :
          (a : shrinkYoneda.{w, v, u}.obj X ⟶ shrinkYoneda.{w, v, u}.obj Y) → (shrinkYoneda.{w, v, u}.obj Y).obj (op X))
        (Functor.map shrinkYoneda.{w, v, u} f)) =
    f

Tactic:
simp [shrinkYonedaEquiv_shrinkYoneda_map]

Premises used: CategoryTheory.shrinkYonedaEquiv_shrinkYoneda_map
-- Module: Mathlib.CategoryTheory.ShrinkYoneda
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
⊢ Functor.Faithful (C := C) shrinkYoneda.{w, v, u}

Tactic:
(fullyFaithfulShrinkYoneda C).faithful

Premises used: CategoryTheory.Functor.FullyFaithful.faithful, CategoryTheory.fullyFaithfulShrinkYoneda
-- Module: Mathlib.CategoryTheory.ShrinkYoneda
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
⊢ Functor.Full (C := C) shrinkYoneda.{w, v, u}

Tactic:
(fullyFaithfulShrinkYoneda C).full

Premises used: CategoryTheory.Functor.FullyFaithful.full, CategoryTheory.fullyFaithfulShrinkYoneda
-- Module: Mathlib.CategoryTheory.ShrinkYoneda
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
X : C
X_1 Y : Cᵒᵖ
f : X_1 ⟶ Y
h :
  ∀ (x : Functor.obj (Functor.obj shrinkYoneda.{v, v, u} X) X_1),
    Eq (α := Functor.obj (Functor.obj yoneda X) Y)
      (TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (Functor.map (Functor.obj shrinkYoneda.{v, v, u} X) f ≫
            Iso.hom
              ((fun (Y : Cᵒᵖ) ↦
                  (Equiv.toIso shrinkYonedaObjObjEquiv :
                    Functor.obj (Functor.obj shrinkYoneda.{v, v, u} X) Y ≅ unop Y ⟶ X))
                Y)))
        x)
      (TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (Iso.hom
              ((fun (Y : Cᵒᵖ) ↦
                  (Equiv.toIso shrinkYonedaObjObjEquiv :
                    Functor.obj (Functor.obj shrinkYoneda.{v, v, u} X) Y ≅ unop Y ⟶ X))
                X_1) ≫
            Functor.map (Functor.obj yoneda X) f))
        x)
⊢ Eq (α := Functor.obj (Functor.obj shrinkYoneda.{v, v, u} X) X_1 ⟶ Functor.obj (Functor.obj yoneda X) Y)
    (Functor.map (Functor.obj shrinkYoneda.{v, v, u} X) f ≫
      Iso.hom
        ((fun (Y : Cᵒᵖ) ↦
            (Equiv.toIso shrinkYonedaObjObjEquiv : Functor.obj (Functor.obj shrinkYoneda.{v, v, u} X) Y ≅ unop Y ⟶ X))
          Y))
    (Iso.hom
        ((fun (Y : Cᵒᵖ) ↦
            (Equiv.toIso shrinkYonedaObjObjEquiv : Functor.obj (Functor.obj shrinkYoneda.{v, v, u} X) Y ≅ unop Y ⟶ X))
          X_1) ≫
      Functor.map (Functor.obj yoneda X) f)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.ShrinkYoneda
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
X : C
X_1 Y : Cᵒᵖ
f : X_1 ⟶ Y
x : Functor.obj (Functor.obj shrinkYoneda.{v, v, u} X) X_1
⊢ Eq (α := Functor.obj (Functor.obj yoneda X) Y)
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (Functor.map (Functor.obj shrinkYoneda.{v, v, u} X) f ≫
          Iso.hom
            ((fun (Y : Cᵒᵖ) ↦
                (Equiv.toIso shrinkYonedaObjObjEquiv :
                  Functor.obj (Functor.obj shrinkYoneda.{v, v, u} X) Y ≅ unop Y ⟶ X))
              Y)))
      x)
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (Iso.hom
            ((fun (Y : Cᵒᵖ) ↦
                (Equiv.toIso shrinkYonedaObjObjEquiv :
                  Functor.obj (Functor.obj shrinkYoneda.{v, v, u} X) Y ≅ unop Y ⟶ X))
              X_1) ≫
          Functor.map (Functor.obj yoneda X) f))
      x)

Tactic:
simp [shrinkYonedaObjObjEquiv_obj_map]

Premises used: CategoryTheory.shrinkYonedaObjObjEquiv_obj_map
-- Module: Mathlib.CategoryTheory.ShrinkYoneda
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
X Y : C
f : X ⟶ Y
w :
  ∀ (x : Cᵒᵖ) (x_1 : Functor.obj (Functor.obj shrinkYoneda.{v, v, u} X) x),
    Eq (α := Functor.obj (Functor.obj yoneda Y) x)
      (TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (NatTrans.app
            (Functor.map shrinkYoneda.{v, v, u} f ≫
              Iso.hom
                ((fun (X : C) ↦
                    (NatIso.ofComponents (fun (Y : Cᵒᵖ) ↦ Equiv.toIso shrinkYonedaObjObjEquiv) ⋯ :
                      Iso (C := Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)) (Functor.obj shrinkYoneda.{v, v, u} X)
                        (Functor.obj yoneda X)))
                  Y))
            x))
        x_1)
      (TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (NatTrans.app
            (Iso.hom
                ((fun (X : C) ↦
                    (NatIso.ofComponents (fun (Y : Cᵒᵖ) ↦ Equiv.toIso shrinkYonedaObjObjEquiv) ⋯ :
                      Iso (C := Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)) (Functor.obj shrinkYoneda.{v, v, u} X)
                        (Functor.obj yoneda X)))
                  X) ≫
              Functor.map yoneda f)
            x))
        x_1)
⊢ Eq (α :=
    Quiver.Hom (V := Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)) (Functor.obj shrinkYoneda.{v, v, u} X)
      (Functor.obj yoneda Y))
    (Functor.map shrinkYoneda.{v, v, u} f ≫
      Iso.hom
        ((fun (X : C) ↦
            (NatIso.ofComponents (fun (Y : Cᵒᵖ) ↦ Equiv.toIso shrinkYonedaObjObjEquiv) ⋯ :
              Iso (C := Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)) (Functor.obj shrinkYoneda.{v, v, u} X)
                (Functor.obj yoneda X)))
          Y))
    (Iso.hom
        ((fun (X : C) ↦
            (NatIso.ofComponents (fun (Y : Cᵒᵖ) ↦ Equiv.toIso shrinkYonedaObjObjEquiv) ⋯ :
              Iso (C := Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)) (Functor.obj shrinkYoneda.{v, v, u} X)
                (Functor.obj yoneda X)))
          X) ≫
      Functor.map yoneda f)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.ShrinkYoneda
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
X Y : C
f : X ⟶ Y
x : Cᵒᵖ
x_1 : Functor.obj (Functor.obj shrinkYoneda.{v, v, u} X) x
⊢ Eq (α := Functor.obj (Functor.obj yoneda Y) x)
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (NatTrans.app
          (Functor.map shrinkYoneda.{v, v, u} f ≫
            Iso.hom
              ((fun (X : C) ↦
                  (NatIso.ofComponents (fun (Y : Cᵒᵖ) ↦ Equiv.toIso shrinkYonedaObjObjEquiv) ⋯ :
                    Iso (C := Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)) (Functor.obj shrinkYoneda.{v, v, u} X)
                      (Functor.obj yoneda X)))
                Y))
          x))
      x_1)
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (NatTrans.app
          (Iso.hom
              ((fun (X : C) ↦
                  (NatIso.ofComponents (fun (Y : Cᵒᵖ) ↦ Equiv.toIso shrinkYonedaObjObjEquiv) ⋯ :
                    Iso (C := Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)) (Functor.obj shrinkYoneda.{v, v, u} X)
                      (Functor.obj yoneda X)))
                X) ≫
            Functor.map yoneda f)
          x))
      x_1)

Tactic:
simp [shrinkYonedaObjObjEquiv_map_app]

Premises used: CategoryTheory.shrinkYonedaObjObjEquiv_map_app