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 (max w v₁)
τ : obj uliftYoneda.{w, v₁, u₁} X ⟶ F
w :
  ∀ (Y : C) (y : obj (obj yoneda X) (op Y)),
    TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (NatTrans.app
            ((fun (x : F.obj (op X)) ↦
                {
                  app := fun (Y : Cᵒᵖ) ↦
                    ↾fun (y : obj (obj uliftYoneda.{w, v₁, u₁} X) Y) ↦
                      (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Quiver.Hom.op y.down)) :
                          (a : (fun (X : Type (max v₁ w)) ↦ X) (F.obj (op X))) →
                            (fun (X : Type (max v₁ w)) ↦ X) (F.obj (op (unop Y))))
                        x,
                  naturality := ⋯ : NatTrans (obj uliftYoneda.{w, v₁, u₁} X) F })
              ((fun (τ : obj uliftYoneda.{w, v₁, u₁} X ⟶ F) ↦
                  ((ConcreteCategory.hom (FC := TypeCat.Fun) (τ.app (op X)) :
                        (a : (fun (X : Type (max v₁ w)) ↦ X) ((uliftYoneda.{w, v₁, u₁}.obj X).obj (op X))) →
                          (fun (X : Type (max v₁ w)) ↦ X) (F.obj (op X)))
                      { down := 𝟙 (unop (op X)) : ULift.{w, v₁} (obj (obj yoneda X) (op X)) } :
                    (fun (X : Type (max v₁ w)) ↦ X) (F.obj (op X))))
                τ))
            (op Y)))
        { down := y : ULift.{w, v₁} (obj (obj yoneda X) (op Y)) } =
      TypeCat.Fun.toFun (ConcreteCategory.hom (FC := TypeCat.Fun) (τ.app (op Y)))
        { down := y : ULift.{w, v₁} (obj (obj yoneda X) (op Y)) }
⊢ (fun (x : F.obj (op X)) ↦
        {
          app := fun (Y : Cᵒᵖ) ↦
            ↾fun (y : obj (obj uliftYoneda.{w, v₁, u₁} X) Y) ↦
              (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Quiver.Hom.op y.down)) :
                  (a : (fun (X : Type (max v₁ w)) ↦ X) (F.obj (op X))) →
                    (fun (X : Type (max v₁ w)) ↦ X) (F.obj (op (unop Y))))
                x,
          naturality := ⋯ : NatTrans (obj uliftYoneda.{w, v₁, u₁} X) F })
      ((fun (τ : obj uliftYoneda.{w, v₁, u₁} X ⟶ F) ↦
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (τ.app (op X)) :
                (a : (fun (X : Type (max v₁ w)) ↦ X) ((uliftYoneda.{w, v₁, u₁}.obj X).obj (op X))) →
                  (fun (X : Type (max v₁ w)) ↦ X) (F.obj (op X)))
              { down := 𝟙 (unop (op X)) } :
            (fun (X : Type (max v₁ w)) ↦ X) (F.obj (op X))))
        τ) =
    τ

