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 ℰ
P : Cᵒᵖ ⥤ Type (max w v₁ v₂)
E : ℰ
f :
  Quiver.Hom (V := CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P ⥤ ℰ)
    (CostructuredArrow.proj uliftYoneda.{max w v₂, v₁, u₁} P ⋙ A)
    (Functor.obj (Functor.const (CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P)) E)
x x_1 : Cᵒᵖ
g : x ⟶ x_1
h :
  ∀ (x_2 : P.obj x),
    TypeCat.Fun.toFun
        (hom (FC := TypeCat.Fun)
          (P.map g ≫
            ↾fun (x : P.obj x_1) ↦
              {
                down :=
                  f.app
                    (CostructuredArrow.mk (Y := unop x_1)
                      ((Equiv.symm uliftYonedaEquiv :
                          (a : P.obj (op (unop x_1))) → uliftYoneda.{max v₂ w, v₁, u₁}.obj (unop x_1) ⟶ P)
                        x)) :
                ULift.{max v₁ w, v₂} (Functor.obj (Functor.obj yoneda E) (A.op.obj x_1)) }))
        x_2 =
      TypeCat.Fun.toFun
        (hom (FC := TypeCat.Fun)
          ((↾fun (x_3 : P.obj x) ↦
              {
                down :=
                  f.app
                    (CostructuredArrow.mk (Y := unop x)
                      ((Equiv.symm uliftYonedaEquiv :
                          (a : P.obj (op (unop x))) → uliftYoneda.{max v₂ w, v₁, u₁}.obj (unop x) ⟶ P)
                        x_3)) :
                ULift.{max v₁ w, v₂} (Functor.obj (Functor.obj yoneda E) (A.op.obj x)) }) ≫
            ((restrictedULiftYoneda A).obj E).map g))
        x_2
⊢ (P.map g ≫
      ↾fun (x : P.obj x_1) ↦
        {
          down :=
            f.app
              (CostructuredArrow.mk (Y := unop x_1)
                ((Equiv.symm uliftYonedaEquiv :
                    (a : P.obj (op (unop x_1))) → uliftYoneda.{max v₂ w, v₁, u₁}.obj (unop x_1) ⟶ P)
                  x)) }) =
    (↾fun (x_2 : P.obj x) ↦
        {
          down :=
            f.app
              (CostructuredArrow.mk (Y := unop x)
                ((Equiv.symm uliftYonedaEquiv :
                    (a : P.obj (op (unop x))) → uliftYoneda.{max v₂ w, v₁, u₁}.obj (unop x) ⟶ P)
                  x_2)) :
          ULift.{max v₁ w, v₂} (Functor.obj (Functor.obj yoneda E) (A.op.obj x)) }) ≫
      ((restrictedULiftYoneda A).obj E).map g

Tactic:
ext x
-- 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 ℰ
P : Cᵒᵖ ⥤ Type (max w v₁ v₂)
E : ℰ
f :
  Quiver.Hom (V := CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P ⥤ ℰ)
    (CostructuredArrow.proj uliftYoneda.{max w v₂, v₁, u₁} P ⋙ A)
    (Functor.obj (Functor.const (CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P)) E)
x_1 x_2 : Cᵒᵖ
g : x_1 ⟶ x_2
x : P.obj x_1
dsimp :
  Eq (α := Functor.obj uliftYoneda.{max w v₂, v₁, u₁} (unop x_2) ⟶ P)
    (Functor.map uliftYoneda.{max w v₂, v₁, u₁} g.unop ≫
      (Equiv.symm uliftYonedaEquiv : (a : P.obj x_1) → uliftYoneda.{max v₂ w, v₁, u₁}.obj (unop x_1) ⟶ P) x)
    ((Equiv.symm uliftYonedaEquiv : (a : P.obj x_2) → uliftYoneda.{max w v₂, v₁, u₁}.obj (unop x_2) ⟶ P)
      ((hom (FC := TypeCat.Fun) (P.map g) : (a : P.obj x_1) → P.obj x_2) x))
