awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
F : C ⥤ Type v₁
f : obj coyoneda (op X) ⟶ F
⊢ Eq.{v₁ + 1} (α := F.obj X) ((coyonedaEquiv : (a : coyoneda.obj (op X) ⟶ F) → F.obj X) f : F.obj X)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app X) :
          (a : (fun (X : Type v₁) ↦ X) ((coyoneda.obj (op X)).obj X)) → (fun (X : Type v₁) ↦ X) (F.obj X))
        (𝟙 X) :
      (fun (X : Type v₁) ↦ X) (F.obj X))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
F : C ⥤ Type v₁
x : F.obj X
Y : C
f : X ⟶ Y
⊢ Eq (α := (fun (X : Type v₁) ↦ X) (F.obj Y))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (NatTrans.app ((Equiv.symm coyonedaEquiv : (a : F.obj X) → coyoneda.obj (op X) ⟶ F) x) Y) :
          (a : (fun (X : Type v₁) ↦ X) ((coyoneda.obj (op X)).obj Y)) → (fun (X : Type v₁) ↦ X) (F.obj Y))
        f :
      (fun (X : Type v₁) ↦ X) (F.obj Y))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
          (a : (fun (X : Type v₁) ↦ X) (F.obj X)) → (fun (X : Type v₁) ↦ X) (F.obj Y))
        x :
      (fun (X : Type v₁) ↦ X) (F.obj Y))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
F : C ⥤ Type v₁
f : obj coyoneda (op X) ⟶ F
g : X ⟶ Y
change :
  Eq (α := (fun (X : Type v₁) ↦ X) (F.obj Y))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app X ≫ F.map g) :
          (a : (fun (X : Type v₁) ↦ X) ((coyoneda.obj (op X)).obj X)) → (fun (X : Type v₁) ↦ X) (F.obj Y))
        (𝟙 X) :
      (fun (X : Type v₁) ↦ X) (F.obj Y))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app Y) :
          (a : (fun (X : Type v₁) ↦ X) ((coyoneda.obj (op X)).obj Y)) → (fun (X : Type v₁) ↦ X) (F.obj Y))
        (g ≫ 𝟙 Y) :
      (fun (X : Type v₁) ↦ X) (F.obj Y))
⊢ Eq (α := (fun (X : Type v₁) ↦ X) (F.obj Y))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g) :
          (a : (fun (X : Type v₁) ↦ X) (F.obj X)) → (fun (X : Type v₁) ↦ X) (F.obj Y))
        ((coyonedaEquiv : (a : coyoneda.obj (op X) ⟶ F) → F.obj X) f : F.obj X) :
      (fun (X : Type v₁) ↦ X) (F.obj Y))
    ((coyonedaEquiv : (a : coyoneda.obj (op Y) ⟶ F) → F.obj Y) (map coyoneda g.op ≫ f) : F.obj Y)

Tactic:
change (f.app X ≫ F.map g) (𝟙 X) = f.app Y (g ≫ 𝟙 Y)

Premises used: CategoryTheory.ConcreteCategory.hom, CategoryTheory.CategoryStruct.id, CategoryTheory.Functor.map, CategoryTheory.CategoryStruct.comp, DFunLike.coe, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
F : C ⥤ Type v₁
f : obj coyoneda (op X) ⟶ F
g : X ⟶ Y
rw :
  Eq (α := (fun (X : Type v₁) ↦ X) (F.obj Y))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (map (obj coyoneda (op X)) g ≫ f.app Y) :
          (a : (fun (X : Type v₁) ↦ X) ((coyoneda.obj (op X)).obj X)) → (fun (X : Type v₁) ↦ X) (F.obj Y))
        (𝟙 X) :
      (fun (X : Type v₁) ↦ X) (F.obj Y))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app Y) :
          (a : (fun (X : Type v₁) ↦ X) ((coyoneda.obj (op X)).obj Y)) → (fun (X : Type v₁) ↦ X) (F.obj Y))
        (g ≫ 𝟙 Y) :
      (fun (X : Type v₁) ↦ X) (F.obj Y))
