awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Presheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
ℰ : Type u₂
inst_1 : Category.{v₂, u₂} ℰ
A_1 A : Functor.{v₁, v₂, u₁, u₂} C ℰ
inst_2 : Functor.HasPointwiseLeftKanExtension uliftYoneda.{max w v₂, v₁, u₁} A
D : Type u₂
inst_3 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X : C
Y : F.op.LeftExtension (Functor.obj uliftYoneda.{max w v₂, v₁, u₁} X)
Z : Cᵒᵖ
f : Functor.obj (Functor.obj yoneda X) Z
⊢ TypeCat.Fun.toFun
      (hom (FC := TypeCat.Fun)
        (NatTrans.app
          (StructuredArrow.hom
              (Functor.LeftExtension.mk (Functor.obj uliftYoneda.{max w v₁, v₂, u₂} (F.obj X))
                (uliftYonedaMap.{w, v₁, v₂, u₁, u₂} F X)) ≫
            Functor.map (Functor.obj (Functor.whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max (max w v₂) v₁))) F.op)
              ((Equiv.symm uliftYonedaEquiv :
                  (a : (StructuredArrow.right Y).obj (op (F.obj X))) →
                    uliftYoneda.{max v₁ w, v₂, u₂}.obj (F.obj X) ⟶ StructuredArrow.right Y)
                ((uliftYonedaEquiv :
                    (a : uliftYoneda.{max v₂ w, v₁, u₁}.obj X ⟶ F.op ⋙ StructuredArrow.right Y) →
                      (F.op ⋙ StructuredArrow.right Y).obj (op X))
                  (StructuredArrow.hom Y))))
          Z))
      { down := f : ULift.{max w v₂, v₁} (Functor.obj (Functor.obj yoneda X) Z) } =
    (hom (FC := TypeCat.Fun) ((StructuredArrow.hom Y).app Z)).toFun
      { down := f : ULift.{max w v₂, v₁} (Functor.obj (Functor.obj yoneda X) Z) }

Tactic:
simpa [uliftYonedaEquiv, uliftYoneda] using
        ConcreteCategory.congr_hom (CC := fun X ↦ X) (Y.hom.naturality f.op).symm (ULift.up (𝟙 _))

Premises used: Quiver.Hom.op, CategoryTheory.CategoryStruct.id, CategoryTheory.StructuredArrow.hom, CategoryTheory.NatTrans.naturality, CategoryTheory.ConcreteCategory.congr_hom, ULift.up, Eq.symm, CategoryTheory.uliftYoneda, CategoryTheory.uliftYonedaEquiv
-- Module: Mathlib.CategoryTheory.Limits.Presheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
ℰ : Type u₂
inst_1 : Category.{v₂, u₂} ℰ
A_1 A : Functor.{v₁, v₂, u₁, u₂} C ℰ
inst_2 : Functor.HasPointwiseLeftKanExtension uliftYoneda.{max w v₂, v₁, u₁} A
D : Type u₂
inst_3 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X : C
Y : F.op.LeftExtension (Functor.obj uliftYoneda.{max w v₂, v₁, u₁} X)
φ :
  Functor.LeftExtension.mk (Functor.obj uliftYoneda.{max w v₁, v₂, u₂} (F.obj X))
      (uliftYonedaMap.{w, v₁, v₂, u₁, u₂} F X) ⟶
    Y
h :
  StructuredArrow.Hom.right φ =
    StructuredArrow.Hom.right
      (StructuredArrow.homMk
        ((Equiv.symm uliftYonedaEquiv :
            (a : (StructuredArrow.right Y).obj (op (F.obj X))) →
              uliftYoneda.{max v₁ w, v₂, u₂}.obj (F.obj X) ⟶ StructuredArrow.right Y)
          ((uliftYonedaEquiv :
              (a : uliftYoneda.{max v₂ w, v₁, u₁}.obj X ⟶ F.op ⋙ StructuredArrow.right Y) →
                (F.op ⋙ StructuredArrow.right Y).obj (op X))
            (StructuredArrow.hom Y)))
        ⋯)