⊢ Eq (α :=
    Functor.obj uliftYoneda.{max w v₂, v₁, u₁}
        (CostructuredArrow.left (D := Cᵒᵖ ⥤ Type (max (max w v₂) v₁)) (S :=
          (uliftYoneda.{max w v₂, v₁, u₁} : C ⥤ Cᵒᵖ ⥤ Type (max (max w v₂) v₁))) (T := P)
          (CostructuredArrow.mk (Y := unop x_2)
              ((Equiv.symm uliftYonedaEquiv :
                  (a : P.obj (op (unop x_2))) → uliftYoneda.{max w v₂, v₁, u₁}.obj (unop x_2) ⟶ P)
                ((hom (FC := TypeCat.Fun) (P.map g) :
                    (a : (fun (X : Type (max (max v₁ v₂) w)) ↦ X) (P.obj x_1)) →
                      (fun (X : Type (max (max v₁ v₂) w)) ↦ X) (P.obj x_2))
                  x)) :
            CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P)) ⟶
      P)
    (Functor.map uliftYoneda.{max w v₂, v₁, u₁} g.unop ≫
      CostructuredArrow.hom
        (CostructuredArrow.mk (Y := unop x_1)
          ((Equiv.symm uliftYonedaEquiv :
              (a : P.obj (op (unop x_1))) → uliftYoneda.{max v₂ w, v₁, u₁}.obj (unop x_1) ⟶ P)
            x)))
    (CostructuredArrow.hom
      (CostructuredArrow.mk (Y := unop x_2)
        ((Equiv.symm uliftYonedaEquiv : (a : P.obj (op (unop x_2))) → uliftYoneda.{max w v₂, v₁, u₁}.obj (unop x_2) ⟶ P)
          ((hom (FC := TypeCat.Fun) (P.map g) :
              (a : (fun (X : Type (max (max v₁ v₂) w)) ↦ X) (P.obj x_1)) →
                (fun (X : Type (max (max v₁ v₂) w)) ↦ X) (P.obj x_2))
            x))))

Tactic:
dsimp
-- 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 ℰ
P : Cᵒᵖ ⥤ Type (max w v₁ v₂)
E : ℰ
f :
  Quiver.Hom (V := CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P ⥤ ℰ)
    (CostructuredArrow.proj uliftYoneda.{max w v₂, v₁, u₁} P ⋙ A)
    (Functor.obj (Functor.const (CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P)) E)
x_1 x_2 : Cᵒᵖ
g : x_1 ⟶ x_2
x : P.obj x_1
rw rw₁ :
  Eq (α := Functor.obj uliftYoneda.{max w v₂, v₁, u₁} (unop x_2) ⟶ P)
    (Functor.map uliftYoneda.{max w v₂, v₁, u₁} g.unop ≫
      (Equiv.symm uliftYonedaEquiv : (a : P.obj x_1) → uliftYoneda.{max v₂ w, v₁, u₁}.obj (unop x_1) ⟶ P) x)
    (Functor.map uliftYoneda.{max v₂ w, v₁, u₁} g.unop ≫
      (Equiv.symm uliftYonedaEquiv : (a : P.obj (op (unop x_1))) → uliftYoneda.{max v₂ w, v₁, u₁}.obj (unop x_1) ⟶ P) x)
⊢ Eq (α := Functor.obj uliftYoneda.{max w v₂, v₁, u₁} (unop x_2) ⟶ P)
    (Functor.map uliftYoneda.{max w v₂, v₁, u₁} g.unop ≫
      (Equiv.symm uliftYonedaEquiv : (a : P.obj x_1) → uliftYoneda.{max v₂ w, v₁, u₁}.obj (unop x_1) ⟶ P) x)
    ((Equiv.symm uliftYonedaEquiv : (a : P.obj x_2) → uliftYoneda.{max w v₂, v₁, u₁}.obj (unop x_2) ⟶ P)
      ((hom (FC := TypeCat.Fun) (P.map g) : (a : P.obj x_1) → P.obj x_2) x))

Tactic:
rw [uliftYonedaEquiv_symm_map]