Tactic:
ext ⟨Y⟩ ⟨y⟩
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
F : Cᵒᵖ ⥤ Type (max w v₁)
τ : obj uliftYoneda.{w, v₁, u₁} X ⟶ F
Y : C
y : obj (obj yoneda X) (op Y)
⊢ TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (NatTrans.app
          ((fun (x : F.obj (op X)) ↦
              {
                app := fun (Y : Cᵒᵖ) ↦
                  ↾fun (y : obj (obj uliftYoneda.{w, v₁, u₁} X) Y) ↦
                    (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Quiver.Hom.op y.down)) :
                        (a : (fun (X : Type (max v₁ w)) ↦ X) (F.obj (op X))) →
                          (fun (X : Type (max v₁ w)) ↦ X) (F.obj (op (unop Y))))
                      x,
                naturality := ⋯ : NatTrans (obj uliftYoneda.{w, v₁, u₁} X) F })
            ((fun (τ : obj uliftYoneda.{w, v₁, u₁} X ⟶ F) ↦
                ((ConcreteCategory.hom (FC := TypeCat.Fun) (τ.app (op X)) :
                      (a : (fun (X : Type (max v₁ w)) ↦ X) ((uliftYoneda.{w, v₁, u₁}.obj X).obj (op X))) →
                        (fun (X : Type (max v₁ w)) ↦ X) (F.obj (op X)))
                    { down := 𝟙 (unop (op X)) : ULift.{w, v₁} (obj (obj yoneda X) (op X)) } :
                  (fun (X : Type (max v₁ w)) ↦ X) (F.obj (op X))))
              τ))
          (op Y)))
      { down := y : ULift.{w, v₁} (obj (obj yoneda X) (op Y)) } =
    TypeCat.Fun.toFun (ConcreteCategory.hom (FC := TypeCat.Fun) (τ.app (op Y)))
      { down := y : ULift.{w, v₁} (obj (obj yoneda X) (op Y)) }

Tactic:
simp [← NatTrans.naturality_apply]

Premises used: CategoryTheory.NatTrans.naturality_apply
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
F : Cᵒᵖ ⥤ Type (max w v₁)
x : F.obj (op X)
⊢ (fun (τ : obj uliftYoneda.{w, v₁, u₁} X ⟶ F) ↦
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (τ.app (op X)) :
              (a : (fun (X : Type (max v₁ w)) ↦ X) ((uliftYoneda.{w, v₁, u₁}.obj X).obj (op X))) →
                (fun (X : Type (max v₁ w)) ↦ X) (F.obj (op X)))
            { down := 𝟙 (unop (op X)) } :
          (fun (X : Type (max v₁ w)) ↦ X) (F.obj (op X))))
      ((fun (x : F.obj (op X)) ↦
          {
            app := fun (Y : Cᵒᵖ) ↦
              ↾fun (y : obj (obj uliftYoneda.{w, v₁, u₁} X) Y) ↦
                (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map (Quiver.Hom.op y.down)) :
                    (a : (fun (X : Type (max v₁ w)) ↦ X) (F.obj (op X))) →
                      (fun (X : Type (max v₁ w)) ↦ X) (F.obj (op (unop Y))))
                  x,
            naturality := ⋯ : NatTrans (obj uliftYoneda.{w, v₁, u₁} X) F })
        x) =
    x

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : Cᵒᵖ
F : Cᵒᵖ ⥤ Type (max w v₁)
f : obj uliftYoneda.{w, v₁, u₁} (unop X) ⟶ F
g : X ⟶ Y
⊢ Eq (α := (fun (X : Type (max v₁ w)) ↦ X) (F.obj Y))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g) :
          (a : (fun (X : Type (max v₁ w)) ↦ X) (F.obj X)) → (fun (X : Type (max v₁ w)) ↦ X) (F.obj Y))
        ((uliftYonedaEquiv : (a : uliftYoneda.{w, v₁, u₁}.obj (unop X) ⟶ F) → F.obj (op (unop X))) f) :
      (fun (X : Type (max v₁ w)) ↦ X) (F.obj Y))
    ((uliftYonedaEquiv : (a : uliftYoneda.{w, v₁, u₁}.obj (unop Y) ⟶ F) → F.obj (op (unop Y)))
        (map uliftYoneda.{w, v₁, u₁} g.unop ≫ f) :
      F.obj (op (unop Y)))

Tactic:
simp [uliftYonedaEquiv, uliftYoneda, ← f.naturality_apply]