⊢ φ =
    StructuredArrow.homMk
      ((Equiv.symm uliftYonedaEquiv :
          (a : (StructuredArrow.right Y).obj (op (F.obj X))) →
            uliftYoneda.{max v₁ w, v₂, u₂}.obj (F.obj X) ⟶ StructuredArrow.right Y)
        ((uliftYonedaEquiv :
            (a : uliftYoneda.{max v₂ w, v₁, u₁}.obj X ⟶ F.op ⋙ StructuredArrow.right Y) →
              (F.op ⋙ StructuredArrow.right Y).obj (op X))
          (StructuredArrow.hom Y)))
      ⋯

Tactic:
ext : 1
-- Module: Mathlib.CategoryTheory.Limits.Presheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
ℰ : Type u₂
inst_1 : Category.{v₂, u₂} ℰ
A_1 A : Functor.{v₁, v₂, u₁, u₂} C ℰ
inst_2 : Functor.HasPointwiseLeftKanExtension uliftYoneda.{max w v₂, v₁, u₁} A
D : Type u₂
inst_3 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X : C
Y : F.op.LeftExtension (Functor.obj uliftYoneda.{max w v₂, v₁, u₁} X)
φ :
  Functor.LeftExtension.mk (Functor.obj uliftYoneda.{max w v₁, v₂, u₂} (F.obj X))
      (uliftYonedaMap.{w, v₁, v₂, u₁, u₂} F X) ⟶
    Y
h :
  Eq (α := (StructuredArrow.right Y).obj (op (F.obj X)))
    ((uliftYonedaEquiv :
          (a : uliftYoneda.{max v₁ w, v₂, u₂}.obj (F.obj X) ⟶ StructuredArrow.right Y) →
            (StructuredArrow.right Y).obj (op (F.obj X)))
        (StructuredArrow.Hom.right φ) :
      (StructuredArrow.right Y).obj (op (F.obj X)))
    ((uliftYonedaEquiv :
          (a : uliftYoneda.{max v₁ w, v₂, u₂}.obj (F.obj X) ⟶ StructuredArrow.right Y) →
            (StructuredArrow.right Y).obj (op (F.obj X)))
        (StructuredArrow.Hom.right
          (StructuredArrow.homMk
            ((Equiv.symm uliftYonedaEquiv :
                (a : (StructuredArrow.right Y).obj (op (F.obj X))) →
                  uliftYoneda.{max v₁ w, v₂, u₂}.obj (F.obj X) ⟶ StructuredArrow.right Y)
              ((uliftYonedaEquiv :
                  (a : uliftYoneda.{max v₂ w, v₁, u₁}.obj X ⟶ F.op ⋙ StructuredArrow.right Y) →
                    (F.op ⋙ StructuredArrow.right Y).obj (op X))
                (StructuredArrow.hom Y)))
            ⋯)) :
      (StructuredArrow.right Y).obj (op (F.obj X)))
⊢ StructuredArrow.Hom.right φ =
    StructuredArrow.Hom.right
      (StructuredArrow.homMk
        ((Equiv.symm uliftYonedaEquiv :
            (a : (StructuredArrow.right Y).obj (op (F.obj X))) →
              uliftYoneda.{max v₁ w, v₂, u₂}.obj (F.obj X) ⟶ StructuredArrow.right Y)
          ((uliftYonedaEquiv :
              (a : uliftYoneda.{max v₂ w, v₁, u₁}.obj X ⟶ F.op ⋙ StructuredArrow.right Y) →
                (F.op ⋙ StructuredArrow.right Y).obj (op X))
            (StructuredArrow.hom Y)))
        ⋯)

Tactic:
apply uliftYonedaEquiv.injective

Premises used: Equiv.injective, CategoryTheory.uliftYonedaEquiv
-- Module: Mathlib.CategoryTheory.Limits.Presheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
ℰ : Type u₂
inst_1 : Category.{v₂, u₂} ℰ
A_1 A : Functor.{v₁, v₂, u₁, u₂} C ℰ
inst_2 : Functor.HasPointwiseLeftKanExtension uliftYoneda.{max w v₂, v₁, u₁} A
D : Type u₂
inst_3 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X : C
Y : F.op.LeftExtension (Functor.obj uliftYoneda.{max w v₂, v₁, u₁} X)
φ :
  Functor.LeftExtension.mk (Functor.obj uliftYoneda.{max w v₁, v₂, u₂} (F.obj X))
      (uliftYonedaMap.{w, v₁, v₂, u₁, u₂} F X) ⟶
    Y