⊢ Eq (α := (fun (X : Type v₁) ↦ X) (F.obj Y))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app X ≫ F.map g) :
          (a : (fun (X : Type v₁) ↦ X) ((coyoneda.obj (op X)).obj X)) → (fun (X : Type v₁) ↦ X) (F.obj Y))
        (𝟙 X) :
      (fun (X : Type v₁) ↦ X) (F.obj Y))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app Y) :
          (a : (fun (X : Type v₁) ↦ X) ((coyoneda.obj (op X)).obj Y)) → (fun (X : Type v₁) ↦ X) (F.obj Y))
        (g ≫ 𝟙 Y) :
      (fun (X : Type v₁) ↦ X) (F.obj Y))

Tactic:
rw [← f.naturality]

Premises used: CategoryTheory.NatTrans.naturality
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
F : C ⥤ Type v₁
f : obj coyoneda (op X) ⟶ F
g : X ⟶ Y
⊢ Eq (α := (fun (X : Type v₁) ↦ X) (F.obj Y))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (map (obj coyoneda (op X)) g ≫ f.app Y) :
          (a : (fun (X : Type v₁) ↦ X) ((coyoneda.obj (op X)).obj X)) → (fun (X : Type v₁) ↦ X) (F.obj Y))
        (𝟙 X) :
      (fun (X : Type v₁) ↦ X) (F.obj Y))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app Y) :
          (a : (fun (X : Type v₁) ↦ X) ((coyoneda.obj (op X)).obj Y)) → (fun (X : Type v₁) ↦ X) (F.obj Y))
        (g ≫ 𝟙 Y) :
      (fun (X : Type v₁) ↦ X) (F.obj Y))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
F G : C ⥤ Type v₁
α : obj coyoneda (op X) ⟶ F
β : F ⟶ G
⊢ Eq.{v₁ + 1} (α := G.obj X) ((coyonedaEquiv : (a : coyoneda.obj (op X) ⟶ G) → G.obj X) (α ≫ β) : G.obj X)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (β.app X) :
          (a : (fun (X : Type v₁) ↦ X) (F.obj X)) → (fun (X : Type v₁) ↦ X) (G.obj X))
        ((coyonedaEquiv : (a : coyoneda.obj (op X) ⟶ F) → F.obj X) α : F.obj X) :
      (fun (X : Type v₁) ↦ X) (G.obj X))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
rw :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (map coyoneda f.op) Y) :
        (a : (fun (X : Type v₁) ↦ X) ((coyoneda.obj (op Y)).obj Y)) →
          (fun (X : Type v₁) ↦ X) ((coyoneda.obj (op X)).obj Y))
      (𝟙 Y) =
    f
⊢ (coyonedaEquiv : (a : coyoneda.obj (op Y) ⟶ coyoneda.obj (op X)) → (coyoneda.obj (op X)).obj Y) (map coyoneda f.op) =
    f

Tactic:
rw [coyonedaEquiv_apply]

Premises used: CategoryTheory.coyonedaEquiv_apply
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (map coyoneda f.op) Y) :
        (a : (fun (X : Type v₁) ↦ X) ((coyoneda.obj (op Y)).obj Y)) →
          (fun (X : Type v₁) ↦ X) ((coyoneda.obj (op X)).obj Y))
      (𝟙 Y) =
    f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
F : C ⥤ Type v₁
f : obj coyoneda (op X) ⟶ F
g : X ⟶ Y
rw :
  Eq.{v₁ + 1} (α := (fun (X : Type v₁) ↦ X) (F.obj Y))
    ((coyonedaEquiv : (a : coyoneda.obj (op Y) ⟶ F) → F.obj Y) (map coyoneda g.op ≫ f) : F.obj Y)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app Y) :
          (a : (fun (X : Type v₁) ↦ X) ((coyoneda.obj (op X)).obj Y)) → (fun (X : Type v₁) ↦ X) (F.obj Y))
        g :
      (fun (X : Type v₁) ↦ X) (F.obj Y))
