awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Shift.Twist
Goal:
C : Type u
inst : Category.{v, u} C
A : Type w
inst_1 : AddMonoid A
inst_2 : HasShift.{v, u, w} C A
t : TwistShiftData.{w, v, u} C A
i j k : A
h : i + j = k
X : t.Category
this :
  NatTrans.app (Iso.hom (shiftFunctorAdd' t.Category i j k h)) X =
    HSMul.hSMul (β :=
      Functor.obj.{v, v, u, u} (shiftFunctor C k) X ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C i ⋙ shiftFunctor C j) X)
      (↑(t.z i j) : CatCenter C) (NatTrans.app (Iso.hom (shiftFunctorAdd' C i j k h)) X)
⊢ NatTrans.app (Iso.hom (shiftFunctorAdd' C i j k h)) X =
    𝟙 (Functor.obj.{v, v, u, u} (shiftFunctor C k) X) ≫
      NatTrans.app (Iso.hom (shiftFunctorAdd' C i j k h)) X ≫
        Functor.map (shiftFunctor C j) (𝟙 (Functor.obj.{v, v, u, u} (shiftFunctor C i) X)) ≫
          𝟙 (Functor.obj.{v, v, u, u} (shiftFunctor C j) (Functor.obj.{v, v, u, u} (shiftFunctor C i) X))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Shift.Twist
Goal:
C : Type u
inst : Category.{v, u} C
A : Type w
inst_1 : AddMonoid A
inst_2 : HasShift.{v, u, w} C A
t : TwistShiftData.{w, v, u} C A
i j k : A
h : i + j = k
X : t.Category
dsimp :
  NatTrans.app (Iso.inv (shiftFunctorAdd t.Category i j)) X ≫ NatTrans.app (eqToHom ⋯) X =
    HSMul.hSMul (β :=
      Functor.obj.{v, v, u, u} (shiftFunctor C j) (Functor.obj.{v, v, u, u} (shiftFunctor C i) X) ⟶
        Functor.obj.{v, v, u, u} (shiftFunctor C k) X)
      (↑(t.z i j)⁻¹ : CatCenter C) (NatTrans.app (Iso.inv (shiftFunctorAdd C i j)) X ≫ NatTrans.app (eqToHom ⋯) X)
⊢ NatTrans.app (Iso.inv (shiftFunctorAdd' t.Category i j k h)) X =
    HSMul.hSMul (β :=
      Functor.obj.{v, v, u, u} (shiftFunctor C i ⋙ shiftFunctor C j) X ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C k) X)
      (↑(t.z i j)⁻¹ : CatCenter C) (NatTrans.app (Iso.inv (shiftFunctorAdd' C i j k h)) X)

Tactic:
dsimp [shiftFunctorAdd']

Premises used: CategoryTheory.shiftFunctorAdd'
-- Module: Mathlib.CategoryTheory.Shift.Twist
Goal:
C : Type u
inst : Category.{v, u} C
A : Type w
inst_1 : AddMonoid A
inst_2 : HasShift.{v, u, w} C A
t : TwistShiftData.{w, v, u} C A
i j k : A
h : i + j = k
X : t.Category
⊢ NatTrans.app (Iso.inv (shiftFunctorAdd' t.Category i j k h)) X =
    HSMul.hSMul (β :=
      Functor.obj.{v, v, u, u} (shiftFunctor C i ⋙ shiftFunctor C j) X ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C k) X)
      (↑(t.z i j)⁻¹ : CatCenter C) (NatTrans.app (Iso.inv (shiftFunctorAdd' C i j k h)) X)

Tactic:
have : (shiftFunctorAdd' t.Category i j k h).inv.app X =
      ((t.z i j)⁻¹).val • (shiftFunctorAdd' C i j k h).inv.app X := by
    dsimp [shiftFunctorAdd']
    cat_disch
-- Module: Mathlib.CategoryTheory.Shift.Twist
Goal:
C : Type u
inst : Category.{v, u} C
A : Type w
inst_1 : AddMonoid A
inst_2 : HasShift.{v, u, w} C A
t : TwistShiftData.{w, v, u} C A
i j k : A
h : i + j = k
X : t.Category
this :
  NatTrans.app (Iso.inv (shiftFunctorAdd' t.Category i j k h)) X =
    HSMul.hSMul (β :=
      Functor.obj.{v, v, u, u} (shiftFunctor C i ⋙ shiftFunctor C j) X ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C k) X)
      (↑(t.z i j)⁻¹ : CatCenter C) (NatTrans.app (Iso.inv (shiftFunctorAdd' C i j k h)) X)
rw :
  HSMul.hSMul (β :=
      Functor.obj.{v, v, u, u} (shiftFunctor C i ⋙ shiftFunctor C j) X ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C k) X)
      (↑(t.z i j)⁻¹ : CatCenter C) (NatTrans.app (Iso.inv (shiftFunctorAdd' C i j k h)) X) =
    (↑(t.z i j)⁻¹ : CatCenter C) •
      (t.shiftIso j).hom.app (Functor.obj.{v, v, u, u} (shiftFunctor t.Category i) X) ≫
        Functor.map (shiftFunctor C j) ((t.shiftIso i).hom.app X) ≫
          NatTrans.app (Iso.inv (shiftFunctorAdd' C i j k h)) X ≫ (t.shiftIso k).inv.app X
⊢ NatTrans.app (Iso.inv (shiftFunctorAdd' t.Category i j k h)) X =
    (↑(t.z i j)⁻¹ : CatCenter C) •
      (t.shiftIso j).hom.app (Functor.obj.{v, v, u, u} (shiftFunctor t.Category i) X) ≫
        Functor.map (shiftFunctor C j) ((t.shiftIso i).hom.app X) ≫
          NatTrans.app (Iso.inv (shiftFunctorAdd' C i j k h)) X ≫ (t.shiftIso k).inv.app X

Tactic:
rw [this]
-- Module: Mathlib.CategoryTheory.Shift.Twist
Goal:
C : Type u
inst : Category.{v, u} C
A : Type w
inst_1 : AddMonoid A
inst_2 : HasShift.{v, u, w} C A
t : TwistShiftData.{w, v, u} C A
i j k : A
h : i + j = k
X : t.Category
this :
  NatTrans.app (Iso.inv (shiftFunctorAdd' t.Category i j k h)) X =
    HSMul.hSMul (β :=
      Functor.obj.{v, v, u, u} (shiftFunctor C i ⋙ shiftFunctor C j) X ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C k) X)
      (↑(t.z i j)⁻¹ : CatCenter C) (NatTrans.app (Iso.inv (shiftFunctorAdd' C i j k h)) X)
e_a :
  NatTrans.app (Iso.inv (shiftFunctorAdd' C i j k h)) X =
    (t.shiftIso j).hom.app (Functor.obj.{v, v, u, u} (shiftFunctor t.Category i) X) ≫
      Functor.map (shiftFunctor C j) ((t.shiftIso i).hom.app X) ≫
        NatTrans.app (Iso.inv (shiftFunctorAdd' C i j k h)) X ≫ (t.shiftIso k).inv.app X
⊢ HSMul.hSMul (β :=
      Functor.obj.{v, v, u, u} (shiftFunctor C i ⋙ shiftFunctor C j) X ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C k) X)
      (↑(t.z i j)⁻¹ : CatCenter C) (NatTrans.app (Iso.inv (shiftFunctorAdd' C i j k h)) X) =
    (↑(t.z i j)⁻¹ : CatCenter C) •
      (t.shiftIso j).hom.app (Functor.obj.{v, v, u, u} (shiftFunctor t.Category i) X) ≫
        Functor.map (shiftFunctor C j) ((t.shiftIso i).hom.app X) ≫
          NatTrans.app (Iso.inv (shiftFunctorAdd' C i j k h)) X ≫ (t.shiftIso k).inv.app X

Tactic:
congr
-- Module: Mathlib.CategoryTheory.Shift.Twist
Goal:
C : Type u
inst : Category.{v, u} C
A : Type w
inst_1 : AddMonoid A
inst_2 : HasShift.{v, u, w} C A
t : TwistShiftData.{w, v, u} C A
i j k : A
h : i + j = k
X : t.Category
this :
  NatTrans.app (Iso.inv (shiftFunctorAdd' t.Category i j k h)) X =
    HSMul.hSMul (β :=
      Functor.obj.{v, v, u, u} (shiftFunctor C i ⋙ shiftFunctor C j) X ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C k) X)
      (↑(t.z i j)⁻¹ : CatCenter C) (NatTrans.app (Iso.inv (shiftFunctorAdd' C i j k h)) X)
e_a :
  NatTrans.app (Iso.inv (shiftFunctorAdd' C i j k h)) X =
    𝟙 (Functor.obj.{v, v, u, u} (shiftFunctor C j) (Functor.obj.{v, v, u, u} (shiftFunctor C i) X)) ≫
      Functor.map (shiftFunctor C j) (𝟙 (Functor.obj.{v, v, u, u} (shiftFunctor C i) X)) ≫
        NatTrans.app (Iso.inv (shiftFunctorAdd' C i j k h)) X ≫ 𝟙 (Functor.obj.{v, v, u, u} (shiftFunctor C k) X)
⊢ NatTrans.app (Iso.inv (shiftFunctorAdd' C i j k h)) X =
    (t.shiftIso j).hom.app (Functor.obj.{v, v, u, u} (shiftFunctor t.Category i) X) ≫
      Functor.map (shiftFunctor C j) ((t.shiftIso i).hom.app X) ≫
        NatTrans.app (Iso.inv (shiftFunctorAdd' C i j k h)) X ≫ (t.shiftIso k).inv.app X

Tactic:
change _ = 𝟙 _ ≫ (shiftFunctor C j).map (𝟙 _) ≫ _ ≫ 𝟙 _

Premises used: CategoryTheory.shiftFunctor, CategoryTheory.CategoryStruct.id, CategoryTheory.Functor.map
-- Module: Mathlib.CategoryTheory.Shift.Twist
Goal:
C : Type u
inst : Category.{v, u} C
A : Type w
inst_1 : AddMonoid A
inst_2 : HasShift.{v, u, w} C A
t : TwistShiftData.{w, v, u} C A
i j k : A
h : i + j = k
X : t.Category
this :
  NatTrans.app (Iso.inv (shiftFunctorAdd' t.Category i j k h)) X =
    HSMul.hSMul (β :=
      Functor.obj.{v, v, u, u} (shiftFunctor C i ⋙ shiftFunctor C j) X ⟶ Functor.obj.{v, v, u, u} (shiftFunctor C k) X)
      (↑(t.z i j)⁻¹ : CatCenter C) (NatTrans.app (Iso.inv (shiftFunctorAdd' C i j k h)) X)
⊢ NatTrans.app (Iso.inv (shiftFunctorAdd' C i j k h)) X =
    𝟙 (Functor.obj.{v, v, u, u} (shiftFunctor C j) (Functor.obj.{v, v, u, u} (shiftFunctor C i) X)) ≫
      Functor.map (shiftFunctor C j) (𝟙 (Functor.obj.{v, v, u, u} (shiftFunctor C i) X)) ≫
        NatTrans.app (Iso.inv (shiftFunctorAdd' C i j k h)) X ≫ 𝟙 (Functor.obj.{v, v, u, u} (shiftFunctor C k) X)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.ShrinkYoneda
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
X : C
x : Cᵒᵖ
dsimp : Small.{w, v} (unop x ⟶ X)
⊢ Small.{w, v} (Functor.obj (Functor.obj yoneda X) x)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.ShrinkYoneda
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
X : C
x : Cᵒᵖ
⊢ Small.{w, v} (unop x ⟶ X)

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

Tactic:
simp [shrinkYoneda, shrinkYonedaObjObjEquiv]

Premises used: CategoryTheory.shrinkYoneda, CategoryTheory.shrinkYonedaObjObjEquiv
-- Module: Mathlib.CategoryTheory.ShrinkYoneda
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w, v, u} C
X Y Y' : C
g : Y' ⟶ Y
f : Y ⟶ X
⊢ Eq.{w + 1} (α := Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} X) (op Y'))
    ((Equiv.symm shrinkYonedaObjObjEquiv : (a : unop (op Y') ⟶ X) → (shrinkYoneda.{w, v, u}.obj X).obj (op Y'))
        (g ≫ f) :
      Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} X) (op Y'))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Functor.map (Functor.obj shrinkYoneda.{w, v, u} X) g.op) :
          (a : (fun (X : Type w) ↦ X) ((shrinkYoneda.{w, v, u}.obj X).obj (op Y))) →
            (fun (X : Type w) ↦ X) ((shrinkYoneda.{w, v, u}.obj X).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) (Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} X) (op Y')))

Tactic:
(shrinkYoneda_obj_map_shrinkYonedaObjObjEquiv_symm g.op f).symm

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

Tactic:
simp [shrinkYoneda, shrinkYonedaObjObjEquiv]

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

Tactic:
simp [shrinkYoneda, shrinkYonedaObjObjEquiv]

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

Tactic:
simp [shrinkYonedaObjObjEquiv, shrinkYoneda]

Premises used: CategoryTheory.shrinkYoneda, 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 : Functor.{v, w, u, w + 1} Cᵒᵖ (Type w)
x : P.obj (op X)
Y Z : Cᵒᵖ
g : Y ⟶ Z
h :
  ∀ (x_1 : Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} X) Y),
    TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (Functor.map (Functor.obj shrinkYoneda.{w, v, u} X) g ≫
            ↾fun (f : Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} X) Z) ↦
              (ConcreteCategory.hom (FC := TypeCat.Fun)
                    (P.map
                      (Quiver.Hom.op
                        ((Equiv.symm (equivShrink (Functor.obj (Functor.obj yoneda X) Z)) :
                            (a : Shrink.{w, v} ((yoneda.obj X).obj Z)) → (yoneda.obj X).obj Z)
                          f))) :
                  (a : (fun (X : Type w) ↦ X) (P.obj (op X))) → (fun (X : Type w) ↦ X) (P.obj (op (unop Z))))
                x))
        x_1 =
      TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          ((↾fun (f : Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} X) Y) ↦
              (ConcreteCategory.hom (FC := TypeCat.Fun)
                    (P.map
                      (Quiver.Hom.op
                        ((Equiv.symm (equivShrink (Functor.obj (Functor.obj yoneda X) Y)) :
                            (a : Shrink.{w, v} ((yoneda.obj X).obj Y)) → (yoneda.obj X).obj Y)
                          f))) :
                  (a : (fun (X : Type w) ↦ X) (P.obj (op X))) → (fun (X : Type w) ↦ X) (P.obj (op (unop Y))))
                x) ≫
            P.map g))
        x_1
⊢ Eq (α := Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} X) Y ⟶ P.obj Z)
    (Functor.map (Functor.obj shrinkYoneda.{w, v, u} X) g ≫
      ↾fun (f : Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} X) Z) ↦
        (ConcreteCategory.hom (FC := TypeCat.Fun)
              (P.map
                (Quiver.Hom.op
                  ((Equiv.symm (equivShrink (Functor.obj (Functor.obj yoneda X) Z)) :
                      (a : Shrink.{w, v} ((yoneda.obj X).obj Z)) → (yoneda.obj X).obj Z)
                    f))) :
            (a : (fun (X : Type w) ↦ X) (P.obj (op X))) → (fun (X : Type w) ↦ X) (P.obj (op (unop Z))))
          x)
    ((↾fun (f : Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} X) Y) ↦
        (ConcreteCategory.hom (FC := TypeCat.Fun)
              (P.map
                (Quiver.Hom.op
                  ((Equiv.symm (equivShrink (Functor.obj (Functor.obj yoneda X) Y)) :
                      (a : Shrink.{w, v} ((yoneda.obj X).obj Y)) → (yoneda.obj X).obj Y)
                    f))) :
            (a : (fun (X : Type w) ↦ X) (P.obj (op X))) → (fun (X : Type w) ↦ X) (P.obj (op (unop Y))))
          x) ≫
      P.map g)

Tactic:
ext
-- 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)
x : P.obj (op X)
Y Z : Cᵒᵖ
g : Y ⟶ Z
x_1 : Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} X) Y
⊢ TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (Functor.map (Functor.obj shrinkYoneda.{w, v, u} X) g ≫
          ↾fun (f : Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} X) Z) ↦
            (ConcreteCategory.hom (FC := TypeCat.Fun)
                  (P.map
                    (Quiver.Hom.op
                      ((Equiv.symm (equivShrink (Functor.obj (Functor.obj yoneda X) Z)) :
                          (a : Shrink.{w, v} ((yoneda.obj X).obj Z)) → (yoneda.obj X).obj Z)
                        f))) :
                (a : (fun (X : Type w) ↦ X) (P.obj (op X))) → (fun (X : Type w) ↦ X) (P.obj (op (unop Z))))
              x))
      x_1 =
    TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        ((↾fun (f : Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} X) Y) ↦
            (ConcreteCategory.hom (FC := TypeCat.Fun)
                  (P.map
                    (Quiver.Hom.op
                      ((Equiv.symm (equivShrink (Functor.obj (Functor.obj yoneda X) Y)) :
                          (a : Shrink.{w, v} ((yoneda.obj X).obj Y)) → (yoneda.obj X).obj Y)
                        f))) :
                (a : (fun (X : Type w) ↦ X) (P.obj (op X))) → (fun (X : Type w) ↦ X) (P.obj (op (unop Y))))
              x) ≫
          P.map g))
      x_1

Tactic:
simp [shrinkYoneda]

Premises used: CategoryTheory.shrinkYoneda
-- 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)
τ : Functor.obj shrinkYoneda.{w, v, u} X ⟶ P
Y : Cᵒᵖ
f : Functor.obj (Functor.obj yoneda X) Y
⊢ TypeCat.Fun.toFun (X := Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} X) Y)
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (NatTrans.app
          ((fun (x : P.obj (op X)) ↦
              ({
                  app := fun (Y : Cᵒᵖ) ↦
                    ↾fun (f : Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} X) Y) ↦
                      (ConcreteCategory.hom (FC := TypeCat.Fun)
                            (P.map
                              (Quiver.Hom.op
                                ((Equiv.symm (equivShrink (Functor.obj (Functor.obj yoneda X) Y)) :
                                    (a : Shrink.{w, v} ((yoneda.obj X).obj Y)) → (yoneda.obj X).obj Y)
                                  f))) :
                          (a : (fun (X : Type w) ↦ X) (P.obj (op X))) → (fun (X : Type w) ↦ X) (P.obj (op (unop Y))))
                        x,
                  naturality := ⋯ } :
                NatTrans (Functor.obj shrinkYoneda.{w, v, u} X) P))
            ((fun (τ : Functor.obj shrinkYoneda.{w, v, u} X ⟶ P) ↦
                ((ConcreteCategory.hom (FC := TypeCat.Fun) (τ.app (op X)) :
                      (a : (fun (X : Type w) ↦ X) ((shrinkYoneda.{w, v, u}.obj X).obj (op X))) →
                        (fun (X : Type w) ↦ X) (P.obj (op X)))
                    ((equivShrink (Functor.obj (Functor.obj yoneda X) (op X)) :
                          (a : (yoneda.obj X).obj (op X)) → Shrink.{w, v} ((yoneda.obj X).obj (op X)))
                        (𝟙 X) :
                      Shrink.{w, v} (Functor.obj (Functor.obj yoneda X) (op X))) :
                  (fun (X : Type w) ↦ X) (P.obj (op X))))
              τ))
          Y))
      ((equivShrink (Functor.obj (Functor.obj yoneda X) Y) :
          (a : (yoneda.obj X).obj Y) → Shrink.{w, v} ((yoneda.obj X).obj Y))
        f) =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (τ.app Y)).toFun
      ((equivShrink (Functor.obj (Functor.obj yoneda X) Y) :
          (a : (yoneda.obj X).obj Y) → Shrink.{w, v} ((yoneda.obj X).obj Y))
        f)

Tactic:
simpa [shrinkYoneda] using ((τ.naturality_apply f.op) (equivShrink _ (𝟙 X))).symm

Premises used: CategoryTheory.NatTrans.naturality_apply, Quiver.Hom.op, CategoryTheory.shrinkYoneda, CategoryTheory.CategoryStruct.id, Eq.symm, equivShrink, DFunLike.coe
-- 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)
x : P.obj (op X)
⊢ (fun (τ : Functor.obj shrinkYoneda.{w, v, u} X ⟶ P) ↦
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (τ.app (op X)) :
              (a : (fun (X : Type w) ↦ X) ((shrinkYoneda.{w, v, u}.obj X).obj (op X))) →
                (fun (X : Type w) ↦ X) (P.obj (op X)))
            ((equivShrink (Functor.obj (Functor.obj yoneda X) (op X)) :
                  (a : (yoneda.obj X).obj (op X)) → Shrink.{w, v} ((yoneda.obj X).obj (op X)))
                (𝟙 X) :
              Shrink.{w, v} (Functor.obj (Functor.obj yoneda X) (op X))) :
          (fun (X : Type w) ↦ X) (P.obj (op X))))
      ((fun (x : P.obj (op X)) ↦
          ({
              app := fun (Y : Cᵒᵖ) ↦
                ↾fun (f : Functor.obj.{v, w, u, w + 1} (Functor.obj shrinkYoneda.{w, v, u} X) Y) ↦
                  (ConcreteCategory.hom (FC := TypeCat.Fun)
                        (P.map
                          (Quiver.Hom.op
                            ((Equiv.symm (equivShrink (Functor.obj (Functor.obj yoneda X) Y)) :
                                (a : Shrink.{w, v} ((yoneda.obj X).obj Y)) → (yoneda.obj X).obj Y)
                              f))) :
                      (a : (fun (X : Type w) ↦ X) (P.obj (op X))) → (fun (X : Type w) ↦ X) (P.obj (op (unop Y))))
                    x,
              naturality := ⋯ } :
            NatTrans (Functor.obj shrinkYoneda.{w, v, u} X) P))
        x) =
    x

Tactic:
simp
-- 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)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (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)) g :
          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)))

Tactic:
simp [shrinkYonedaObjObjEquiv, shrinkYonedaEquiv, shrinkYoneda,
    ← comp_apply, ← NatTrans.naturality]

Premises used: CategoryTheory.shrinkYoneda, CategoryTheory.comp_apply, CategoryTheory.shrinkYonedaEquiv, CategoryTheory.NatTrans.naturality, CategoryTheory.shrinkYonedaObjObjEquiv