⊢ Eq (α := (StructuredArrow.right Y).obj (op (F.obj X)))
    ((uliftYonedaEquiv :
          (a : uliftYoneda.{max v₁ w, v₂, u₂}.obj (F.obj X) ⟶ StructuredArrow.right Y) →
            (StructuredArrow.right Y).obj (op (F.obj X)))
        (StructuredArrow.Hom.right φ) :
      (StructuredArrow.right Y).obj (op (F.obj X)))
    ((uliftYonedaEquiv :
          (a : uliftYoneda.{max v₁ w, v₂, u₂}.obj (F.obj X) ⟶ StructuredArrow.right Y) →
            (StructuredArrow.right Y).obj (op (F.obj X)))
        (StructuredArrow.Hom.right
          (StructuredArrow.homMk
            ((Equiv.symm uliftYonedaEquiv :
                (a : (StructuredArrow.right Y).obj (op (F.obj X))) →
                  uliftYoneda.{max v₁ w, v₂, u₂}.obj (F.obj X) ⟶ StructuredArrow.right Y)
              ((uliftYonedaEquiv :
                  (a : uliftYoneda.{max v₂ w, v₁, u₁}.obj X ⟶ F.op ⋙ StructuredArrow.right Y) →
                    (F.op ⋙ StructuredArrow.right Y).obj (op X))
                (StructuredArrow.hom Y)))
            ⋯)) :
      (StructuredArrow.right Y).obj (op (F.obj X)))

Tactic:
simp [← StructuredArrow.w φ, uliftYonedaEquiv, uliftYonedaMap]

Premises used: CategoryTheory.StructuredArrow.w, CategoryTheory.uliftYonedaMap, CategoryTheory.uliftYonedaEquiv
-- Module: Mathlib.CategoryTheory.Limits.Presheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
ℰ : Type u₂
inst_1 : Category.{v₂, u₂} ℰ
A_1 A : Functor.{v₁, v₂, u₁, u₂} C ℰ
inst_2 : Functor.HasPointwiseLeftKanExtension uliftYoneda.{max w v₂, v₁, u₁} A
D : Type u₂
inst_3 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X : C
⊢ Functor.IsLeftKanExtension (Functor.obj uliftYoneda.{max w v₁, v₂, u₂} (F.obj X))
    (uliftYonedaMap.{w, v₁, v₂, u₁, u₂} F X)

Tactic:
⟨⟨Limits.IsInitial.ofUnique _⟩⟩

Premises used: Nonempty.intro, CategoryTheory.Limits.IsInitial.ofUnique, CategoryTheory.Functor.IsLeftKanExtension.mk
-- Module: Mathlib.CategoryTheory.Limits.Presheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
ℰ : Type u₂
inst_1 : Category.{v₂, u₂} ℰ
A_1 A : Functor.{v₁, v₂, u₁, u₂} C ℰ
inst_2 : Functor.HasPointwiseLeftKanExtension uliftYoneda.{max w v₂, v₁, u₁} A
D : Type u₂
inst_3 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : ∀ (P : Cᵒᵖ ⥤ Type (max w v₁ v₂)), F.op.HasLeftKanExtension P
X Y : C
f : X ⟶ Y
⊢ Eq (α := (Functor.obj F.op.lan (Functor.obj uliftYoneda.{max v₂ w, v₁, u₁} Y)).obj (F.op.obj (op X)))
    ((hom (FC := TypeCat.Fun)
            ((uliftYonedaMap.{w, v₁, v₂, u₁, u₂} F Y).app (op X) ≫
              NatTrans.app
                (Functor.descOfIsLeftKanExtension (Functor.obj uliftYoneda.{max w v₁, v₂, u₂} (F.obj Y))
                  (uliftYonedaMap.{w, v₁, v₂, u₁, u₂} F Y)
                  (Functor.obj F.op.lan (Functor.obj uliftYoneda.{max v₂ w, v₁, u₁} Y))
                  (NatTrans.app F.op.lanUnit (Functor.obj uliftYoneda.{max v₂ w, v₁, u₁} Y)))
                (F.op.obj (op X))) :
          (a : (uliftYoneda.{max w v₂, v₁, u₁}.obj Y).obj (op X)) →
            (F.op.lan.obj (uliftYoneda.{max v₂ w, v₁, u₁}.obj Y)).obj (F.op.obj (op X)))
        { down := f } :
      (Functor.obj F.op.lan (Functor.obj uliftYoneda.{max v₂ w, v₁, u₁} Y)).obj (F.op.obj (op X)))
    ((hom (FC := TypeCat.Fun)
            (NatTrans.app (NatTrans.app F.op.lanUnit (Functor.obj uliftYoneda.{max v₂ w, v₁, u₁} Y)) (op X)) :
          (a : (uliftYoneda.{max w v₂, v₁, u₁}.obj Y).obj (op X)) →
            (F.op.lan.obj (uliftYoneda.{max v₂ w, v₁, u₁}.obj Y)).obj (F.op.obj (op X)))
        { down := f } :
      (Functor.obj F.op.lan (Functor.obj uliftYoneda.{max v₂ w, v₁, u₁} Y)).obj (F.op.obj (op X)))