Premises used: CategoryTheory.uliftYonedaEquiv_symm_map
-- 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 ℰ
P : Cᵒᵖ ⥤ Type (max w v₁ v₂)
E : ℰ
f :
  Quiver.Hom (V := CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P ⥤ ℰ)
    (CostructuredArrow.proj uliftYoneda.{max w v₂, v₁, u₁} P ⋙ A)
    (Functor.obj (Functor.const (CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P)) E)
x_1 x_2 : Cᵒᵖ
g : x_1 ⟶ x_2
x : P.obj x_1
φ : Quiver.Hom (V := CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P)
  (CostructuredArrow.mk (Y := unop x_2)
      ((Equiv.symm uliftYonedaEquiv : (a : P.obj (op (unop x_2))) → uliftYoneda.{max w v₂, v₁, u₁}.obj (unop x_2) ⟶ P)
        ((hom (FC := TypeCat.Fun) (P.map g) :
            (a : (fun (X : Type (max (max v₁ v₂) w)) ↦ X) (P.obj x_1)) →
              (fun (X : Type (max (max v₁ v₂) w)) ↦ X) (P.obj x_2))
          x)) :
    CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P)
  (CostructuredArrow.mk (Y := unop x_1)
      ((Equiv.symm uliftYonedaEquiv : (a : P.obj (op (unop x_1))) → uliftYoneda.{max v₂ w, v₁, u₁}.obj (unop x_1) ⟶ P)
        x) :
    CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P) :=
  CostructuredArrow.homMk g.unop ⋯
h :
  Eq (α := ((restrictedULiftYoneda A).obj E).obj x_2)
    ({
        down :=
          f.app
            (CostructuredArrow.mk (Y := unop x_2)
              ((Equiv.symm uliftYonedaEquiv : (a : P.obj x_2) → uliftYoneda.{max v₂ w, v₁, u₁}.obj (unop x_2) ⟶ P)
                ((hom (FC := TypeCat.Fun) (P.map g) : (a : P.obj x_1) → P.obj x_2) x))) } :
      ULift.{max v₁ w, v₂} (A.obj (unop x_2) ⟶ E))
    ({
        down :=
          A.map g.unop ≫
            f.app
              (CostructuredArrow.mk (Y := unop x_1)
                ((Equiv.symm uliftYonedaEquiv : (a : P.obj x_1) → uliftYoneda.{max v₂ w, v₁, u₁}.obj (unop x_1) ⟶ P)
                  x)) } :
      ULift.{max v₁ w, v₂} (A.obj (unop x_2) ⟶ E))
⊢ TypeCat.Fun.toFun
      (hom (FC := TypeCat.Fun)
        (P.map g ≫
          ↾fun (x : P.obj x_2) ↦
            {
              down :=
                f.app
                  (CostructuredArrow.mk (Y := unop x_2)
                    ((Equiv.symm uliftYonedaEquiv :
                        (a : P.obj (op (unop x_2))) → uliftYoneda.{max v₂ w, v₁, u₁}.obj (unop x_2) ⟶ P)
                      x)) :
              ULift.{max v₁ w, v₂} (Functor.obj (Functor.obj yoneda E) (A.op.obj x_2)) }))
      x =
    TypeCat.Fun.toFun
      (hom (FC := TypeCat.Fun)
        ((↾fun (x : P.obj x_1) ↦
            {
              down :=
                f.app
                  (CostructuredArrow.mk (Y := unop x_1)
                    ((Equiv.symm uliftYonedaEquiv :
                        (a : P.obj (op (unop x_1))) → uliftYoneda.{max v₂ w, v₁, u₁}.obj (unop x_1) ⟶ P)
                      x)) :
              ULift.{max v₁ w, v₂} (Functor.obj (Functor.obj yoneda E) (A.op.obj x_1)) }) ≫
          ((restrictedULiftYoneda A).obj E).map g))
      x

