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 : Functor.{v₁, v₂, u₁, u₂} C ℰ
inst_2 : Functor.HasPointwiseLeftKanExtension uliftYoneda.{max w v₂, v₁, u₁} A
L : (Cᵒᵖ ⥤ Type (max w v₁ v₂)) ⥤ ℰ
α : A ⟶ uliftYoneda.{max w v₂, v₁, u₁} ⋙ L
left : IsIso α
right :
  PreservesColimitsOfSize.{v₁, max w u₁ v₁ v₂, max (max (max u₁ v₁) v₂) w, v₂,
      max (max (max u₁ (v₁ + 1)) (v₂ + 1)) (w + 1), u₂}
    L
mpr : (Functor.LeftExtension.mk L α).IsPointwiseLeftKanExtension
⊢ L.IsLeftKanExtension α

Tactic:
apply Functor.LeftExtension.IsPointwiseLeftKanExtension.isLeftKanExtension
      (E := Functor.LeftExtension.mk _ α)

Premises used: CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtension.isLeftKanExtension
-- Module: Mathlib.CategoryTheory.Limits.Presheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
ℰ : Type u₂
inst_1 : Category.{v₂, u₂} ℰ
A : Functor.{v₁, v₂, u₁, u₂} C ℰ
inst_2 : Functor.HasPointwiseLeftKanExtension uliftYoneda.{max w v₂, v₁, u₁} A
L : (Cᵒᵖ ⥤ Type (max w v₁ v₂)) ⥤ ℰ
α : A ⟶ uliftYoneda.{max w v₂, v₁, u₁} ⋙ L
left : IsIso α
right :
  PreservesColimitsOfSize.{v₁, max w u₁ v₁ v₂, max (max (max u₁ v₁) v₂) w, v₂,
      max (max (max u₁ (v₁ + 1)) (v₂ + 1)) (w + 1), u₂}
    L
P : Cᵒᵖ ⥤ Type (max (max w v₂) v₁)
mpr :
  IsColimit
    (Cocone.whisker (CategoryOfElements.costructuredArrowULiftYonedaEquivalence P).functor
      ((Functor.LeftExtension.mk L α).coconeAt P))
⊢ IsColimit ((Functor.LeftExtension.mk L α).coconeAt P)

Tactic:
apply IsColimit.ofWhiskerEquivalence
      (CategoryOfElements.costructuredArrowULiftYonedaEquivalence _)

Premises used: CategoryTheory.CategoryOfElements.costructuredArrowULiftYonedaEquivalence, CategoryTheory.Limits.IsColimit.ofWhiskerEquivalence
-- Module: Mathlib.CategoryTheory.Limits.Presheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
ℰ : Type u₂
inst_1 : Category.{v₂, u₂} ℰ
A : Functor.{v₁, v₂, u₁, u₂} C ℰ
inst_2 : Functor.HasPointwiseLeftKanExtension uliftYoneda.{max w v₂, v₁, u₁} A
L : (Cᵒᵖ ⥤ Type (max w v₁ v₂)) ⥤ ℰ
α : A ⟶ uliftYoneda.{max w v₂, v₁, u₁} ⋙ L
left : IsIso α
right :
  PreservesColimitsOfSize.{v₁, max w u₁ v₁ v₂, max (max (max u₁ v₁) v₂) w, v₂,
      max (max (max u₁ (v₁ + 1)) (v₂ + 1)) (w + 1), u₂}
    L
P : Cᵒᵖ ⥤ Type (max (max w v₂) v₁)
e : (CategoryOfElements.costructuredArrowULiftYonedaEquivalence P).functor ⋙
    CostructuredArrow.proj uliftYoneda.{max w v₂, v₁, u₁} P ⋙ A ≅
  functorToRepresentables P ⋙ L :=
  (CategoryOfElements.costructuredArrowULiftYonedaEquivalence P).functor.isoWhiskerLeft
      (Functor.isoWhiskerLeft (CostructuredArrow.proj uliftYoneda.{max w v₂, v₁, u₁} P) (asIso α)) ≪≫
    (CategoryOfElements.costructuredArrowULiftYonedaEquivalence P).functor.isoWhiskerLeft
        (Iso.symm
          (Functor.associator (CostructuredArrow.proj uliftYoneda.{max w v₂, v₁, u₁} P) uliftYoneda.{max w v₂, v₁, u₁}
            L)) ≪≫
      ((CategoryOfElements.costructuredArrowULiftYonedaEquivalence P).functor.associator
            (CostructuredArrow.proj uliftYoneda.{max w v₂, v₁, u₁} P ⋙ uliftYoneda.{max w v₂, v₁, u₁}) L).symm ≪≫
        Functor.isoWhiskerRight
          (Iso.refl
            ((CategoryOfElements.costructuredArrowULiftYonedaEquivalence P).functor ⋙
              CostructuredArrow.proj uliftYoneda.{max w v₂, v₁, u₁} P ⋙ uliftYoneda.{max w v₂, v₁, u₁}))
          L