Tactic:
have eq₁ := ConcreteCategory.congr_hom
        ((uliftYoneda.{max w v₁}.obj (F.obj Y)).descOfIsLeftKanExtension_fac_app
        (uliftYonedaMap F Y) (F.op.lan.obj (uliftYoneda.obj Y))
          (F.op.lanUnit.app (uliftYoneda.obj Y)) _) ⟨f⟩
-- Module: Mathlib.CategoryTheory.Limits.Presheaf
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
inst_2 : ∀ (P : Cᵒᵖ ⥤ Type (max w v₁ v₂)), F.op.HasLeftKanExtension P
X : C
⊢ Eq (α := Functor.obj (Functor.obj uliftYoneda.{max w v₁, v₂, u₂} (F.obj X)) (F.op.obj (op X)))
    ((hom (FC := TypeCat.Fun) ((uliftYonedaMap.{w, v₁, v₂, u₁, u₂} F X).app (op X)) :
          (a : ((𝟭 (Cᵒᵖ ⥤ Type (max (max w v₂) v₁))).obj (uliftYoneda.{max w v₂, v₁, u₁}.obj X)).obj (op X)) →
            (uliftYoneda.{max w v₁, v₂, u₂}.obj (F.obj X)).obj (F.op.obj (op X)))
        { down := 𝟙 X } :
      Functor.obj (Functor.obj uliftYoneda.{max w v₁, v₂, u₂} (F.obj X)) (F.op.obj (op X)))
    ({ down := 𝟙 (F.obj X) } : ULift.{max v₁ w, v₂} (F.obj X ⟶ F.obj X))

Tactic:
simp [uliftYonedaMap]

Premises used: CategoryTheory.uliftYonedaMap
-- Module: Mathlib.CategoryTheory.Limits.Presheaf
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
G : (Cᵒᵖ ⥤ Type (max w v₁ v₂)) ⥤ Dᵒᵖ ⥤ Type (max w v₁ v₂)
φ : F ⋙ uliftYoneda.{max w v₁, v₂, u₂} ⟶ uliftYoneda.{max w v₂, v₁, u₁} ⋙ G
P : Cᵒᵖ ⥤ Type (max w v₁ v₂)
x y : P.Elements
f : x ⟶ y
⊢ Eq (α := P.obj (op (unop (y.fst (β := fun (c : Cᵒᵖ) ↦ P.obj c)))))
    ((uliftYonedaEquiv : (a : uliftYoneda.{max v₂ w, v₁, u₁}.obj (unop y.fst) ⟶ P) → P.obj (op (unop y.fst)))
        (Functor.map uliftYoneda.{max v₂ w, v₁, u₁} (↑f : x.fst ⟶ y.fst).unop ≫
          (Equiv.symm uliftYonedaEquiv :
              (a : P.obj (op (unop x.fst))) → uliftYoneda.{max v₂ w, v₁, u₁}.obj (unop x.fst) ⟶ P)
            (x.snd (β := fun (c : Cᵒᵖ) ↦ P.obj c))) :
      P.obj (op (unop (y.fst (β := fun (c : Cᵒᵖ) ↦ P.obj c)))))
    ((uliftYonedaEquiv : (a : uliftYoneda.{max v₂ w, v₁, u₁}.obj (unop y.fst) ⟶ P) → P.obj (op (unop y.fst)))
        ((Equiv.symm uliftYonedaEquiv : (a : P.obj (op (unop y.1))) → uliftYoneda.{max w v₂, v₁, u₁}.obj (unop y.1) ⟶ P)
          (y.snd (β := fun (c : Cᵒᵖ) ↦ P.obj c))) :
      P.obj (op (unop (y.fst (β := fun (c : Cᵒᵖ) ↦ P.obj c)))))