Tactic:
dsimp
-- 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 ℰ
P : Cᵒᵖ ⥤ Type (max w v₁ v₂)
E : ℰ
f :
  Quiver.Hom (V := CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P ⥤ ℰ)
    (CostructuredArrow.proj uliftYoneda.{max w v₂, v₁, u₁} P ⋙ A)
    (Functor.obj (Functor.const (CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P)) E)
x_1 x_2 : Cᵒᵖ
g : x_1 ⟶ x_2
x : P.obj x_1
φ : Quiver.Hom (V := CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P)
  (CostructuredArrow.mk (Y := unop x_2)
      ((Equiv.symm uliftYonedaEquiv : (a : P.obj (op (unop x_2))) → uliftYoneda.{max w v₂, v₁, u₁}.obj (unop x_2) ⟶ P)
        ((hom (FC := TypeCat.Fun) (P.map g) :
            (a : (fun (X : Type (max (max v₁ v₂) w)) ↦ X) (P.obj x_1)) →
              (fun (X : Type (max (max v₁ v₂) w)) ↦ X) (P.obj x_2))
          x)) :
    CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P)
  (CostructuredArrow.mk (Y := unop x_1)
      ((Equiv.symm uliftYonedaEquiv : (a : P.obj (op (unop x_1))) → uliftYoneda.{max v₂ w, v₁, u₁}.obj (unop x_1) ⟶ P)
        x) :
    CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P) :=
  CostructuredArrow.homMk g.unop ⋯
⊢ Eq (α := A.obj (unop x_2) ⟶ E)
    (f.app
        (CostructuredArrow.mk (Y := unop x_2)
          ((Equiv.symm uliftYonedaEquiv : (a : P.obj x_2) → uliftYoneda.{max v₂ w, v₁, u₁}.obj (unop x_2) ⟶ P)
            ((hom (FC := TypeCat.Fun) (P.map g) : (a : P.obj x_1) → P.obj x_2) x))) :
      Functor.obj (C := CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P)
          (CostructuredArrow.proj uliftYoneda.{max w v₂, v₁, u₁} P ⋙ A)
          (CostructuredArrow.mk (Y := unop x_2)
            ((Equiv.symm uliftYonedaEquiv : (a : P.obj x_2) → uliftYoneda.{max v₂ w, v₁, u₁}.obj (unop x_2) ⟶ P)
              ((hom (FC := TypeCat.Fun) (P.map g) : (a : P.obj x_1) → P.obj x_2) x))) ⟶
        Functor.obj (C := CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P)
          (Functor.obj (Functor.const (CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P)) E :
            CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P ⥤ ℰ)
          (CostructuredArrow.mk (Y := unop x_2)
              ((Equiv.symm uliftYonedaEquiv : (a : P.obj x_2) → uliftYoneda.{max v₂ w, v₁, u₁}.obj (unop x_2) ⟶ P)
                ((hom (FC := TypeCat.Fun) (P.map g) : (a : P.obj x_1) → P.obj x_2) x)) :
            CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P))
    (A.map g.unop ≫
      f.app
        (CostructuredArrow.mk (Y := unop x_1)
          ((Equiv.symm uliftYonedaEquiv : (a : P.obj x_1) → uliftYoneda.{max v₂ w, v₁, u₁}.obj (unop x_1) ⟶ P) x)))

Tactic:
simpa using (f.naturality φ).symm