rw₁ :
  Eq (α := (fun (X : Type v₁) ↦ X) (F.obj Y))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app Y) :
          (a : (fun (X : Type v₁) ↦ X) ((coyoneda.obj (op X)).obj Y)) → (fun (X : Type v₁) ↦ X) (F.obj Y))
        ((coyonedaEquiv : (a : coyoneda.obj (op Y) ⟶ coyoneda.obj (op X)) → (coyoneda.obj (op X)).obj Y)
            (map coyoneda g.op) :
          obj (obj coyoneda (op X)) Y) :
      (fun (X : Type v₁) ↦ X) (F.obj Y))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app Y) :
          (a : (fun (X : Type v₁) ↦ X) ((coyoneda.obj (op X)).obj Y)) → (fun (X : Type v₁) ↦ X) (F.obj Y))
        g :
      (fun (X : Type v₁) ↦ X) (F.obj Y))
rw₂ rw₃ :
  Eq (α := (fun (X : Type v₁) ↦ X) (F.obj Y))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app Y) :
          (a : (fun (X : Type v₁) ↦ X) ((coyoneda.obj (op X)).obj Y)) → (fun (X : Type v₁) ↦ X) (F.obj Y))
        g :
      (fun (X : Type v₁) ↦ X) (F.obj Y))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app Y) :
          (a : (fun (X : Type v₁) ↦ X) ((coyoneda.obj (op X)).obj Y)) → (fun (X : Type v₁) ↦ X) (F.obj Y))
        g :
      (fun (X : Type v₁) ↦ X) (F.obj Y))
⊢ Eq (α := (fun (X : Type v₁) ↦ X) (F.obj Y))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g) :
          (a : (fun (X : Type v₁) ↦ X) (F.obj X)) → (fun (X : Type v₁) ↦ X) (F.obj Y))
        ((coyonedaEquiv : (a : coyoneda.obj (op X) ⟶ F) → F.obj X) f : F.obj X) :
      (fun (X : Type v₁) ↦ X) (F.obj Y))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app Y) :
          (a : (fun (X : Type v₁) ↦ X) ((coyoneda.obj (op X)).obj Y)) → (fun (X : Type v₁) ↦ X) (F.obj Y))
        g :
      (fun (X : Type v₁) ↦ X) (F.obj Y))

Tactic:
rw [coyonedaEquiv_naturality, coyonedaEquiv_comp, coyonedaEquiv_coyoneda_map]

Premises used: CategoryTheory.coyonedaEquiv_comp, CategoryTheory.coyonedaEquiv_naturality, CategoryTheory.coyonedaEquiv_coyoneda_map
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
F : C ⥤ Type v₁
t : F.obj X
obtain :
  ∀ (u : obj coyoneda (op X) ⟶ F),
    Eq (α := obj coyoneda (op Y) ⟶ F)
      ((Equiv.symm coyonedaEquiv : (a : F.obj Y) → coyoneda.obj (op Y) ⟶ F)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
              (a : (fun (X : Type v₁) ↦ X) (F.obj X)) → (fun (X : Type v₁) ↦ X) (F.obj Y))
            ((coyonedaEquiv : (a : coyoneda.obj (op X) ⟶ F) → F.obj X) u : F.obj X)) :
        obj coyoneda (op Y) ⟶ F)
      (map coyoneda f.op ≫
          (Equiv.symm coyonedaEquiv : (a : F.obj X) → coyoneda.obj (op X) ⟶ F)
            ((coyonedaEquiv : (a : coyoneda.obj (op X) ⟶ F) → F.obj X) u) :
        obj coyoneda (op Y) ⟶ F)
⊢ Eq (α := obj coyoneda (op Y) ⟶ F)
    ((Equiv.symm coyonedaEquiv : (a : F.obj Y) → coyoneda.obj (op Y) ⟶ F)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
            (a : (fun (X : Type v₁) ↦ X) (F.obj X)) → (fun (X : Type v₁) ↦ X) (F.obj Y))
          t) :
      obj coyoneda (op Y) ⟶ F)
    (map coyoneda f.op ≫ (Equiv.symm coyonedaEquiv : (a : F.obj X) → coyoneda.obj (op X) ⟶ F) t :
      obj coyoneda (op Y) ⟶ F)

Tactic:
obtain ⟨u, rfl⟩ := coyonedaEquiv.surjective t