mpr :
  IsColimit
    ((Cocone.precompose e.symm.hom).obj
      (Cocone.whisker (CategoryOfElements.costructuredArrowULiftYonedaEquivalence P).functor
        ((Functor.LeftExtension.mk L α).coconeAt P)))
⊢ IsColimit
    (Cocone.whisker (CategoryOfElements.costructuredArrowULiftYonedaEquivalence P).functor
      ((Functor.LeftExtension.mk L α).coconeAt P))

Tactic:
refine (IsColimit.precomposeHomEquiv e.symm _).1 ?_

Premises used: Equiv.toFun, CategoryTheory.Iso.symm, CategoryTheory.Limits.IsColimit.precomposeHomEquiv
-- Module: Mathlib.CategoryTheory.Limits.Presheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
ℰ : Type u₂
inst_1 : Category.{v₂, u₂} ℰ
A : Functor.{v₁, v₂, u₁, u₂} C ℰ
inst_2 : Functor.HasPointwiseLeftKanExtension uliftYoneda.{max w v₂, v₁, u₁} A
L : (Cᵒᵖ ⥤ Type (max w v₁ v₂)) ⥤ ℰ
α : A ⟶ uliftYoneda.{max w v₂, v₁, u₁} ⋙ L
left : IsIso α
right :
  PreservesColimitsOfSize.{v₁, max w u₁ v₁ v₂, max (max (max u₁ v₁) v₂) w, v₂,
      max (max (max u₁ (v₁ + 1)) (v₂ + 1)) (w + 1), u₂}
    L
P : Cᵒᵖ ⥤ Type (max (max w v₂) v₁)
e : (CategoryOfElements.costructuredArrowULiftYonedaEquivalence P).functor ⋙
    CostructuredArrow.proj uliftYoneda.{max w v₂, v₁, u₁} P ⋙ A ≅
  functorToRepresentables P ⋙ L :=
  (CategoryOfElements.costructuredArrowULiftYonedaEquivalence P).functor.isoWhiskerLeft
      (Functor.isoWhiskerLeft (CostructuredArrow.proj uliftYoneda.{max w v₂, v₁, u₁} P) (asIso α)) ≪≫
    (CategoryOfElements.costructuredArrowULiftYonedaEquivalence P).functor.isoWhiskerLeft
        (Iso.symm
          (Functor.associator (CostructuredArrow.proj uliftYoneda.{max w v₂, v₁, u₁} P) uliftYoneda.{max w v₂, v₁, u₁}
            L)) ≪≫
      ((CategoryOfElements.costructuredArrowULiftYonedaEquivalence P).functor.associator
            (CostructuredArrow.proj uliftYoneda.{max w v₂, v₁, u₁} P ⋙ uliftYoneda.{max w v₂, v₁, u₁}) L).symm ≪≫
        Functor.isoWhiskerRight
          (Iso.refl
            ((CategoryOfElements.costructuredArrowULiftYonedaEquivalence P).functor ⋙
              CostructuredArrow.proj uliftYoneda.{max w v₂, v₁, u₁} P ⋙ uliftYoneda.{max w v₂, v₁, u₁}))
          L
⊢ IsColimit
    ((Cocone.precompose e.symm.hom).obj
      (Cocone.whisker (CategoryOfElements.costructuredArrowULiftYonedaEquivalence P).functor
        ((Functor.LeftExtension.mk L α).coconeAt P)))

Tactic:
exact IsColimit.ofIsoColimit (isColimitOfPreserves L (colimitOfRepresentable.{max w v₂} P))
      (Cocone.ext (Iso.refl _))