Tactic:
simpa only [Equiv.apply_symm_apply, ← uliftYonedaEquiv_naturality] using f.2

Premises used: Equiv.apply_symm_apply, CategoryTheory.uliftYonedaEquiv_naturality, Subtype.property
-- Module: Mathlib.CategoryTheory.Limits.Presheaf
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
G : (Cᵒᵖ ⥤ Type (max w v₁ v₂)) ⥤ Dᵒᵖ ⥤ Type (max w v₁ v₂)
φ : F ⋙ uliftYoneda.{max w v₁, v₂, u₂} ⟶ uliftYoneda.{max w v₂, v₁, u₁} ⋙ G
P : Cᵒᵖ ⥤ Type (max w v₁ v₂)
x y : P.Elements
f : x ⟶ y
⊢ Eq (α := Functor.obj uliftYoneda.{max v₂ w, v₁, u₁} (unop (y.fst (β := fun (c : Cᵒᵖ) ↦ P.obj c))) ⟶ P)
    (Functor.map uliftYoneda.{max v₂ w, v₁, u₁} (↑f : x.fst ⟶ y.fst).unop ≫
      (Equiv.symm uliftYonedaEquiv :
          (a : P.obj (op (unop x.fst))) → uliftYoneda.{max v₂ w, v₁, u₁}.obj (unop x.fst) ⟶ P)
        (x.snd (β := fun (c : Cᵒᵖ) ↦ P.obj c)))
    ((Equiv.symm uliftYonedaEquiv : (a : P.obj (op (unop y.1))) → uliftYoneda.{max w v₂, v₁, u₁}.obj (unop y.1) ⟶ P)
      (y.snd (β := fun (c : Cᵒᵖ) ↦ P.obj c)))

Tactic:
have eq₁ : uliftYoneda.map f.1.unop ≫ uliftYonedaEquiv.symm x.2 =
      uliftYonedaEquiv.{max w v₂}.symm y.2 :=
    uliftYonedaEquiv.injective
      (by simpa only [Equiv.apply_symm_apply, ← uliftYonedaEquiv_naturality] using f.2)
-- Module: Mathlib.CategoryTheory.Limits.Presheaf
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
G : (Cᵒᵖ ⥤ Type (max w v₁ v₂)) ⥤ Dᵒᵖ ⥤ Type (max w v₁ v₂)
φ : F ⋙ uliftYoneda.{max w v₁, v₂, u₂} ⟶ uliftYoneda.{max w v₂, v₁, u₁} ⋙ G
P : Cᵒᵖ ⥤ Type (max w v₁ v₂)
X : C
f : Functor.obj uliftYoneda.{max w v₂, v₁, u₁} X ⟶ P
obtain :
  ∀ (x : P.obj (op X)),
    Eq (α := (F.op ⋙ G.obj P).obj (op X))
      ((uliftYonedaEquiv : (a : uliftYoneda.{max v₂ w, v₁, u₁}.obj X ⟶ F.op ⋙ G.obj P) → (F.op ⋙ G.obj P).obj (op X))
          ((Equiv.symm uliftYonedaEquiv : (a : P.obj (op X)) → uliftYoneda.{max v₂ w, v₁, u₁}.obj X ⟶ P) x ≫
            presheafHom.{w, v₁, v₂, u₁, u₂} φ P) :
        (F.op ⋙ G.obj P).obj (op X))
      ((hom (FC := TypeCat.Fun)
              (NatTrans.app
                (G.map
                  ((Equiv.symm uliftYonedaEquiv : (a : P.obj (op X)) → uliftYoneda.{max v₂ w, v₁, u₁}.obj X ⟶ P) x))
                (op (F.obj X))) :
            (a :
                (fun (X : Type (max (max v₁ v₂) w)) ↦ X)
                  ((G.obj (uliftYoneda.{max w v₂, v₁, u₁}.obj X)).obj (op (F.obj X)))) →
              (fun (X : Type (max (max v₁ v₂) w)) ↦ X) ((G.obj P).obj (op (F.obj X))))
          ((hom (FC := TypeCat.Fun) ((φ.app X).app (op (F.obj X))) :
              (a :
                  (fun (X : Type (max (max v₁ v₂) w)) ↦ X)
                    (((F ⋙ uliftYoneda.{max w v₁, v₂, u₂}).obj X).obj (op (F.obj X)))) →
                (fun (X : Type (max (max v₁ v₂) w)) ↦ X)
                  (((uliftYoneda.{max w v₂, v₁, u₁} ⋙ G).obj X).obj (op (F.obj X))))
            { down := 𝟙 (unop (op (F.obj X))) }) :
        (fun (X : Type (max (max v₁ v₂) w)) ↦ X) ((G.obj P).obj (op (F.obj X))))