Premises used: CategoryTheory.coyonedaEquiv, Equiv.surjective, rfl
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
F : C ⥤ Type v₁
u : obj coyoneda (op X) ⟶ F
⊢ Eq (α := obj coyoneda (op Y) ⟶ F)
    ((Equiv.symm coyonedaEquiv : (a : F.obj Y) → coyoneda.obj (op Y) ⟶ F)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
            (a : (fun (X : Type v₁) ↦ X) (F.obj X)) → (fun (X : Type v₁) ↦ X) (F.obj Y))
          ((coyonedaEquiv : (a : coyoneda.obj (op X) ⟶ F) → F.obj X) u : F.obj X)) :
      obj coyoneda (op Y) ⟶ F)
    (map coyoneda f.op ≫
        (Equiv.symm coyonedaEquiv : (a : F.obj X) → coyoneda.obj (op X) ⟶ F)
          ((coyonedaEquiv : (a : coyoneda.obj (op X) ⟶ F) → F.obj X) u) :
      obj coyoneda (op Y) ⟶ F)

Tactic:
simp [coyonedaEquiv_naturality u f]

Premises used: CategoryTheory.coyonedaEquiv_naturality
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P Q : C × (C ⥤ Type v₁)
α : P ⟶ Q
x : obj (coyonedaEvaluation C) P
⊢ Eq (α := obj (evaluationUncurried C (Type v₁)) Q)
    (ULift.down.{u₁, v₁}
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (map (coyonedaEvaluation C) α) :
            (a : (fun (X : Type (max u₁ v₁)) ↦ X) ((coyonedaEvaluation C).obj P)) →
              (fun (X : Type (max u₁ v₁)) ↦ X) ((coyonedaEvaluation C).obj Q))
          x) :
      obj (evaluationUncurried C (Type v₁)) Q)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (α.2.app Q.1) :
          (a : (fun (X : Type v₁) ↦ X) (P.2.obj Q.1)) → (fun (X : Type v₁) ↦ X) (Q.2.obj Q.1))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (P.2.map α.1) :
              (a : (fun (X : Type v₁) ↦ X) (P.2.obj P.1)) → (fun (X : Type v₁) ↦ X) (P.2.obj Q.1))
            x.down :
          (fun (X : Type v₁) ↦ X) (P.2.obj Q.1)) :
      (fun (X : Type v₁) ↦ X) (Q.2.obj Q.1))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C × (C ⥤ Type v₁)
x y : obj (coyonedaPairing C) X
w : ∀ (Y : C), x.app Y = y.app Y
⊢ x = y

Tactic:
NatTrans.ext (funext w)

Premises used: CategoryTheory.NatTrans.ext, funext
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P Q : C × (C ⥤ Type v₁)
α : P ⟶ Q
β : obj (coyonedaPairing C) P
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (map (coyonedaPairing C) α) :
        (a : (fun (X : Type (max u₁ v₁)) ↦ X) ((coyonedaPairing C).obj P)) →
          (fun (X : Type (max u₁ v₁)) ↦ X) ((coyonedaPairing C).obj Q))
      β =
    map coyoneda α.1.op ≫ β ≫ α.2

Tactic:
rfl

Premises used: CategoryTheory.NatTrans.vcomp, rfl
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
F : C ⥤ Type v₁
this :
  ∀ (Y : C) (G : C ⥤ Type v₁) (f : (X, F) ⟶ (Y, G)),
    Eq (α := obj (coyonedaPairing C) (X, F) ⟶ obj (coyonedaEvaluation C) (Y, G))
      (map (coyonedaPairing C) f ≫
        Iso.hom
          ((fun (x : C × (C ⥤ Type v₁)) ↦
              (Equiv.toIso (Equiv.trans coyonedaEquiv (Equiv.symm Equiv.ulift)) :
                obj (coyonedaPairing C) x ≅ obj (coyonedaEvaluation C) x))
            (Y, G)))
      (Iso.hom
          ((fun (x : C × (C ⥤ Type v₁)) ↦
              (Equiv.toIso (Equiv.trans coyonedaEquiv (Equiv.symm Equiv.ulift)) :
                obj (coyonedaPairing C) x ≅ obj (coyonedaEvaluation C) x))
            (X, F)) ≫
        map (coyonedaEvaluation C) f)