Premises used: CategoryTheory.NatTrans.naturality_apply, CategoryTheory.uliftYoneda, CategoryTheory.uliftYonedaEquiv
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
F G : Cᵒᵖ ⥤ Type (max w v₁)
α : obj uliftYoneda.{w, v₁, u₁} X ⟶ F
β : F ⟶ G
⊢ Eq (α := G.obj (op X))
    ((uliftYonedaEquiv : (a : uliftYoneda.{w, v₁, u₁}.obj X ⟶ G) → G.obj (op X)) (α ≫ β) : G.obj (op X))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (β.app (op X)) :
          (a : (fun (X : Type (max v₁ w)) ↦ X) (F.obj (op X))) → (fun (X : Type (max v₁ w)) ↦ X) (G.obj (op X)))
        ((uliftYonedaEquiv : (a : uliftYoneda.{w, v₁, u₁}.obj X ⟶ F) → F.obj (op X)) α) :
      (fun (X : Type (max v₁ w)) ↦ X) (G.obj (op X)))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : Cᵒᵖ
f : X ⟶ Y
F : Cᵒᵖ ⥤ Type (max w v₁)
t : F.obj X
obtain :
  ∀ (u : obj uliftYoneda.{w, v₁, u₁} (unop X) ⟶ F),
    Eq (α := obj uliftYoneda.{w, v₁, u₁} (unop Y) ⟶ F)
      ((Equiv.symm uliftYonedaEquiv : (a : F.obj (op (unop Y))) → uliftYoneda.{w, v₁, u₁}.obj (unop Y) ⟶ F)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
              (a : (fun (X : Type (max v₁ w)) ↦ X) (F.obj X)) → (fun (X : Type (max v₁ w)) ↦ X) (F.obj Y))
            ((uliftYonedaEquiv : (a : uliftYoneda.{w, v₁, u₁}.obj (unop X) ⟶ F) → F.obj (op (unop X))) u)) :
        obj uliftYoneda.{w, v₁, u₁} (unop Y) ⟶ F)
      (map uliftYoneda.{w, v₁, u₁} f.unop ≫
          (Equiv.symm uliftYonedaEquiv : (a : F.obj (op (unop X))) → uliftYoneda.{w, v₁, u₁}.obj (unop X) ⟶ F)
            ((uliftYonedaEquiv : (a : uliftYoneda.{w, v₁, u₁}.obj (unop X) ⟶ F) → F.obj (op (unop X))) u) :
        obj uliftYoneda.{w, v₁, u₁} (unop Y) ⟶ F)
⊢ Eq (α := obj uliftYoneda.{w, v₁, u₁} (unop Y) ⟶ F)
    ((Equiv.symm uliftYonedaEquiv : (a : F.obj (op (unop Y))) → uliftYoneda.{w, v₁, u₁}.obj (unop Y) ⟶ F)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map f) :
            (a : (fun (X : Type (max v₁ w)) ↦ X) (F.obj X)) → (fun (X : Type (max v₁ w)) ↦ X) (F.obj Y))
          t) :
      obj uliftYoneda.{w, v₁, u₁} (unop Y) ⟶ F)
    (map uliftYoneda.{w, v₁, u₁} f.unop ≫
        (Equiv.symm uliftYonedaEquiv : (a : F.obj (op (unop X))) → uliftYoneda.{w, v₁, u₁}.obj (unop X) ⟶ F) t :
      obj uliftYoneda.{w, v₁, u₁} (unop Y) ⟶ F)

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

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

Tactic:
rw [uliftYonedaEquiv_naturality]

Premises used: CategoryTheory.uliftYonedaEquiv_naturality
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : Cᵒᵖ
f : X ⟶ Y
F : Cᵒᵖ ⥤ Type (max w v₁)
u : obj uliftYoneda.{w, v₁, u₁} (unop X) ⟶ F
⊢ Eq (α := obj uliftYoneda.{w, v₁, u₁} (unop Y) ⟶ F)
    ((Equiv.symm uliftYonedaEquiv : (a : F.obj (op (unop Y))) → uliftYoneda.{w, v₁, u₁}.obj (unop Y) ⟶ F)
        ((uliftYonedaEquiv : (a : uliftYoneda.{w, v₁, u₁}.obj (unop Y) ⟶ F) → F.obj (op (unop Y)))
          (map uliftYoneda.{w, v₁, u₁} f.unop ≫ u)) :
      obj uliftYoneda.{w, v₁, u₁} (unop Y) ⟶ F)
    (map uliftYoneda.{w, v₁, u₁} f.unop ≫
        (Equiv.symm uliftYonedaEquiv : (a : F.obj (op (unop X))) → uliftYoneda.{w, v₁, u₁}.obj (unop X) ⟶ F)
          ((uliftYonedaEquiv : (a : uliftYoneda.{w, v₁, u₁}.obj (unop X) ⟶ F) → F.obj (op (unop X))) u) :
      obj uliftYoneda.{w, v₁, u₁} (unop Y) ⟶ F)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