-- Module: Mathlib.CategoryTheory.Limits.Presheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
ℰ : Type u₂
inst_1 : Category.{v₂, u₂} ℰ
A : Functor.{v₁, v₂, u₁, u₂} C ℰ
inst_2 : Functor.HasPointwiseLeftKanExtension uliftYoneda.{max w v₂, v₁, u₁} A
L : (Cᵒᵖ ⥤ Type (max w v₁ v₂)) ⥤ ℰ
e : A ≅ uliftYoneda.{max w v₂, v₁, u₁} ⋙ L
inst_3 :
  PreservesColimitsOfSize.{v₁, max w u₁ v₁ v₂, max (max (max u₁ v₁) v₂) w, v₂,
      max (max (max u₁ (v₁ + 1)) (v₂ + 1)) (w + 1), u₂}
    L
rw :
  IsIso e.hom ∧
    PreservesColimitsOfSize.{v₁, max w u₁ v₁ v₂, max (max (max u₁ v₁) v₂) w, v₂,
        max (max (max u₁ (v₁ + 1)) (v₂ + 1)) (w + 1), u₂}
      L
⊢ L.IsLeftKanExtension e.hom

Tactic:
rw [isLeftKanExtension_along_uliftYoneda_iff]

Premises used: CategoryTheory.Presheaf.isLeftKanExtension_along_uliftYoneda_iff
-- Module: Mathlib.CategoryTheory.Limits.Presheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
ℰ : Type u₂
inst_1 : Category.{v₂, u₂} ℰ
A : Functor.{v₁, v₂, u₁, u₂} C ℰ
inst_2 : Functor.HasPointwiseLeftKanExtension uliftYoneda.{max w v₂, v₁, u₁} A
L : (Cᵒᵖ ⥤ Type (max w v₁ v₂)) ⥤ ℰ
e : A ≅ uliftYoneda.{max w v₂, v₁, u₁} ⋙ L
inst_3 :
  PreservesColimitsOfSize.{v₁, max w u₁ v₁ v₂, max (max (max u₁ v₁) v₂) w, v₂,
      max (max (max u₁ (v₁ + 1)) (v₂ + 1)) (w + 1), u₂}
    L
⊢ IsIso e.hom ∧
    PreservesColimitsOfSize.{v₁, max w u₁ v₁ v₂, max (max (max u₁ v₁) v₂) w, v₂,
        max (max (max u₁ (v₁ + 1)) (v₂ + 1)) (w + 1), u₂}
      L

Tactic:
⟨inferInstance, ⟨inferInstance⟩⟩

Premises used: inferInstance, CategoryTheory.Limits.PreservesColimitsOfSize.mk, And.intro
-- Module: Mathlib.CategoryTheory.Limits.Presheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
ℰ : Type u₂
inst_1 : Category.{v₂, u₂} ℰ
A : Functor.{v₁, v₂, u₁, u₂} C ℰ
inst_2 : Functor.HasPointwiseLeftKanExtension uliftYoneda.{max w v₂, v₁, u₁} A
L : (Cᵒᵖ ⥤ Type (max w v₁ v₂)) ⥤ ℰ
e : A ≅ uliftYoneda.{max w v₂, v₁, u₁} ⋙ L
inst_3 :
  PreservesColimitsOfSize.{v₁, max w u₁ v₁ v₂, max (max (max u₁ v₁) v₂) w, v₂,
      max (max (max u₁ (v₁ + 1)) (v₂ + 1)) (w + 1), u₂}
    L
⊢ IsIso e.hom ∧
    PreservesColimitsOfSize.{v₁, max w u₁ v₁ v₂, max (max (max u₁ v₁) v₂) w, v₂,
        max (max (max u₁ (v₁ + 1)) (v₂ + 1)) (w + 1), u₂}
      L

Tactic:
exact ⟨inferInstance, ⟨inferInstance⟩⟩
-- 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
L : (Cᵒᵖ ⥤ Type (max w v₁ v₂)) ⥤ ℰ
inst_3 :
  PreservesColimitsOfSize.{v₁, max w u₁ v₁ v₂, max (max (max u₁ v₁) v₂) w, v₂,
      max (max (max u₁ (v₁ + 1)) (v₂ + 1)) (w + 1), u₂}
    L