Premises used: CategoryTheory.NatTrans.naturality, Eq.symm
-- 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 ℰ
P : Cᵒᵖ ⥤ Type (max w v₁ v₂)
E : ℰ
g : P ⟶ (restrictedULiftYoneda A).obj E
y y' : CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P
f : y ⟶ y'
dsimp :
  A.map f.left ≫
      ULift.down
        ((uliftYonedaEquiv :
            (a : uliftYoneda.{max w v₂, v₁, u₁}.obj y'.left ⟶ (restrictedULiftYoneda A).obj E) →
              ((restrictedULiftYoneda A).obj E).obj (op y'.left))
          (y'.hom ≫ g)) =
    ULift.down
        ((uliftYonedaEquiv :
            (a : uliftYoneda.{max w v₂, v₁, u₁}.obj y.left ⟶ (restrictedULiftYoneda A).obj E) →
              ((restrictedULiftYoneda A).obj E).obj (op y.left))
          (y.hom ≫ g)) ≫
      𝟙 E
⊢ Eq (α :=
    Functor.obj (CostructuredArrow.proj uliftYoneda.{max w v₂, v₁, u₁} P ⋙ A) y ⟶
      Functor.obj (Functor.obj (Functor.const (CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P)) E) y')
    (Functor.map (CostructuredArrow.proj uliftYoneda.{max w v₂, v₁, u₁} P ⋙ A) f ≫
      ULift.down
        ((uliftYonedaEquiv :
            (a : uliftYoneda.{max w v₂, v₁, u₁}.obj y'.left ⟶ (restrictedULiftYoneda A).obj E) →
              ((restrictedULiftYoneda A).obj E).obj (op y'.left))
          (y'.hom ≫ g)))
    (ULift.down
        ((uliftYonedaEquiv :
            (a : uliftYoneda.{max w v₂, v₁, u₁}.obj y.left ⟶ (restrictedULiftYoneda A).obj E) →
              ((restrictedULiftYoneda A).obj E).obj (op y.left))
          (y.hom ≫ g)) ≫
      Functor.map (Functor.obj (Functor.const (CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P)) E) f)

Tactic:
dsimp
-- 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 ℰ
P : Cᵒᵖ ⥤ Type (max w v₁ v₂)
E : ℰ
f :
  Quiver.Hom (V := CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P ⥤ ℰ)
    (CostructuredArrow.proj uliftYoneda.{max w v₂, v₁, u₁} P ⋙ A)
    (Functor.obj (Functor.const (CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P)) E)
X : CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P
Y : Cᵒᵖ
x :
  Functor.obj
    (Functor.obj uliftYoneda.{max w v₂, v₁, u₁}
      (CostructuredArrow.left (D := Cᵒᵖ ⥤ Type (max (max w v₂) v₁)) (S :=
        (uliftYoneda.{max w v₂, v₁, u₁} : C ⥤ Cᵒᵖ ⥤ Type (max (max w v₂) v₁))) (T := P)
        (CostructuredArrow.mk (Y := X.left)
            ((Equiv.symm uliftYonedaEquiv : (a : P.obj (op X.left)) → uliftYoneda.{max w v₂, v₁, u₁}.obj X.left ⟶ P)
              ((hom (FC := TypeCat.Fun) (X.hom.app (op X.left)) :
                  (a :
                      (fun (X : Type (max (max v₁ v₂) w)) ↦ X)
                        ((uliftYoneda.{max w v₂, v₁, u₁}.obj X.left).obj (op X.left))) →
                    (fun (X : Type (max (max v₁ v₂) w)) ↦ X) (P.obj (op X.left)))
                { down := 𝟙 X.left })) :
          CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P)))
    Y
⊢ Eq (α := P.obj Y)
    ((hom (FC := TypeCat.Fun) (X.hom.app Y) : (a : ULift.{max v₂ w, v₁} (unop Y ⟶ X.left)) → P.obj Y)
        { down := x.down ≫ 𝟙 X.left } :
      P.obj Y)
    ((hom (FC := TypeCat.Fun) (P.map x.down.op) : (a : P.obj (op X.left)) → P.obj Y)
        (((@hom _ types TypeCat.Fun _ _ _ _ _ (X.hom.app (op X.left)) :
              TypeCat.Fun (ULift.{max v₂ w, v₁} (X.left ⟶ X.left)) (P.obj (op X.left))) :
            (a : ULift.{max v₂ w, v₁} (X.left ⟶ X.left)) → P.obj (op X.left))
          { down := 𝟙 X.left }) :
      P.obj Y)

Tactic:
simp [← NatTrans.naturality_apply]

Premises used: CategoryTheory.NatTrans.naturality_apply
-- 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 ℰ
P : Cᵒᵖ ⥤ Type (max w v₁ v₂)
E : ℰ
g : P ⟶ (restrictedULiftYoneda A).obj E
X : Cᵒᵖ
x : P.obj X
⊢ ULift.down
      (TypeCat.Fun.toFun
        (hom (FC := TypeCat.Fun)
          (NatTrans.app
            ((fun
                  (f :
                    Quiver.Hom (V := CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P ⥤ ℰ)
                      (CostructuredArrow.proj uliftYoneda.{max w v₂, v₁, u₁} P ⋙ A)
                      (Functor.obj (Functor.const (CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P)) E)) ↦
                ({
                    app := fun (x : Cᵒᵖ) ↦
                      ↾fun (x_1 : P.obj x) ↦
                        {
                          down :=
                            f.app
                              (CostructuredArrow.mk (Y := unop x)
                                ((Equiv.symm uliftYonedaEquiv :
                                    (a : P.obj (op (unop x))) → uliftYoneda.{max v₂ w, v₁, u₁}.obj (unop x) ⟶ P)
                                  x_1)) :
                          ULift.{max v₁ w, v₂} (Functor.obj (Functor.obj yoneda E) (A.op.obj x)) },
                    naturality := ⋯ } :
                  NatTrans P ((restrictedULiftYoneda A).obj E)))
              ((fun (g : P ⟶ (restrictedULiftYoneda A).obj E) ↦
                  ({
                      app := fun (y : CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P) ↦
                        ULift.down
                          ((uliftYonedaEquiv :
                              (a : uliftYoneda.{max w v₂, v₁, u₁}.obj y.left ⟶ (restrictedULiftYoneda A).obj E) →
                                ((restrictedULiftYoneda A).obj E).obj (op y.left))
                            (y.hom ≫ g)),
                      naturality := ⋯ } :
                    NatTrans (C := CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P)
                      (CostructuredArrow.proj uliftYoneda.{max w v₂, v₁, u₁} P ⋙ A)
                      (Functor.obj (Functor.const (CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P)) E)))
                g))
            X))
        x) =
    ((hom (FC := TypeCat.Fun) (g.app X)).toFun x).down

Tactic:
simp [uliftYonedaEquiv]

Premises used: CategoryTheory.uliftYonedaEquiv
-- 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 ℰ
P : Cᵒᵖ ⥤ Type (max w v₁ v₂)
E E' : ℰ
g : E ⟶ E'
f : P ⟶ (restrictedULiftYoneda A).obj E
⊢ Eq (α :=
    Quiver.Hom (V := CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P ⥤ ℰ)
      (CostructuredArrow.proj uliftYoneda.{max w v₂, v₁, u₁} P ⋙ A)
      (Functor.obj (Functor.const (CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P)) E'))
    (((restrictedULiftYonedaHomEquiv'.{w, v₁, v₂, u₁, u₂} A P E').symm :
          (a : P ⟶ (restrictedULiftYoneda A).obj E') →
            CostructuredArrow.proj uliftYoneda.{max w v₂, v₁, u₁} P ⋙ A ⟶
              (Functor.const (CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P)).obj E')
        (f ≫ (restrictedULiftYoneda A).map g) :
      Quiver.Hom (V := CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P ⥤ ℰ)
        (CostructuredArrow.proj uliftYoneda.{max w v₂, v₁, u₁} P ⋙ A)
        (Functor.obj (Functor.const (CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P)) E'))
    (((restrictedULiftYonedaHomEquiv'.{w, v₁, v₂, u₁, u₂} A P E).symm :
            (a : P ⟶ (restrictedULiftYoneda A).obj E) →
              CostructuredArrow.proj uliftYoneda.{max w v₂, v₁, u₁} P ⋙ A ⟶
                (Functor.const (CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P)).obj E)
          f ≫
        Functor.map (Functor.const (CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P)) g :
      Quiver.Hom (V := CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P ⥤ ℰ)
        (CostructuredArrow.proj uliftYoneda.{max w v₂, v₁, u₁} P ⋙ A)
        (Functor.obj (Functor.const (CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P)) E'))

Tactic:
rfl
-- 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 ℰ
P Q : Cᵒᵖ ⥤ Type (max w v₁ v₂)
f : P ⟶ Q
E : ℰ
g : Q ⟶ (restrictedULiftYoneda A).obj E
p : CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P
⊢ Eq.{v₂ + 1} (α :=
    Functor.obj (CostructuredArrow.proj uliftYoneda.{max w v₂, v₁, u₁} P ⋙ A) p ⟶
      Functor.obj (Functor.obj (Functor.const (CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P)) E) p)
    (NatTrans.app
      (((restrictedULiftYonedaHomEquiv'.{w, v₁, v₂, u₁, u₂} A P E).symm :
          (a : P ⟶ (restrictedULiftYoneda A).obj E) →
            CostructuredArrow.proj uliftYoneda.{max w v₂, v₁, u₁} P ⋙ A ⟶
              (Functor.const (CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P)).obj E)
        (f ≫ g))
      p)
    (NatTrans.app
      (((restrictedULiftYonedaHomEquiv'.{w, v₁, v₂, u₁, u₂} A Q E).symm :
          (a : Q ⟶ (restrictedULiftYoneda A).obj E) →
            CostructuredArrow.proj uliftYoneda.{max w v₂, v₁, u₁} Q ⋙ A ⟶
              (Functor.const (CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} Q)).obj E)
        g)
      (Functor.obj (CostructuredArrow.map f) p))

Tactic:
rfl

Premises used: CategoryTheory.CostructuredArrow, rfl
-- 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 ℰ
P : ℰᵒᵖ ⥤ Type (max w v₁ v₂)
inst_2 : HasColimitsOfSize.{v₁, max u₁ v₁ v₂ w, v₂, u₂} ℰ
⊢ Functor.HasPointwiseLeftKanExtension uliftYoneda.{max w v₂, v₁, u₁} A

Tactic:
infer_instance
-- 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 ℰ
P_1 : ℰᵒᵖ ⥤ Type (max w v₁ v₂)
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
inst_3 : L.IsLeftKanExtension α
P Q : Cᵒᵖ ⥤ Type (max w v₁ v₂)
X : ℰ
f : P ⟶ Q
g : Q ⟶ (restrictedULiftYoneda A).obj X
apply :
  ∀ (j : CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P),
    Eq (α := Functor.obj (CostructuredArrow.proj uliftYoneda.{max w v₂, v₁, u₁} P ⋙ A) j ⟶ X)
      (((Functor.LeftExtension.mk L α).coconeAt P).ι.app j ≫
        ((restrictedULiftYonedaHomEquiv.{w, v₁, v₂, u₁, u₂} L α P X).symm :
            (a : P ⟶ (restrictedULiftYoneda A).obj X) → L.obj P ⟶ X)
          (f ≫ g))
      (((Functor.LeftExtension.mk L α).coconeAt P).ι.app j ≫
        L.map f ≫
          ((restrictedULiftYonedaHomEquiv.{w, v₁, v₂, u₁, u₂} L α Q X).symm :
              (a : Q ⟶ (restrictedULiftYoneda A).obj X) → L.obj Q ⟶ X)
            g)
⊢ Eq.{v₂ + 1} (α := L.obj P ⟶ X)
    (((restrictedULiftYonedaHomEquiv.{w, v₁, v₂, u₁, u₂} L α P X).symm :
          (a : P ⟶ (restrictedULiftYoneda A).obj X) → L.obj P ⟶ X)
        (f ≫ g) :
      L.obj P ⟶ X)
    (L.map f ≫
        ((restrictedULiftYonedaHomEquiv.{w, v₁, v₂, u₁, u₂} L α Q X).symm :
            (a : Q ⟶ (restrictedULiftYoneda A).obj X) → L.obj Q ⟶ X)
          g :
      L.obj P ⟶ X)

Tactic:
apply (Functor.isPointwiseLeftKanExtensionOfIsLeftKanExtension L α P).hom_ext

Premises used: CategoryTheory.Limits.IsColimit.hom_ext, CategoryTheory.Functor.isPointwiseLeftKanExtensionOfIsLeftKanExtension