F G : Cᵒᵖ ⥤ Type (max w v₁)
X : Cᵒᵖ
x : F.obj X
f : F ⟶ G
rw :
  Eq (α := G.obj (op (unop X)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op (unop X))) :
          (a : (fun (X : Type (max v₁ w)) ↦ X) (F.obj (op (unop X)))) →
            (fun (X : Type (max v₁ w)) ↦ X) (G.obj (op (unop X))))
        ((uliftYonedaEquiv : (a : uliftYoneda.{w, v₁, u₁}.obj (unop X) ⟶ F) → F.obj (op (unop X)))
          ((Equiv.symm uliftYonedaEquiv : (a : F.obj (op (unop X))) → uliftYoneda.{w, v₁, u₁}.obj (unop X) ⟶ F) x)) :
      (fun (X : Type (max v₁ w)) ↦ X) (G.obj (op (unop X))))
    ((uliftYonedaEquiv : (a : uliftYoneda.{w, v₁, u₁}.obj (unop X) ⟶ G) → G.obj (op (unop X)))
        ((Equiv.symm uliftYonedaEquiv : (a : G.obj (op (unop X))) → uliftYoneda.{w, v₁, u₁}.obj (unop X) ⟶ G)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op (unop X))) :
              (a : (fun (X : Type (max v₁ w)) ↦ X) (F.obj (op (unop X)))) →
                (fun (X : Type (max v₁ w)) ↦ X) (G.obj (op (unop X))))
            x)) :
      G.obj (op (unop X)))
⊢ Eq (α := G.obj (op (unop X)))
    ((uliftYonedaEquiv : (a : uliftYoneda.{w, v₁, u₁}.obj (unop X) ⟶ G) → G.obj (op (unop X)))
        ((Equiv.symm uliftYonedaEquiv : (a : F.obj (op (unop X))) → uliftYoneda.{w, v₁, u₁}.obj (unop X) ⟶ F) x ≫ f) :
      G.obj (op (unop X)))
    ((uliftYonedaEquiv : (a : uliftYoneda.{w, v₁, u₁}.obj (unop X) ⟶ G) → G.obj (op (unop X)))
        ((Equiv.symm uliftYonedaEquiv : (a : G.obj (op (unop X))) → uliftYoneda.{w, v₁, u₁}.obj (unop X) ⟶ G)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op (unop X))) :
              (a : (fun (X : Type (max v₁ w)) ↦ X) (F.obj (op (unop X)))) →
                (fun (X : Type (max v₁ w)) ↦ X) (G.obj (op (unop X))))
            x)) :
      G.obj (op (unop X)))

Tactic:
rw [uliftYonedaEquiv_comp]