⊢ Eq (α := (F.op ⋙ G.obj P).obj (op X))
    ((uliftYonedaEquiv : (a : uliftYoneda.{max v₂ w, v₁, u₁}.obj X ⟶ F.op ⋙ G.obj P) → (F.op ⋙ G.obj P).obj (op X))
        (f ≫ presheafHom.{w, v₁, v₂, u₁, u₂} φ P) :
      (F.op ⋙ G.obj P).obj (op X))
    ((hom (FC := TypeCat.Fun) ((G.map f).app (op (F.obj X))) :
          (a :
              (fun (X : Type (max (max v₁ v₂) w)) ↦ X)
                ((G.obj (uliftYoneda.{max w v₂, v₁, u₁}.obj X)).obj (op (F.obj X)))) →
            (fun (X : Type (max (max v₁ v₂) w)) ↦ X) ((G.obj P).obj (op (F.obj X))))
        ((hom (FC := TypeCat.Fun) ((φ.app X).app (op (F.obj X))) :
            (a :
                (fun (X : Type (max (max v₁ v₂) w)) ↦ X)
                  (((F ⋙ uliftYoneda.{max w v₁, v₂, u₂}).obj X).obj (op (F.obj X)))) →
              (fun (X : Type (max (max v₁ v₂) w)) ↦ X)
                (((uliftYoneda.{max w v₂, v₁, u₁} ⋙ G).obj X).obj (op (F.obj X))))
          { down := 𝟙 (unop (op (F.obj X))) }) :
      (fun (X : Type (max (max v₁ v₂) w)) ↦ X) ((G.obj P).obj (op (F.obj X))))

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

Premises used: Equiv.surjective, Equiv.symm, rfl, CategoryTheory.uliftYonedaEquiv
-- Module: Mathlib.CategoryTheory.Limits.Presheaf
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
G : (Cᵒᵖ ⥤ Type (max w v₁ v₂)) ⥤ Dᵒᵖ ⥤ Type (max w v₁ v₂)
φ : F ⋙ uliftYoneda.{max w v₁, v₂, u₂} ⟶ uliftYoneda.{max w v₂, v₁, u₁} ⋙ G
P : Cᵒᵖ ⥤ Type (max w v₁ v₂)
X : C
x : P.obj (op X)
⊢ Eq (α := (F.op ⋙ G.obj P).obj (op X))
    ((uliftYonedaEquiv : (a : uliftYoneda.{max v₂ w, v₁, u₁}.obj X ⟶ F.op ⋙ G.obj P) → (F.op ⋙ G.obj P).obj (op X))
        ((Equiv.symm uliftYonedaEquiv :
            (a : (F.op ⋙ G.obj P).obj (op X)) → uliftYoneda.{max v₂ w, v₁, u₁}.obj X ⟶ F.op ⋙ G.obj P)
          ((hom (FC := TypeCat.Fun)
                (NatTrans.app
                  (G.map
                    ((Equiv.symm uliftYonedaEquiv : (a : P.obj (op X)) → uliftYoneda.{max w v₂, v₁, u₁}.obj X ⟶ P) x))
                  (F.op.obj (op X))) :
              (a : (G.obj (uliftYoneda.{max w v₂, v₁, u₁}.obj X)).obj (F.op.obj (op X))) →
                (G.obj P).obj (F.op.obj (op X)))
            ((hom (FC := TypeCat.Fun) ((φ.app X).app (F.op.obj (op X))) :
                (a : ((F ⋙ uliftYoneda.{max w v₁, v₂, u₂}).obj X).obj (F.op.obj (op X))) →
                  ((uliftYoneda.{max w v₂, v₁, u₁} ⋙ G).obj X).obj (F.op.obj (op X)))
              { down := 𝟙 (unop (F.op.obj (op X))) }))) :
      (F.op ⋙ G.obj P).obj (op X))
    ((hom (FC := TypeCat.Fun)
            (NatTrans.app
              (G.map ((Equiv.symm uliftYonedaEquiv : (a : P.obj (op X)) → uliftYoneda.{max v₂ w, v₁, u₁}.obj X ⟶ P) x))
              (op (F.obj X))) :
          (a : (G.obj (uliftYoneda.{max w v₂, v₁, u₁}.obj X)).obj (op (F.obj X))) → (G.obj P).obj (op (F.obj X)))
        ((hom (FC := TypeCat.Fun) ((φ.app X).app (op (F.obj X))) :
            (a : ((F ⋙ uliftYoneda.{max w v₁, v₂, u₂}).obj X).obj (op (F.obj X))) →
              ((uliftYoneda.{max w v₂, v₁, u₁} ⋙ G).obj X).obj (op (F.obj X)))
          { down := 𝟙 (F.obj X) }) :
      (G.obj P).obj (op (F.obj X)))