inst_4 : Functor.HasPointwiseLeftKanExtension uliftYoneda.{max w v₂, v₁, u₁} (uliftYoneda.{max w v₂, v₁, u₁} ⋙ L)
⊢ L.IsLeftKanExtension (𝟙 (uliftYoneda.{max w v₂, v₁, u₁} ⋙ L))

Tactic:
isLeftKanExtension_of_preservesColimits _ (Iso.refl _)

Premises used: CategoryTheory.Iso.refl, CategoryTheory.Presheaf.isLeftKanExtension_of_preservesColimits
-- Module: Mathlib.CategoryTheory.Limits.Presheaf
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
ℰ : Type u₂
inst_1 : Category.{v₂, u₂} ℰ
L : (C ⥤ Type (max w v₁ v₂)) ⥤ ℰ
inst_2 :
  PreservesColimitsOfSize.{v₁, max w u₁ v₁ v₂, max (max (max u₁ v₁) v₂) w, v₂,
      max (max (max u₁ (v₁ + 1)) (v₂ + 1)) (w + 1), u₂}
    L
inst_3 :
  Functor.HasPointwiseLeftKanExtension uliftYoneda.{max w v₂, v₁, u₁}
    (uliftYoneda.{max w v₂, v₁, u₁} ⋙ Equivalence.functor (Equivalence.congrLeft (opOpEquivalence C)) ⋙ L)
⊢ L.IsLeftAdjoint

Tactic:
⟨_, ⟨((opOpEquivalence C).congrLeft.symm.toAdjunction.comp
    (uliftYonedaAdjunction _ (𝟙 _))).ofNatIsoLeft
      ((opOpEquivalence C).congrLeft.invFunIdAssoc L)⟩⟩

Premises used: CategoryTheory.Equivalence.congrLeft, CategoryTheory.CategoryStruct.id, Nonempty.intro, CategoryTheory.Presheaf.uliftYonedaAdjunction, CategoryTheory.opOpEquivalence, Exists.intro, CategoryTheory.Functor.IsLeftAdjoint.mk, CategoryTheory.Equivalence.toAdjunction, CategoryTheory.Equivalence.invFunIdAssoc, CategoryTheory.Adjunction.comp, CategoryTheory.Equivalence.symm, CategoryTheory.Adjunction.ofNatIsoLeft
-- 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 yoneda X)
w :
  ∀ (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 yoneda (F.obj X)) (yonedaMap F X)) ≫
              Functor.map (Functor.obj (Functor.whiskeringLeft Cᵒᵖ Dᵒᵖ (Type v₁)) F.op)
                ((Equiv.symm yonedaEquiv :
                    (a : (StructuredArrow.right Y).obj (op (F.obj X))) → yoneda.obj (F.obj X) ⟶ StructuredArrow.right Y)
                  ((yonedaEquiv :
                      (a : yoneda.obj X ⟶ F.op ⋙ StructuredArrow.right Y) → (F.op ⋙ StructuredArrow.right Y).obj (op X))
                    (StructuredArrow.hom Y))))
            Z))
        f =
      (hom (FC := TypeCat.Fun) ((StructuredArrow.hom Y).app Z)).toFun f
⊢ StructuredArrow.hom (Functor.LeftExtension.mk (Functor.obj yoneda (F.obj X)) (yonedaMap F X)) ≫
      Functor.map (Functor.obj (Functor.whiskeringLeft Cᵒᵖ Dᵒᵖ (Type v₁)) F.op)
        ((Equiv.symm yonedaEquiv :
            (a : (StructuredArrow.right Y).obj (op (F.obj X))) → yoneda.obj (F.obj X) ⟶ StructuredArrow.right Y)
          ((yonedaEquiv :
              (a : yoneda.obj X ⟶ F.op ⋙ StructuredArrow.right Y) → (F.op ⋙ StructuredArrow.right Y).obj (op X))
            (StructuredArrow.hom Y))) =
    StructuredArrow.hom Y