⊢ ∀ {Y : C × (C ⥤ Type v₁)} (f : (X, F) ⟶ Y),
    Eq (α := obj (coyonedaPairing C) (X, F) ⟶ obj (coyonedaEvaluation C) Y)
      (map (coyonedaPairing C) f ≫
        Iso.hom
          ((fun (x : C × (C ⥤ Type v₁)) ↦
              (Equiv.toIso (Equiv.trans coyonedaEquiv (Equiv.symm Equiv.ulift)) :
                obj (coyonedaPairing C) x ≅ obj (coyonedaEvaluation C) x))
            Y))
      (Iso.hom
          ((fun (x : C × (C ⥤ Type v₁)) ↦
              (Equiv.toIso (Equiv.trans coyonedaEquiv (Equiv.symm Equiv.ulift)) :
                obj (coyonedaPairing C) x ≅ obj (coyonedaEvaluation C) x))
            (X, F)) ≫
        map (coyonedaEvaluation C) f)

Tactic:
(Y, G)
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
F : C ⥤ Type v₁
Y : C
G : C ⥤ Type v₁
f : (X, F) ⟶ (Y, G)
h :
  ∀ (a : obj coyoneda (op X) ⟶ F),
    Eq (α := obj (coyonedaEvaluation C) (Y, G))
      (TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (map (coyonedaPairing C) f ≫
            Iso.hom
              ((fun (x : C × (C ⥤ Type v₁)) ↦
                  (Equiv.toIso (Equiv.trans coyonedaEquiv (Equiv.symm Equiv.ulift)) :
                    obj (coyonedaPairing C) x ≅ obj (coyonedaEvaluation C) x))
                (Y, G))))
        a)
      (TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (Iso.hom
              ((fun (x : C × (C ⥤ Type v₁)) ↦
                  (Equiv.toIso (Equiv.trans coyonedaEquiv (Equiv.symm Equiv.ulift)) :
                    obj (coyonedaPairing C) x ≅ obj (coyonedaEvaluation C) x))
                (X, F)) ≫
            map (coyonedaEvaluation C) f))
        a)
⊢ Eq (α := obj (coyonedaPairing C) (X, F) ⟶ obj (coyonedaEvaluation C) (Y, G))
    (map (coyonedaPairing C) f ≫
      Iso.hom
        ((fun (x : C × (C ⥤ Type v₁)) ↦
            (Equiv.toIso (Equiv.trans coyonedaEquiv (Equiv.symm Equiv.ulift)) :
              obj (coyonedaPairing C) x ≅ obj (coyonedaEvaluation C) x))
          (Y, G)))
    (Iso.hom
        ((fun (x : C × (C ⥤ Type v₁)) ↦
            (Equiv.toIso (Equiv.trans coyonedaEquiv (Equiv.symm Equiv.ulift)) :
              obj (coyonedaPairing C) x ≅ obj (coyonedaEvaluation C) x))
          (X, F)) ≫
      map (coyonedaEvaluation C) f)

Tactic:
ext (a : coyoneda.obj (op X) ⟶ F)

Premises used: CategoryTheory.coyoneda, Opposite.op, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
F : C ⥤ Type v₁
Y : C
G : C ⥤ Type v₁
f : (X, F) ⟶ (Y, G)
a : obj coyoneda (op X) ⟶ F
h :
  Eq.{v₁ + 1} (α := obj (evaluationUncurried C (Type v₁)) (Y, G))
    (ULift.down.{u₁, v₁}
      (TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (map (coyonedaPairing C) f ≫
            Iso.hom
              ((fun (x : C × (C ⥤ Type v₁)) ↦
                  (Equiv.toIso (Equiv.trans coyonedaEquiv (Equiv.symm Equiv.ulift)) :
                    obj (coyonedaPairing C) x ≅ obj (coyonedaEvaluation C) x))
                (Y, G))))
        a))
    (ULift.down.{u₁, v₁}
      (TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (Iso.hom
              ((fun (x : C × (C ⥤ Type v₁)) ↦
                  (Equiv.toIso (Equiv.trans coyonedaEquiv (Equiv.symm Equiv.ulift)) :
                    obj (coyonedaPairing C) x ≅ obj (coyonedaEvaluation C) x))
                (X, F)) ≫
            map (coyonedaEvaluation C) f))
        a))
