awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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.rightOp uliftCoyoneda.{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.rightOp uliftCoyoneda.{w, v₁, u₁} ⋙ coyoneda) X) f ≫
            Iso.hom
              ((fun (x : C ⥤ Type (max w v₁)) ↦
                  (Equiv.toIso (Equiv.trans uliftCoyonedaEquiv (Equiv.symm Equiv.ulift)) :
                    obj (obj (Functor.rightOp uliftCoyoneda.{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 uliftCoyonedaEquiv (Equiv.symm Equiv.ulift)) :
                    obj (obj (Functor.rightOp uliftCoyoneda.{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 uliftCoyonedaEquiv_comp _ _

Premises used: CategoryTheory.uliftCoyonedaEquiv_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.rightOp uliftCoyoneda.{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.rightOp uliftCoyoneda.{w, v₁, u₁} ⋙ coyoneda) f ≫
              Iso.hom
                ((fun (X : C) ↦
                    (NatIso.ofComponents
                        (fun (x : C ⥤ Type (max w v₁)) ↦
                          Equiv.toIso (Equiv.trans uliftCoyonedaEquiv (Equiv.symm Equiv.ulift)))
                        ⋯ :
                      Iso (C := (C ⥤ Type (max w v₁)) ⥤ Type (max (max w u₁) v₁))
                        (obj (Functor.rightOp uliftCoyoneda.{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 uliftCoyonedaEquiv (Equiv.symm Equiv.ulift)))
                        ⋯ :
                      Iso (C := (C ⥤ Type (max w v₁)) ⥤ Type (max (max w u₁) v₁))
                        (obj (Functor.rightOp uliftCoyoneda.{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 (uliftCoyonedaEquiv_naturality _ _).symm

Premises used: CategoryTheory.uliftCoyonedaEquiv_naturality, Eq.symm
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u_1
inst_1 : Category.{v₁, u_1} D
F : Functor.{v₁, v₁, u₁, u_1} C D
Y : C
X : Cᵒᵖ
f : unop X ⟶ Y
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) ((yonedaMap F Y).app X) : (a : unop X ⟶ Y) → F.obj (unop X) ⟶ F.obj Y) f =
    F.map f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
Y : C
X : Cᵒᵖ
f : unop X ⟶ Y
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) ((uliftYonedaMap.{w, v₁, v₂, u₁, u₂} F Y).app X) :
        (a : ULift.{max v₂ w, v₁} (unop X ⟶ Y)) → ULift.{max v₁ w, v₂} (F.obj (unop X) ⟶ F.obj Y))
      { down := f } =
    { down := F.map f : ULift.{max v₁ w, v₂} (F.obj (unop X) ⟶ F.obj Y) }

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C_1 : Type u₁
inst : Category.{v₁, u₁} C_1
C : Type u₁
inst_1 : Category.{v₁, u₁} C
F : Functor.{v₁, u₂, u₁, u₂ + 1} C (Type u₂)
X : Type u₂
inst_2 : Unique X
s : (↑F.sections : Type (max u₁ u₂))
x x_1 : C
x_2 : x ⟶ x_1
h :
  ∀ (x_3 : obj.{v₁, u₂, u₁, u₂ + 1} (obj (const C) X) x),
    TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (map (obj (const C) X) x_2 ≫
            ↾fun (x : obj.{v₁, u₂, u₁, u₂ + 1} (obj (const C) X) x_1) ↦ (↑s : (j : C) → F.obj j) x_1))
        x_3 =
      TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          ((↾fun (x_4 : obj.{v₁, u₂, u₁, u₂ + 1} (obj (const C) X) x) ↦ (↑s : (j : C) → F.obj j) x) ≫ F.map x_2))
        x_3
⊢ Eq (α := obj.{v₁, u₂, u₁, u₂ + 1} (obj (const C) X) x ⟶ F.obj x_1)
    (map (obj (const C) X) x_2 ≫
      ↾fun (x : obj.{v₁, u₂, u₁, u₂ + 1} (obj (const C) X) x_1) ↦ (↑s : (j : C) → F.obj j) x_1)
    ((↾fun (x_3 : obj.{v₁, u₂, u₁, u₂ + 1} (obj (const C) X) x) ↦ (↑s : (j : C) → F.obj j) x) ≫ F.map x_2)

Tactic:
ext x
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C_1 : Type u₁
inst : Category.{v₁, u₁} C_1
C : Type u₁
inst_1 : Category.{v₁, u₁} C
F : Functor.{v₁, u₂, u₁, u₂ + 1} C (Type u₂)
X : Type u₂
inst_2 : Unique X
s : (↑F.sections : Type (max u₁ u₂))
x_1 x_2 : C
x_3 : x_1 ⟶ x_2
x : obj.{v₁, u₂, u₁, u₂ + 1} (obj (const C) X) x_1
⊢ TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (map (obj (const C) X) x_3 ≫
          ↾fun (x : obj.{v₁, u₂, u₁, u₂ + 1} (obj (const C) X) x_2) ↦ (↑s : (j : C) → F.obj j) x_2))
      x =
    TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        ((↾fun (x : obj.{v₁, u₂, u₁, u₂ + 1} (obj (const C) X) x_1) ↦ (↑s : (j : C) → F.obj j) x_1) ≫ F.map x_3))
      x

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C_1 : Type u₁
inst : Category.{v₁, u₁} C_1
C : Type u₁
inst_1 : Category.{v₁, u₁} C
F : Functor.{v₁, u₂, u₁, u₂ + 1} C (Type u₂)
X : Type u₂
inst_2 : Unique X
τ : obj (const C) X ⟶ F
refine :
  ∀ {j j' : C} (φ : j ⟶ j'),
    Eq (α := (fun (X : Type u₂) ↦ X) (F.obj j'))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map φ) :
            (a : (fun (X : Type u₂) ↦ X) (F.obj j)) → (fun (X : Type u₂) ↦ X) (F.obj j'))
          ((fun (j : C) ↦
              ((ConcreteCategory.hom (FC := TypeCat.Fun) (τ.app j) :
                    (a : (fun (X : Type u₂) ↦ X) (((const C).obj X).obj j)) → (fun (X : Type u₂) ↦ X) (F.obj j))
                  default :
                (fun (X : Type u₂) ↦ X) (F.obj j)))
            j) :
        (fun (X : Type u₂) ↦ X) (F.obj j'))
      ((fun (j : C) ↦
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (τ.app j) :
                  (a : (fun (X : Type u₂) ↦ X) (((const C).obj X).obj j)) → (fun (X : Type u₂) ↦ X) (F.obj j))
                default :
              (fun (X : Type u₂) ↦ X) (F.obj j)))
          j' :
        (fun (X : Type u₂) ↦ X) (F.obj j'))
⊢ (↑F.sections : Type (max u₁ u₂))

Tactic:
refine ⟨fun j ↦ τ.app _ (default : X), fun φ ↦ ?_⟩
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C_1 : Type u₁
inst : Category.{v₁, u₁} C_1
C : Type u₁
inst_1 : Category.{v₁, u₁} C
F : Functor.{v₁, u₂, u₁, u₂ + 1} C (Type u₂)
X : Type u₂
inst_2 : Unique X
τ : obj (const C) X ⟶ F
j j' : C
φ : j ⟶ j'
simp :
  Eq (α := F.obj j')
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 X ≫ τ.app j') : (a : ((const C).obj X).obj j) → F.obj j') default :
      F.obj j')
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (τ.app j') : (a : ((const C).obj X).obj j') → F.obj j') default :
      F.obj j')
⊢ Eq (α := (fun (X : Type u₂) ↦ X) (F.obj j'))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map φ) :
          (a : (fun (X : Type u₂) ↦ X) (F.obj j)) → (fun (X : Type u₂) ↦ X) (F.obj j'))
        ((fun (j : C) ↦
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (τ.app j) :
                  (a : (fun (X : Type u₂) ↦ X) (((const C).obj X).obj j)) → (fun (X : Type u₂) ↦ X) (F.obj j))
                default :
              (fun (X : Type u₂) ↦ X) (F.obj j)))
          j) :
      (fun (X : Type u₂) ↦ X) (F.obj j'))
    ((fun (j : C) ↦
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (τ.app j) :
                (a : (fun (X : Type u₂) ↦ X) (((const C).obj X).obj j)) → (fun (X : Type u₂) ↦ X) (F.obj j))
              default :
            (fun (X : Type u₂) ↦ X) (F.obj j)))
        j' :
      (fun (X : Type u₂) ↦ X) (F.obj j'))

Tactic:
simp [-const_obj_obj, ← comp_apply, -types_comp_apply, ← NatTrans.naturality]

Premises used: CategoryTheory.comp_apply, CategoryTheory.NatTrans.naturality, CategoryTheory.Functor.const_obj_obj, CategoryTheory.types_comp_apply
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C_1 : Type u₁
inst : Category.{v₁, u₁} C_1
C : Type u₁
inst_1 : Category.{v₁, u₁} C
F : Functor.{v₁, u₂, u₁, u₂ + 1} C (Type u₂)
X : Type u₂
inst_2 : Unique X
τ : obj (const C) X ⟶ F
j j' : C
φ : j ⟶ j'
⊢ Eq (α := F.obj j')
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 X ≫ τ.app j') : (a : ((const C).obj X).obj j) → F.obj j') default :
      F.obj j')
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (τ.app j') : (a : ((const C).obj X).obj j') → F.obj j') default :
      F.obj j')

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C_1 : Type u₁
inst : Category.{v₁, u₁} C_1
C : Type u₁
inst_1 : Category.{v₁, u₁} C
F : Functor.{v₁, u₂, u₁, u₂ + 1} C (Type u₂)
X : Type u₂
inst_2 : Unique X
τ : obj (const C) X ⟶ F
w :
  ∀ (x : C) (x_1 : X),
    TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (NatTrans.app
            ((fun (s : (↑F.sections : Type (max u₁ u₂))) ↦
                ({
                    app := fun (j : C) ↦
                      ↾fun (x : obj.{v₁, u₂, u₁, u₂ + 1} (obj (const C) X) j) ↦ (↑s : (j : C) → F.obj j) j,
                    naturality := ⋯ } :
                  NatTrans (obj (const C) X) F))
              ((fun (τ : obj (const C) X ⟶ F) ↦
                  (Subtype.mk (p := fun (x : (j : C) → F.obj j) ↦ x ∈ F.sections)
                      (fun (j : C) ↦
                        (ConcreteCategory.hom (FC := TypeCat.Fun) (τ.app j) :
                            (a : (fun (X : Type u₂) ↦ X) (((const C).obj X).obj j)) → (fun (X : Type u₂) ↦ X) (F.obj j))
                          default)
                      ⋯ :
                    { x : (j : C) → F.obj j // x ∈ F.sections }))
                τ))
            x))
        x_1 =
      (ConcreteCategory.hom (FC := TypeCat.Fun) (τ.app x)).toFun x_1
⊢ (fun (s : (↑F.sections : Type (max u₁ u₂))) ↦
        ({ app := fun (j : C) ↦ ↾fun (x : obj.{v₁, u₂, u₁, u₂ + 1} (obj (const C) X) j) ↦ (↑s : (j : C) → F.obj j) j,
            naturality := ⋯ } :
          NatTrans (obj (const C) X) F))
      ((fun (τ : obj (const C) X ⟶ F) ↦
          (Subtype.mk (p := fun (x : (j : C) → F.obj j) ↦ x ∈ F.sections)
              (fun (j : C) ↦
                (ConcreteCategory.hom (FC := TypeCat.Fun) (τ.app j) :
                    (a : (fun (X : Type u₂) ↦ X) (((const C).obj X).obj j)) → (fun (X : Type u₂) ↦ X) (F.obj j))
                  default)
              ⋯ :
            { x : (j : C) → F.obj j // x ∈ F.sections }))
        τ) =
    τ

Tactic:
ext _ (x : X)
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C_1 : Type u₁
inst : Category.{v₁, u₁} C_1
C : Type u₁
inst_1 : Category.{v₁, u₁} C
F : Functor.{v₁, u₂, u₁, u₂ + 1} C (Type u₂)
X : Type u₂
inst_2 : Unique X
τ : obj (const C) X ⟶ F
x_1 : C
x : X
w :
  TypeCat.Fun.toFun (X := obj.{v₁, u₂, u₁, u₂ + 1} (obj (const C) X) x_1)
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (NatTrans.app
          ((fun (s : (↑F.sections : Type (max u₁ u₂))) ↦
              ({
                  app := fun (j : C) ↦
                    ↾fun (x : obj.{v₁, u₂, u₁, u₂ + 1} (obj (const C) X) j) ↦ (↑s : (j : C) → F.obj j) j,
                  naturality := ⋯ } :
                NatTrans (obj (const C) X) F))
            ((fun (τ : obj (const C) X ⟶ F) ↦
                (Subtype.mk (p := fun (x : (j : C) → F.obj j) ↦ x ∈ F.sections)
                    (fun (j : C) ↦
                      (ConcreteCategory.hom (FC := TypeCat.Fun) (τ.app j) :
                          (a : (fun (X : Type u₂) ↦ X) (((const C).obj X).obj j)) → (fun (X : Type u₂) ↦ X) (F.obj j))
                        default)
                    ⋯ :
                  { x : (j : C) → F.obj j // x ∈ F.sections }))
              τ))
          x_1))
      default =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (τ.app x_1)).toFun default
⊢ TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (NatTrans.app
          ((fun (s : (↑F.sections : Type (max u₁ u₂))) ↦
              ({
                  app := fun (j : C) ↦
                    ↾fun (x : obj.{v₁, u₂, u₁, u₂ + 1} (obj (const C) X) j) ↦ (↑s : (j : C) → F.obj j) j,
                  naturality := ⋯ } :
                NatTrans (obj (const C) X) F))
            ((fun (τ : obj (const C) X ⟶ F) ↦
                (Subtype.mk (p := fun (x : (j : C) → F.obj j) ↦ x ∈ F.sections)
                    (fun (j : C) ↦
                      (ConcreteCategory.hom (FC := TypeCat.Fun) (τ.app j) :
                          (a : (fun (X : Type u₂) ↦ X) (((const C).obj X).obj j)) → (fun (X : Type u₂) ↦ X) (F.obj j))
                        default)
                    ⋯ :
                  { x : (j : C) → F.obj j // x ∈ F.sections }))
              τ))
          x_1))
      x =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (τ.app x_1)).toFun x

Tactic:
rw [Unique.eq_default x]

Premises used: Unique.eq_default
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C_1 : Type u₁
inst : Category.{v₁, u₁} C_1
C : Type u₁
inst_1 : Category.{v₁, u₁} C
F : Functor.{v₁, u₂, u₁, u₂ + 1} C (Type u₂)
X : Type u₂
inst_2 : Unique X
τ : obj (const C) X ⟶ F
x_1 : C
x : X
⊢ TypeCat.Fun.toFun (X := obj.{v₁, u₂, u₁, u₂ + 1} (obj (const C) X) x_1)
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (NatTrans.app
          ((fun (s : (↑F.sections : Type (max u₁ u₂))) ↦
              ({
                  app := fun (j : C) ↦
                    ↾fun (x : obj.{v₁, u₂, u₁, u₂ + 1} (obj (const C) X) j) ↦ (↑s : (j : C) → F.obj j) j,
                  naturality := ⋯ } :
                NatTrans (obj (const C) X) F))
            ((fun (τ : obj (const C) X ⟶ F) ↦
                (Subtype.mk (p := fun (x : (j : C) → F.obj j) ↦ x ∈ F.sections)
                    (fun (j : C) ↦
                      (ConcreteCategory.hom (FC := TypeCat.Fun) (τ.app j) :
                          (a : (fun (X : Type u₂) ↦ X) (((const C).obj X).obj j)) → (fun (X : Type u₂) ↦ X) (F.obj j))
                        default)
                    ⋯ :
                  { x : (j : C) → F.obj j // x ∈ F.sections }))
              τ))
          x_1))
      default =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (τ.app x_1)).toFun default

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
F G : Functor.{v₁, u₂, u₁, u₂ + 1} C (Type u₂)
f : F ⟶ G
X : Type u₂
inst_1 : Unique X
x : (↑F.sections : Type (max u₁ u₂))
⊢ Eq (α := obj (const C) X ⟶ G)
    ((G.sectionsEquivHom X : (a : (↑G.sections : Type (max u₁ u₂))) → (const C).obj X ⟶ G)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (map (sectionsFunctor C) f) :
            (a : (fun (X : Type (max u₁ u₂)) ↦ X) ((sectionsFunctor C).obj F)) →
              (fun (X : Type (max u₁ u₂)) ↦ X) ((sectionsFunctor C).obj G))
          x) :
      obj (const C) X ⟶ G)
    ((F.sectionsEquivHom X : (a : (↑F.sections : Type (max u₁ u₂))) → (const C).obj X ⟶ F) x ≫ f : obj (const C) X ⟶ G)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
F G : Functor.{v₁, u₂, u₁, u₂ + 1} C (Type u₂)
f : F ⟶ G
X : Type u₂
inst_1 : Unique X
τ : obj (const C) X ⟶ F
⊢ Eq (α := (↑G.sections : Type (max u₁ u₂)))
    (((G.sectionsEquivHom X).symm : (a : (const C).obj X ⟶ G) → (↑G.sections : Type (max u₁ u₂))) (τ ≫ f) :
      (↑G.sections : Type (max u₁ u₂)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (map (sectionsFunctor C) f) :
          (a : (fun (X : Type (max u₁ u₂)) ↦ X) ((sectionsFunctor C).obj F)) →
            (fun (X : Type (max u₁ u₂)) ↦ X) ((sectionsFunctor C).obj G))
        (((F.sectionsEquivHom X).symm : (a : (const C).obj X ⟶ F) → (↑F.sections : Type (max u₁ u₂))) τ) :
      (fun (X : Type (max u₁ u₂)) ↦ X) (obj (sectionsFunctor C) G))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C_1 : Type u₁
inst : Category.{v₁, u₁} C_1
C : Type u₁
inst_1 : Category.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
hF : F.FullyFaithful
X : C
X_1 Y : Cᵒᵖ
f : X_1 ⟶ Y
h :
  ∀ (x : (F.op ⋙ obj uliftYoneda.{v₁, v₂, u₂} (F.obj X)).obj X_1),
    Eq (α := obj (obj uliftYoneda.{v₂, v₁, u₁} X) Y)
      (TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          ((F.op ⋙ obj uliftYoneda.{v₁, v₂, u₂} (F.obj X)).map f ≫
            Iso.hom
              ((fun (Y : Cᵒᵖ) ↦
                  (Equiv.toIso
                      (Equiv.trans Equiv.ulift (Equiv.trans (Equiv.symm hF.homEquiv) (Equiv.symm Equiv.ulift))) :
                    (F.op ⋙ obj uliftYoneda.{v₁, v₂, u₂} (F.obj X)).obj Y ≅ obj (obj uliftYoneda.{v₂, v₁, u₁} X) Y))
                Y)))
        x)
      (TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (Iso.hom
              ((fun (Y : Cᵒᵖ) ↦
                  (Equiv.toIso
                      (Equiv.trans Equiv.ulift (Equiv.trans (Equiv.symm hF.homEquiv) (Equiv.symm Equiv.ulift))) :
                    (F.op ⋙ obj uliftYoneda.{v₁, v₂, u₂} (F.obj X)).obj Y ≅ obj (obj uliftYoneda.{v₂, v₁, u₁} X) Y))
                X_1) ≫
            map (obj uliftYoneda.{v₂, v₁, u₁} X) f))
        x)
⊢ Eq (α := (F.op ⋙ obj uliftYoneda.{v₁, v₂, u₂} (F.obj X)).obj X_1 ⟶ obj (obj uliftYoneda.{v₂, v₁, u₁} X) Y)
    ((F.op ⋙ obj uliftYoneda.{v₁, v₂, u₂} (F.obj X)).map f ≫
      Iso.hom
        ((fun (Y : Cᵒᵖ) ↦
            (Equiv.toIso (Equiv.trans Equiv.ulift (Equiv.trans (Equiv.symm hF.homEquiv) (Equiv.symm Equiv.ulift))) :
              (F.op ⋙ obj uliftYoneda.{v₁, v₂, u₂} (F.obj X)).obj Y ≅ obj (obj uliftYoneda.{v₂, v₁, u₁} X) Y))
          Y))
    (Iso.hom
        ((fun (Y : Cᵒᵖ) ↦
            (Equiv.toIso (Equiv.trans Equiv.ulift (Equiv.trans (Equiv.symm hF.homEquiv) (Equiv.symm Equiv.ulift))) :
              (F.op ⋙ obj uliftYoneda.{v₁, v₂, u₂} (F.obj X)).obj Y ≅ obj (obj uliftYoneda.{v₂, v₁, u₁} X) Y))
          X_1) ≫
      map (obj uliftYoneda.{v₂, v₁, u₁} X) f)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C_1 : Type u₁
inst : Category.{v₁, u₁} C_1
C : Type u₁
inst_1 : Category.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
hF : F.FullyFaithful
X : C
X_1 Y : Cᵒᵖ
f : X_1 ⟶ Y
x : (F.op ⋙ obj uliftYoneda.{v₁, v₂, u₂} (F.obj X)).obj X_1
⊢ Eq (α := F.obj (unop Y) ⟶ F.obj X)
    (F.map
      ((Equiv.ulift : (a : ULift.{v₂, v₁} ((yoneda.obj X).obj Y)) → (yoneda.obj X).obj Y)
        (TypeCat.Fun.toFun
          (ConcreteCategory.hom (FC := TypeCat.Fun)
            ((F.op ⋙ obj uliftYoneda.{v₁, v₂, u₂} (F.obj X)).map f ≫
              Iso.hom
                ((fun (Y : Cᵒᵖ) ↦
                    (Equiv.toIso
                        (Equiv.trans Equiv.ulift (Equiv.trans (Equiv.symm hF.homEquiv) (Equiv.symm Equiv.ulift))) :
                      (F.op ⋙ obj uliftYoneda.{v₁, v₂, u₂} (F.obj X)).obj Y ≅ obj (obj uliftYoneda.{v₂, v₁, u₁} X) Y))
                  Y)))
          x)))
    (F.map
      ((Equiv.ulift : (a : ULift.{v₂, v₁} ((yoneda.obj X).obj Y)) → (yoneda.obj X).obj Y)
        (TypeCat.Fun.toFun
          (ConcreteCategory.hom (FC := TypeCat.Fun)
            (Iso.hom
                ((fun (Y : Cᵒᵖ) ↦
                    (Equiv.toIso
                        (Equiv.trans Equiv.ulift (Equiv.trans (Equiv.symm hF.homEquiv) (Equiv.symm Equiv.ulift))) :
                      (F.op ⋙ obj uliftYoneda.{v₁, v₂, u₂} (F.obj X)).obj Y ≅ obj (obj uliftYoneda.{v₂, v₁, u₁} X) Y))
                  X_1) ≫
              map (obj uliftYoneda.{v₂, v₁, u₁} X) f))
          x)))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Yoneda
Goal:
C_1 : Type u₁
inst : Category.{v₁, u₁} C_1
C : Type u₁
inst_1 : Category.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
hF : F.FullyFaithful
X : C
X_1 Y : Cᵒᵖ
f : X_1 ⟶ Y
x : (F.op ⋙ obj uliftYoneda.{v₁, v₂, u₂} (F.obj X)).obj X_1
⊢ Eq (α := obj (obj uliftYoneda.{v₂, v₁, u₁} X) Y)
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        ((F.op ⋙ obj uliftYoneda.{v₁, v₂, u₂} (F.obj X)).map f ≫
          Iso.hom
            ((fun (Y : Cᵒᵖ) ↦
                (Equiv.toIso (Equiv.trans Equiv.ulift (Equiv.trans (Equiv.symm hF.homEquiv) (Equiv.symm Equiv.ulift))) :
                  (F.op ⋙ obj uliftYoneda.{v₁, v₂, u₂} (F.obj X)).obj Y ≅ obj (obj uliftYoneda.{v₂, v₁, u₁} X) Y))
              Y)))
      x)
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (Iso.hom
            ((fun (Y : Cᵒᵖ) ↦
                (Equiv.toIso (Equiv.trans Equiv.ulift (Equiv.trans (Equiv.symm hF.homEquiv) (Equiv.symm Equiv.ulift))) :
                  (F.op ⋙ obj uliftYoneda.{v₁, v₂, u₂} (F.obj X)).obj Y ≅ obj (obj uliftYoneda.{v₂, v₁, u₁} X) Y))
              X_1) ≫
          map (obj uliftYoneda.{v₂, v₁, u₁} X) f))
      x)

Tactic:
exact Equiv.ulift.injective (hF.map_injective (by simp))

Premises used: CategoryTheory.Functor.FullyFaithful.map_injective, Equiv.ulift, Equiv.injective