Tactic:
apply Equiv.apply_symm_apply

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.CategoryTheory.Limits.Presheaf
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
G : (Cᵒᵖ ⥤ Type (max w v₁ v₂)) ⥤ Dᵒᵖ ⥤ Type (max w v₁ v₂)
φ : F ⋙ uliftYoneda.{max w v₁, v₂, u₂} ⟶ uliftYoneda.{max w v₂, v₁, u₁} ⋙ G
X : C
⊢ Eq (α := (F.op ⋙ G.obj (Functor.obj uliftYoneda.{max w v₂, v₁, u₁} X)).obj (op X))
    ((uliftYonedaEquiv :
          (a : uliftYoneda.{max w v₂, v₁, u₁}.obj X ⟶ F.op ⋙ G.obj (uliftYoneda.{max w v₂, v₁, u₁}.obj X)) →
            (F.op ⋙ G.obj (uliftYoneda.{max w v₂, v₁, u₁}.obj X)).obj (op X))
        (presheafHom.{w, v₁, v₂, u₁, u₂} φ (Functor.obj uliftYoneda.{max w v₂, v₁, u₁} X)) :
      (F.op ⋙ G.obj (Functor.obj uliftYoneda.{max w v₂, v₁, u₁} X)).obj (op X))
    ((hom (FC := TypeCat.Fun) ((φ.app X).app (F.op.obj (op X))) :
          (a :
              (fun (X : Type (max (max v₁ v₂) w)) ↦ X)
                (((F ⋙ uliftYoneda.{max w v₁, v₂, u₂}).obj X).obj (F.op.obj (op X)))) →
            (fun (X : Type (max (max v₁ v₂) w)) ↦ X)
              (((uliftYoneda.{max w v₂, v₁, u₁} ⋙ G).obj X).obj (F.op.obj (op X))))
        { down := 𝟙 (unop (F.op.obj (op X))) } :
      (fun (X : Type (max (max v₁ v₂) w)) ↦ X) (((uliftYoneda.{max w v₂, v₁, u₁} ⋙ G).obj X).obj (F.op.obj (op X))))