Premises used: CategoryTheory.uliftYonedaEquiv_comp
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
F G : Cᵒᵖ ⥤ Type (max w v₁)
X : Cᵒᵖ
x : F.obj X
f : F ⟶ G
⊢ Eq (α := G.obj (op (unop X)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op (unop X))) :
          (a : (fun (X : Type (max v₁ w)) ↦ X) (F.obj (op (unop X)))) →
            (fun (X : Type (max v₁ w)) ↦ X) (G.obj (op (unop X))))
        ((uliftYonedaEquiv : (a : uliftYoneda.{w, v₁, u₁}.obj (unop X) ⟶ F) → F.obj (op (unop X)))
          ((Equiv.symm uliftYonedaEquiv : (a : F.obj (op (unop X))) → uliftYoneda.{w, v₁, u₁}.obj (unop X) ⟶ F) x)) :
      (fun (X : Type (max v₁ w)) ↦ X) (G.obj (op (unop X))))
    ((uliftYonedaEquiv : (a : uliftYoneda.{w, v₁, u₁}.obj (unop X) ⟶ G) → G.obj (op (unop X)))
        ((Equiv.symm uliftYonedaEquiv : (a : G.obj (op (unop X))) → uliftYoneda.{w, v₁, u₁}.obj (unop X) ⟶ G)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (op (unop X))) :
              (a : (fun (X : Type (max v₁ w)) ↦ X) (F.obj (op (unop X)))) →
                (fun (X : Type (max v₁ w)) ↦ X) (G.obj (op (unop X))))
            x)) :
      G.obj (op (unop X)))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
⊢ (uliftYonedaEquiv : (a : uliftYoneda.{w, v₁, u₁}.obj X ⟶ uliftYoneda.{w, v₁, u₁}.obj Y) → ULift.{w, v₁} (X ⟶ Y))
      (map uliftYoneda.{w, v₁, u₁} f) =
    { down := f : ULift.{w, v₁} (X ⟶ Y) }

Tactic:
simp [uliftYonedaEquiv, uliftYoneda]

Premises used: CategoryTheory.uliftYoneda, CategoryTheory.uliftYonedaEquiv
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P Q : Cᵒᵖ ⥤ Type (max w v₁)
f g : P ⟶ Q
h : ∀ (X : C) (p : obj uliftYoneda.{w, v₁, u₁} X ⟶ P), p ≫ f = p ≫ g
w :
  ∀ (X : Cᵒᵖ) (x : P.obj X),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (f.app X)).toFun x =
      (ConcreteCategory.hom (FC := TypeCat.Fun) (g.app X)).toFun x
⊢ f = g

Tactic:
ext X x
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P Q : Cᵒᵖ ⥤ Type (max w v₁)
f g : P ⟶ Q
h : ∀ (X : C) (p : obj uliftYoneda.{w, v₁, u₁} X ⟶ P), p ≫ f = p ≫ g
X : Cᵒᵖ
x : P.obj X
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (f.app X)).toFun x =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (g.app X)).toFun x

Tactic:
simpa [-op_unop, uliftYonedaEquiv_comp] using
    congr_arg uliftYonedaEquiv.{w} (h _ (uliftYonedaEquiv.symm x))

Premises used: Opposite.op_unop, CategoryTheory.uliftYonedaEquiv_comp
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C_1 : Type u₁
inst : Category.{v₁, u₁} C_1
C : Type u₁
inst_1 : Category.{v₁, u₁} C
X : Cᵒᵖ
Y Z : Cᵒᵖ ⥤ Type (max w v₁)
f : Y ⟶ Z
g : obj (obj (Functor.op uliftYoneda.{w, v₁, u₁} ⋙ coyoneda) X) Y
⊢ Eq (α := obj (obj (evaluation Cᵒᵖ (Type (max v₁ w))) X) Z)
    (ULift.down
      (TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (map (obj (Functor.op uliftYoneda.{w, v₁, u₁} ⋙ coyoneda) X) f ≫
            Iso.hom
              ((fun (x : Cᵒᵖ ⥤ Type (max w v₁)) ↦
                  (Equiv.toIso (Equiv.trans uliftYonedaEquiv (Equiv.symm Equiv.ulift)) :
                    obj (obj (Functor.op uliftYoneda.{w, v₁, u₁} ⋙ coyoneda) X) x ≅
                      obj
                        (obj
                          (evaluation Cᵒᵖ (Type (max v₁ w)) ⋙
                            obj (whiskeringRight (Cᵒᵖ ⥤ Type (max v₁ w)) (Type (max v₁ w)) (Type (max (max w u₁) v₁)))
                              uliftFunctor.{u₁, max v₁ w})
                          X)
                        x))
                Z)))
        g))
    (ULift.down
      (TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (Iso.hom
              ((fun (x : Cᵒᵖ ⥤ Type (max w v₁)) ↦
                  (Equiv.toIso (Equiv.trans uliftYonedaEquiv (Equiv.symm Equiv.ulift)) :
                    obj (obj (Functor.op uliftYoneda.{w, v₁, u₁} ⋙ coyoneda) X) x ≅
                      obj
                        (obj
                          (evaluation Cᵒᵖ (Type (max v₁ w)) ⋙
                            obj (whiskeringRight (Cᵒᵖ ⥤ Type (max v₁ w)) (Type (max v₁ w)) (Type (max (max w u₁) v₁)))
                              uliftFunctor.{u₁, max v₁ w})
                          X)
                        x))
                Y) ≫
            map
              (obj
                (evaluation Cᵒᵖ (Type (max v₁ w)) ⋙
                  obj (whiskeringRight (Cᵒᵖ ⥤ Type (max v₁ w)) (Type (max v₁ w)) (Type (max (max w u₁) v₁)))
                    uliftFunctor.{u₁, max v₁ w})
                X)
              f))
        g))