Tactic:
ext Z f
-- 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 yoneda X)
Z : Cᵒᵖ
f : Functor.obj (Functor.obj yoneda X) Z
⊢ Eq (α :=
    (Functor.obj (Functor.obj (Functor.whiskeringLeft Cᵒᵖ Dᵒᵖ (Type v₁)) F.op) (StructuredArrow.right Y)).obj
      (op (unop Z)))
    ((hom (FC := TypeCat.Fun)
            ((Functor.obj (Functor.obj (Functor.whiskeringLeft Cᵒᵖ Dᵒᵖ (Type v₁)) F.op) (StructuredArrow.right Y)).map
              (Quiver.Hom.op f)) :
          (a : (((Functor.whiskeringLeft Cᵒᵖ Dᵒᵖ (Type v₁)).obj F.op).obj (StructuredArrow.right Y)).obj (op X)) →
            (((Functor.whiskeringLeft Cᵒᵖ Dᵒᵖ (Type v₁)).obj F.op).obj (StructuredArrow.right Y)).obj (op (unop Z)))
        ((hom (FC := TypeCat.Fun) ((StructuredArrow.hom Y).app (op X)) :
              (a : (yoneda.obj X).obj (op X)) →
                (((Functor.whiskeringLeft Cᵒᵖ Dᵒᵖ (Type v₁)).obj F.op).obj (StructuredArrow.right Y)).obj (op X))
            (𝟙 X) :
          (Functor.obj (Functor.obj (Functor.whiskeringLeft Cᵒᵖ Dᵒᵖ (Type v₁)) F.op) (StructuredArrow.right Y)).obj
            (op X)) :
      (Functor.obj (Functor.obj (Functor.whiskeringLeft Cᵒᵖ Dᵒᵖ (Type v₁)) F.op) (StructuredArrow.right Y)).obj
        (op (unop Z)))
    ((hom (FC := TypeCat.Fun) ((StructuredArrow.hom Y).app (op (unop Z))) :
          (a : (yoneda.obj X).obj (op (unop Z))) →
            (((Functor.whiskeringLeft Cᵒᵖ Dᵒᵖ (Type v₁)).obj F.op).obj (StructuredArrow.right Y)).obj (op (unop Z)))
        ((hom (FC := TypeCat.Fun) (Functor.map (Functor.obj yoneda X) (Quiver.Hom.op f)) :
              (a : (yoneda.obj X).obj (op X)) → (yoneda.obj X).obj (op (unop Z)))
            (𝟙 X) :
          Functor.obj (Functor.obj yoneda X) (op (unop Z))) :
      (Functor.obj (Functor.obj (Functor.whiskeringLeft Cᵒᵖ Dᵒᵖ (Type v₁)) F.op) (StructuredArrow.right Y)).obj
        (op (unop Z)))

Tactic:
(Y.hom.naturality_apply f.op _).symm

Premises used: CategoryTheory.NatTrans.naturality_apply, Quiver.Hom.op, CategoryTheory.StructuredArrow.hom, Eq.symm
-- 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 yoneda X)
Z : Cᵒᵖ
f : Functor.obj (Functor.obj yoneda X) Z
h :
  f =
    (hom (FC := TypeCat.Fun) (Functor.map (Functor.obj yoneda X) (Quiver.Hom.op f)) :
        (a : (yoneda.obj X).obj (op X)) → (yoneda.obj X).obj (op (unop Z)))
      (𝟙 X)
⊢ TypeCat.Fun.toFun
      (hom (FC := TypeCat.Fun)
        (NatTrans.app
          (StructuredArrow.hom (Functor.LeftExtension.mk (Functor.obj yoneda (F.obj X)) (yonedaMap F X)) ≫
            Functor.map (Functor.obj (Functor.whiskeringLeft Cᵒᵖ Dᵒᵖ (Type v₁)) F.op)
              ((Equiv.symm yonedaEquiv :
                  (a : (StructuredArrow.right Y).obj (op (F.obj X))) → yoneda.obj (F.obj X) ⟶ StructuredArrow.right Y)
                ((yonedaEquiv :
                    (a : yoneda.obj X ⟶ F.op ⋙ StructuredArrow.right Y) → (F.op ⋙ StructuredArrow.right Y).obj (op X))
                  (StructuredArrow.hom Y))))
          Z))
      f =
    (hom (FC := TypeCat.Fun) ((StructuredArrow.hom Y).app Z)).toFun f

Tactic:
convert! (Y.hom.naturality_apply f.op _).symm

Premises used: CategoryTheory.NatTrans.naturality_apply, Quiver.Hom.op, CategoryTheory.StructuredArrow.hom, Eq.symm
-- 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 yoneda X)
Z : Cᵒᵖ
f : Functor.obj (Functor.obj yoneda X) Z
⊢ f =
    (hom (FC := TypeCat.Fun) (Functor.map (Functor.obj yoneda X) (Quiver.Hom.op f)) :
        (a : (yoneda.obj X).obj (op X)) → (yoneda.obj X).obj (op (unop Z)))
      (𝟙 X)