Tactic:
simpa using uliftYonedaEquiv_ι_presheafHom.{w} φ (uliftYoneda.obj X) (𝟙 _)
-- Module: Mathlib.CategoryTheory.Limits.Presheaf
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
G : (Cᵒᵖ ⥤ Type (max w v₁ v₂)) ⥤ Dᵒᵖ ⥤ Type (max w v₁ v₂)
φ : F ⋙ uliftYoneda.{max w v₁, v₂, u₂} ⟶ uliftYoneda.{max w v₂, v₁, u₁} ⋙ G
P Q : Cᵒᵖ ⥤ Type (max w v₁ v₂)
f : P ⟶ Q
X : C
p : Functor.obj uliftYoneda.{max w v₂, v₁, u₁} X ⟶ P
rw :
  Eq (α := (F.op ⋙ G.obj Q).obj (op X))
    ((hom (FC := TypeCat.Fun) ((F.op.whiskerLeft (G.map f)).app (op X)) :
          (a : (fun (X : Type (max v₁ v₂ w)) ↦ X) ((F.op ⋙ G.obj P).obj (op X))) →
            (fun (X : Type (max v₁ v₂ w)) ↦ X) ((F.op ⋙ G.obj Q).obj (op X)))
        ((hom (FC := TypeCat.Fun) ((G.map p).app (op (F.obj X))) :
            (a :
                (fun (X : Type (max (max v₁ v₂) w)) ↦ X)
                  ((G.obj (uliftYoneda.{max w v₂, v₁, u₁}.obj X)).obj (op (F.obj X)))) →
              (fun (X : Type (max (max v₁ v₂) w)) ↦ X) ((G.obj P).obj (op (F.obj X))))
          ((hom (FC := TypeCat.Fun) ((φ.app X).app (op (F.obj X))) :
              (a :
                  (fun (X : Type (max (max v₁ v₂) w)) ↦ X)
                    (((F ⋙ uliftYoneda.{max w v₁, v₂, u₂}).obj X).obj (op (F.obj X)))) →
                (fun (X : Type (max (max v₁ v₂) w)) ↦ X)
                  (((uliftYoneda.{max w v₂, v₁, u₁} ⋙ G).obj X).obj (op (F.obj X))))
            { down := 𝟙 (unop (op (F.obj X))) })) :
      (fun (X : Type (max v₁ v₂ w)) ↦ X) ((F.op ⋙ G.obj Q).obj (op X)))
    ((hom (FC := TypeCat.Fun) ((G.map p ≫ G.map f).app (op (F.obj X))) :
          (a :
              (fun (X : Type (max (max v₁ v₂) w)) ↦ X)
                ((G.obj (uliftYoneda.{max w v₂, v₁, u₁}.obj X)).obj (op (F.obj X)))) →
            (fun (X : Type (max (max v₁ v₂) w)) ↦ X) ((G.obj Q).obj (op (F.obj X))))
        ((hom (FC := TypeCat.Fun) ((φ.app X).app (op (F.obj X))) :
            (a :
                (fun (X : Type (max (max v₁ v₂) w)) ↦ X)
                  (((F ⋙ uliftYoneda.{max w v₁, v₂, u₂}).obj X).obj (op (F.obj X)))) →
              (fun (X : Type (max (max v₁ v₂) w)) ↦ X)
                (((uliftYoneda.{max w v₂, v₁, u₁} ⋙ G).obj X).obj (op (F.obj X))))
          { down := 𝟙 (unop (op (F.obj X))) }) :
      (fun (X : Type (max (max v₁ v₂) w)) ↦ X) ((G.obj Q).obj (op (F.obj X))))
⊢ Eq (α := (F.op ⋙ G.obj Q).obj (op X))
    ((uliftYonedaEquiv : (a : uliftYoneda.{max v₂ w, v₁, u₁}.obj X ⟶ F.op ⋙ G.obj Q) → (F.op ⋙ G.obj Q).obj (op X))
        (p ≫ presheafHom.{w, v₁, v₂, u₁, u₂} φ P ≫ F.op.whiskerLeft (G.map f)) :
      (F.op ⋙ G.obj Q).obj (op X))
    ((uliftYonedaEquiv : (a : uliftYoneda.{max v₂ w, v₁, u₁}.obj X ⟶ F.op ⋙ G.obj Q) → (F.op ⋙ G.obj Q).obj (op X))
        (p ≫ f ≫ presheafHom.{w, v₁, v₂, u₁, u₂} φ Q) :
      (F.op ⋙ G.obj Q).obj (op X))

Tactic:
rw [← assoc p f, uliftYonedaEquiv_ι_presheafHom, ← assoc,
      uliftYonedaEquiv_comp, uliftYonedaEquiv_ι_presheafHom,
      Functor.map_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Presheaf.compULiftYonedaIsoULiftYonedaCompLan.uliftYonedaEquiv_ι_presheafHom, CategoryTheory.uliftYonedaEquiv_comp, CategoryTheory.Functor.map_comp