Tactic:
simpa using uliftYonedaEquiv_comp _ _

Premises used: CategoryTheory.uliftYonedaEquiv_comp
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C_1 : Type u₁
inst : Category.{v₁, u₁} C_1
C : Type u₁
inst_1 : Category.{v₁, u₁} C
Y Z : Cᵒᵖ
f : Y ⟶ Z
F : Cᵒᵖ ⥤ Type (max w v₁)
g : obj (obj (Functor.op uliftYoneda.{w, v₁, u₁} ⋙ coyoneda) Y) F
⊢ Eq (α := obj (obj (evaluation Cᵒᵖ (Type (max v₁ w))) Z) F)
    (ULift.down
      (TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (NatTrans.app
            (map (Functor.op uliftYoneda.{w, v₁, u₁} ⋙ coyoneda) f ≫
              Iso.hom
                ((fun (X : Cᵒᵖ) ↦
                    (NatIso.ofComponents
                        (fun (x : Cᵒᵖ ⥤ Type (max w v₁)) ↦
                          Equiv.toIso (Equiv.trans uliftYonedaEquiv (Equiv.symm Equiv.ulift)))
                        ⋯ :
                      Iso (C := (Cᵒᵖ ⥤ Type (max w v₁)) ⥤ Type (max (max w u₁) v₁))
                        (obj (Functor.op uliftYoneda.{w, v₁, u₁} ⋙ coyoneda) X)
                        (obj
                          (evaluation Cᵒᵖ (Type (max v₁ w)) ⋙
                            obj (whiskeringRight (Cᵒᵖ ⥤ Type (max v₁ w)) (Type (max v₁ w)) (Type (max (max w u₁) v₁)))
                              uliftFunctor.{u₁, max v₁ w})
                          X)))
                  Z))
            F))
        g))
    (ULift.down
      (TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (NatTrans.app
            (Iso.hom
                ((fun (X : Cᵒᵖ) ↦
                    (NatIso.ofComponents
                        (fun (x : Cᵒᵖ ⥤ Type (max w v₁)) ↦
                          Equiv.toIso (Equiv.trans uliftYonedaEquiv (Equiv.symm Equiv.ulift)))
                        ⋯ :
                      Iso (C := (Cᵒᵖ ⥤ Type (max w v₁)) ⥤ Type (max (max w u₁) v₁))
                        (obj (Functor.op uliftYoneda.{w, v₁, u₁} ⋙ coyoneda) X)
                        (obj
                          (evaluation Cᵒᵖ (Type (max v₁ w)) ⋙
                            obj (whiskeringRight (Cᵒᵖ ⥤ Type (max v₁ w)) (Type (max v₁ w)) (Type (max (max w u₁) v₁)))
                              uliftFunctor.{u₁, max v₁ w})
                          X)))
                  Y) ≫
              map
                (evaluation Cᵒᵖ (Type (max v₁ w)) ⋙
                  obj (whiskeringRight (Cᵒᵖ ⥤ Type (max v₁ w)) (Type (max v₁ w)) (Type (max (max w u₁) v₁)))
                    uliftFunctor.{u₁, max v₁ w})
                f)
            F))
        g))