⊢ Eq (α := obj (coyonedaEvaluation C) (Y, G))
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (map (coyonedaPairing C) f ≫
          Iso.hom
            ((fun (x : C × (C ⥤ Type v₁)) ↦
                (Equiv.toIso (Equiv.trans coyonedaEquiv (Equiv.symm Equiv.ulift)) :
                  obj (coyonedaPairing C) x ≅ obj (coyonedaEvaluation C) x))
              (Y, G))))
      a)
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (Iso.hom
            ((fun (x : C × (C ⥤ Type v₁)) ↦
                (Equiv.toIso (Equiv.trans coyonedaEquiv (Equiv.symm Equiv.ulift)) :
                  obj (coyonedaPairing C) x ≅ obj (coyonedaEvaluation C) x))
              (X, F)) ≫
          map (coyonedaEvaluation C) f))
      a)

Tactic:
apply ULift.ext

Premises used: ULift.ext
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
F : C ⥤ Type v₁
Y : C
G : C ⥤ Type v₁
f : (X, F) ⟶ (Y, G)
a : obj coyoneda (op X) ⟶ F
h :
  Eq (α := G.obj Y)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.2.app Y) : (a : F.obj Y) → G.obj Y)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (a.app Y) : (a : X ⟶ Y) → F.obj Y) (f.1 ≫ 𝟙 Y) : F.obj Y) :
      G.obj Y)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.2.app Y) : (a : F.obj Y) → G.obj Y)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f.1) : (a : F.obj X) → F.obj Y)
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (a.app X) : (a : X ⟶ X) → F.obj X) (𝟙 X) : F.obj X) :
          F.obj Y) :
      G.obj Y)
⊢ Eq.{v₁ + 1} (α := obj (evaluationUncurried C (Type v₁)) (Y, G))
    (ULift.down.{u₁, v₁}
      (TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (map (coyonedaPairing C) f ≫
            Iso.hom
              ((fun (x : C × (C ⥤ Type v₁)) ↦
                  (Equiv.toIso (Equiv.trans coyonedaEquiv (Equiv.symm Equiv.ulift)) :
                    obj (coyonedaPairing C) x ≅ obj (coyonedaEvaluation C) x))
                (Y, G))))
        a))
    (ULift.down.{u₁, v₁}
      (TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (Iso.hom
              ((fun (x : C × (C ⥤ Type v₁)) ↦
                  (Equiv.toIso (Equiv.trans coyonedaEquiv (Equiv.symm Equiv.ulift)) :
                    obj (coyonedaPairing C) x ≅ obj (coyonedaEvaluation C) x))
                (X, F)) ≫
            map (coyonedaEvaluation C) f))
        a))

Tactic:
dsimp [coyonedaEquiv, coyonedaEvaluation]

Premises used: CategoryTheory.coyonedaEquiv, CategoryTheory.coyonedaEvaluation
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
F : C ⥤ Type v₁
Y : C
G : C ⥤ Type v₁
f : (X, F) ⟶ (Y, G)
a : obj coyoneda (op X) ⟶ F
⊢ Eq (α := G.obj Y)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.2.app Y) : (a : F.obj Y) → G.obj Y)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (a.app Y) : (a : X ⟶ Y) → F.obj Y) (f.1 ≫ 𝟙 Y) : F.obj Y) :
      G.obj Y)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.2.app Y) : (a : F.obj Y) → G.obj Y)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f.1) : (a : F.obj X) → F.obj Y)
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (a.app X) : (a : X ⟶ X) → F.obj X) (𝟙 X) : F.obj X) :
          F.obj Y) :
      G.obj Y)

Tactic:
simp [← NatTrans.naturality_apply]