Tactic:
simp
-- 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 yoneda X)
φ : Functor.LeftExtension.mk (Functor.obj yoneda (F.obj X)) (yonedaMap F X) ⟶ Y
h :
  StructuredArrow.Hom.right φ =
    StructuredArrow.Hom.right
      (StructuredArrow.homMk
        ((Equiv.symm yonedaEquiv :
            (a : (StructuredArrow.right Y).obj (op (F.obj X))) → yoneda.obj (F.obj X) ⟶ StructuredArrow.right Y)
          ((yonedaEquiv :
              (a : yoneda.obj X ⟶ F.op ⋙ StructuredArrow.right Y) → (F.op ⋙ StructuredArrow.right Y).obj (op X))
            (StructuredArrow.hom Y)))
        ⋯)
⊢ φ =
    StructuredArrow.homMk
      ((Equiv.symm yonedaEquiv :
          (a : (StructuredArrow.right Y).obj (op (F.obj X))) → yoneda.obj (F.obj X) ⟶ StructuredArrow.right Y)
        ((yonedaEquiv :
            (a : yoneda.obj X ⟶ F.op ⋙ StructuredArrow.right Y) → (F.op ⋙ StructuredArrow.right Y).obj (op X))
          (StructuredArrow.hom Y)))
      ⋯

Tactic:
ext1
-- 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 yoneda X)
φ : Functor.LeftExtension.mk (Functor.obj yoneda (F.obj X)) (yonedaMap F X) ⟶ Y
h :
  Eq.{v₁ + 1} (α := (StructuredArrow.right Y).obj (op (F.obj X)))
    ((yonedaEquiv : (a : yoneda.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)))
    ((yonedaEquiv : (a : yoneda.obj (F.obj X) ⟶ StructuredArrow.right Y) → (StructuredArrow.right Y).obj (op (F.obj X)))
        (StructuredArrow.Hom.right
          (StructuredArrow.homMk
            ((Equiv.symm yonedaEquiv :
                (a : (StructuredArrow.right Y).obj (op (F.obj X))) → yoneda.obj (F.obj X) ⟶ StructuredArrow.right Y)
              ((yonedaEquiv :
                  (a : yoneda.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 yonedaEquiv :
            (a : (StructuredArrow.right Y).obj (op (F.obj X))) → yoneda.obj (F.obj X) ⟶ StructuredArrow.right Y)
          ((yonedaEquiv :
              (a : yoneda.obj X ⟶ F.op ⋙ StructuredArrow.right Y) → (F.op ⋙ StructuredArrow.right Y).obj (op X))
            (StructuredArrow.hom Y)))
        ⋯)

Tactic:
apply yonedaEquiv.injective

Premises used: Equiv.injective, CategoryTheory.yonedaEquiv
-- 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 yoneda X)
φ : Functor.LeftExtension.mk (Functor.obj yoneda (F.obj X)) (yonedaMap F X) ⟶ Y
⊢ Eq.{v₁ + 1} (α := (StructuredArrow.right Y).obj (op (F.obj X)))
    ((yonedaEquiv : (a : yoneda.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)))
    ((yonedaEquiv : (a : yoneda.obj (F.obj X) ⟶ StructuredArrow.right Y) → (StructuredArrow.right Y).obj (op (F.obj X)))
        (StructuredArrow.Hom.right
          (StructuredArrow.homMk
            ((Equiv.symm yonedaEquiv :
                (a : (StructuredArrow.right Y).obj (op (F.obj X))) → yoneda.obj (F.obj X) ⟶ StructuredArrow.right Y)
              ((yonedaEquiv :
                  (a : yoneda.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 φ, yonedaEquiv, yonedaMap]

Premises used: CategoryTheory.yonedaMap, CategoryTheory.StructuredArrow.w, CategoryTheory.yonedaEquiv
-- 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 yoneda (F.obj X)) (yonedaMap 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
X : C
Y : F.op.LeftExtension (Functor.obj uliftYoneda.{max w v₂, v₁, u₁} X)
w :
  ∀ (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) }
⊢ 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))) =
    StructuredArrow.hom Y

Tactic:
ext Z ⟨f⟩