Tactic:
simpa using (uliftYonedaEquiv_naturality _ _).symm

Premises used: Eq.symm
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
F : C ⥤ Type v₁
η : obj coyoneda (op X) ⟶ F
w :
  ∀ (Y : C) (x : X ⟶ Y),
    TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (NatTrans.app
            ((fun (ξ : F.obj X) ↦
                {
                  app := fun (x : C) ↦
                    ↾fun (x_1 : obj (obj coyoneda (op X)) x) ↦
                      (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map x_1) :
                          (a : (fun (X : Type v₁) ↦ X) (F.obj (unop (op X)))) → (fun (X : Type v₁) ↦ X) (F.obj x))
                        ξ,
                  naturality := ⋯ : NatTrans (obj coyoneda (op X)) F })
              ((fun (η : obj coyoneda (op X) ⟶ F) ↦
                  ((ConcreteCategory.hom (FC := TypeCat.Fun) (η.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)))
                η))
            Y))
        x =
      (ConcreteCategory.hom (FC := TypeCat.Fun) (η.app Y)).toFun x
⊢ (fun (ξ : F.obj X) ↦
        {
          app := fun (x : C) ↦
            ↾fun (x_1 : obj (obj coyoneda (op X)) x) ↦
              (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map x_1) :
                  (a : (fun (X : Type v₁) ↦ X) (F.obj (unop (op X)))) → (fun (X : Type v₁) ↦ X) (F.obj x))
                ξ,
          naturality := ⋯ : NatTrans (obj coyoneda (op X)) F })
      ((fun (η : obj coyoneda (op X) ⟶ F) ↦
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (η.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:
ext Y (x : X ⟶ Y)
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
F : C ⥤ Type v₁
η : obj coyoneda (op X) ⟶ F
Y : C
x : X ⟶ Y
⊢ TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (NatTrans.app
          ((fun (ξ : F.obj X) ↦
              {
                app := fun (x : C) ↦
                  ↾fun (x_1 : obj (obj coyoneda (op X)) x) ↦
                    (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map x_1) :
                        (a : (fun (X : Type v₁) ↦ X) (F.obj (unop (op X)))) → (fun (X : Type v₁) ↦ X) (F.obj x))
                      ξ,
                naturality := ⋯ : NatTrans (obj coyoneda (op X)) F })
            ((fun (η : obj coyoneda (op X) ⟶ F) ↦
                ((ConcreteCategory.hom (FC := TypeCat.Fun) (η.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)))
              η))
          Y))
      x =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (η.app Y)).toFun x

Tactic:
simp [← NatTrans.naturality_apply]

Premises used: CategoryTheory.NatTrans.naturality_apply
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
F : C ⥤ Type v₁
ξ : F.obj X
⊢ (fun (η : obj coyoneda (op X) ⟶ F) ↦
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (η.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)))
      ((fun (ξ : F.obj X) ↦
          {
            app := fun (x : C) ↦
              ↾fun (x_1 : obj (obj coyoneda (op X)) x) ↦
                (ConcreteCategory.hom (FC := TypeCat.Fun) (F.map x_1) :
                    (a : (fun (X : Type v₁) ↦ X) (F.obj (unop (op X)))) → (fun (X : Type v₁) ↦ X) (F.obj x))
                  ξ,
            naturality := ⋯ : NatTrans (obj coyoneda (op X)) F })
        ξ) =
    ξ

Tactic:
simp