Premises used: CategoryTheory.NatTrans.naturality_apply
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C_1 : Type u₁
inst : Category.{v₁, u₁} C_1
C : Type u₁
inst_1 : SmallCategory C
X Y : C
f : X ⟶ Y
w :
  ∀ (a : C ⥤ Type u₁) (b : obj (obj (Functor.rightOp coyoneda ⋙ coyoneda) X) a),
    Eq (α := obj (obj (evaluation C (Type u₁)) Y) a)
      (TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (NatTrans.app
            (map (Functor.rightOp coyoneda ⋙ coyoneda) f ≫
              Iso.hom
                ((fun (X : C) ↦
                    (NatIso.ofComponents (fun (x : C ⥤ Type u₁) ↦ Equiv.toIso coyonedaEquiv) ⋯ :
                      Iso (C := (C ⥤ Type u₁) ⥤ Type u₁) (obj (Functor.rightOp coyoneda ⋙ coyoneda) X)
                        (obj (evaluation C (Type u₁)) X)))
                  Y))
            a))
        b)
      (TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (NatTrans.app
            (Iso.hom
                ((fun (X : C) ↦
                    (NatIso.ofComponents (fun (x : C ⥤ Type u₁) ↦ Equiv.toIso coyonedaEquiv) ⋯ :
                      Iso (C := (C ⥤ Type u₁) ⥤ Type u₁) (obj (Functor.rightOp coyoneda ⋙ coyoneda) X)
                        (obj (evaluation C (Type u₁)) X)))
                  X) ≫
              map (evaluation C (Type u₁)) f)
            a))
        b)
⊢ Eq (α :=
    Quiver.Hom (V := (C ⥤ Type u₁) ⥤ Type u₁) (obj (Functor.rightOp coyoneda ⋙ coyoneda) X)
      (obj (evaluation C (Type u₁)) Y))
    (map (Functor.rightOp coyoneda ⋙ coyoneda) f ≫
      Iso.hom
        ((fun (X : C) ↦
            (NatIso.ofComponents (fun (x : C ⥤ Type u₁) ↦ Equiv.toIso coyonedaEquiv) ⋯ :
              Iso (C := (C ⥤ Type u₁) ⥤ Type u₁) (obj (Functor.rightOp coyoneda ⋙ coyoneda) X)
                (obj (evaluation C (Type u₁)) X)))
          Y))
    (Iso.hom
        ((fun (X : C) ↦
            (NatIso.ofComponents (fun (x : C ⥤ Type u₁) ↦ Equiv.toIso coyonedaEquiv) ⋯ :
              Iso (C := (C ⥤ Type u₁) ⥤ Type u₁) (obj (Functor.rightOp coyoneda ⋙ coyoneda) X)
                (obj (evaluation C (Type u₁)) X)))
          X) ≫
      map (evaluation C (Type u₁)) f)

Tactic:
ext a b
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C_1 : Type u₁
inst : Category.{v₁, u₁} C_1
C : Type u₁
inst_1 : SmallCategory C
X Y : C
f : X ⟶ Y
a : C ⥤ Type u₁
b : obj (obj (Functor.rightOp coyoneda ⋙ coyoneda) X) a
⊢ Eq (α := obj (obj (evaluation C (Type u₁)) Y) a)
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (NatTrans.app
          (map (Functor.rightOp coyoneda ⋙ coyoneda) f ≫
            Iso.hom
              ((fun (X : C) ↦
                  (NatIso.ofComponents (fun (x : C ⥤ Type u₁) ↦ Equiv.toIso coyonedaEquiv) ⋯ :
                    Iso (C := (C ⥤ Type u₁) ⥤ Type u₁) (obj (Functor.rightOp coyoneda ⋙ coyoneda) X)
                      (obj (evaluation C (Type u₁)) X)))
                Y))
          a))
      b)
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (NatTrans.app
          (Iso.hom
              ((fun (X : C) ↦
                  (NatIso.ofComponents (fun (x : C ⥤ Type u₁) ↦ Equiv.toIso coyonedaEquiv) ⋯ :
                    Iso (C := (C ⥤ Type u₁) ⥤ Type u₁) (obj (Functor.rightOp coyoneda ⋙ coyoneda) X)
                      (obj (evaluation C (Type u₁)) X)))
                X) ≫
            map (evaluation C (Type u₁)) f)
          a))
      b)

Tactic:
simp [coyonedaEquiv, ← NatTrans.naturality_apply]

Premises used: CategoryTheory.NatTrans.naturality_apply, CategoryTheory.coyonedaEquiv