awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Yoneda (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
inst_2 : HasColimitsOfShape.{v₂, u₂, v₁, v₁ + 1} J (Type v₁)
inst_3 : HasColimitsOfShape J (Type (max u₁ v₁))
F : J ⥤ Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)
X : C
j : J
⊢ Eq (α := (F ⋙ obj coyoneda (op (obj yoneda X))).obj j ⟶ obj yoneda X ⟶ colimit F)
    ((F.whiskerLeft (NatTrans.app (Iso.hom largeCurriedYonedaLemma) (op X))).app j ≫
      CategoryStruct.comp (Y := colimit (F.flip.obj (op X) ⋙ uliftFunctor.{u₁, v₁}))
        (colimit.ι (F.flip.obj (op X) ⋙ uliftFunctor.{u₁, v₁}) j :
          (F.flip.obj (op X) ⋙ uliftFunctor.{u₁, v₁}).obj j ⟶ colimit (F.flip.obj (op X) ⋙ uliftFunctor.{u₁, v₁}))
        (CategoryStruct.comp (Y := ULift.{u₁, v₁} (colimit (F.flip.obj (op X))))
            (Iso.inv (preservesColimitIso uliftFunctor.{u₁, v₁} (F.flip.obj (op X))))
            ((↾fun (x : ULift.{u₁, v₁} (colimit (F.flip.obj (op X)))) ↦
                {
                  down :=
                    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Iso.inv (colimitObjIsoColimitCompEvaluation F (op X))) :
                          TypeCat.Fun (colimit (F.flip.obj (op X))) ((colimit F).obj (op X))) :
                        (a : colimit (F.flip.obj (op X))) → (colimit F).obj (op X))
                      x.down }) ≫
              (yonedaOpCompYonedaObj (colimit F)).inv.app (op X)) :
          colimit (F.flip.obj (op X) ⋙ uliftFunctor.{u₁, v₁}) ⟶ obj yoneda X ⟶ colimit F))
    (map (obj coyoneda (op (obj yoneda X))) (colimit.ι F j))
have w : Eq (α := (F ⋙ obj coyoneda (op (obj yoneda X))).obj j ⟶ obj yoneda X ⟶ colimit F)
  ((F.whiskerLeft (NatTrans.app (Iso.hom largeCurriedYonedaLemma) (op X))).app j ≫
    CategoryStruct.comp (Y := uliftFunctor.{u₁, v₁}.obj (colimit (F.flip.obj (op X))))
      (uliftFunctor.{u₁, v₁}.map (colimit.ι (F.flip.obj (op X)) j))
      ((↾fun (x : ULift.{u₁, v₁} (colimit (F.flip.obj (op X)))) ↦
          {
            down :=
              ((ConcreteCategory.hom (FC := TypeCat.Fun) (Iso.inv (colimitObjIsoColimitCompEvaluation F (op X))) :
                    TypeCat.Fun (colimit (F.flip.obj (op X))) ((colimit F).obj (op X))) :
                  (a : colimit (F.flip.obj (op X))) → (colimit F).obj (op X))
                x.down }) ≫
        (yonedaOpCompYonedaObj (colimit F)).inv.app (op X)))
  (map (obj coyoneda (op (obj yoneda X))) (colimit.ι F j))
Tactic: rw [ι_preservesColimitIso_inv_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Yoneda (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
inst_2 : HasColimitsOfShape.{v₂, u₂, v₁, v₁ + 1} J (Type v₁)
inst_3 : HasColimitsOfShape J (Type (max u₁ v₁))
F : J ⥤ Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)
X : C
j : J
⊢ Eq (α := (F ⋙ obj coyoneda (op (obj yoneda X))).obj j ⟶ obj yoneda X ⟶ colimit F)
    ((F.whiskerLeft (NatTrans.app (Iso.hom largeCurriedYonedaLemma) (op X))).app j ≫
      CategoryStruct.comp (Y := uliftFunctor.{u₁, v₁}.obj (colimit (F.flip.obj (op X))))
        (uliftFunctor.{u₁, v₁}.map (colimit.ι (F.flip.obj (op X)) j))
        ((↾fun (x : ULift.{u₁, v₁} (colimit (F.flip.obj (op X)))) ↦
            {
              down :=
                ((ConcreteCategory.hom (FC := TypeCat.Fun) (Iso.inv (colimitObjIsoColimitCompEvaluation F (op X))) :
                      TypeCat.Fun (colimit (F.flip.obj (op X))) ((colimit F).obj (op X))) :
                    (a : colimit (F.flip.obj (op X))) → (colimit F).obj (op X))
                  x.down }) ≫
          (yonedaOpCompYonedaObj (colimit F)).inv.app (op X)))
    (map (obj coyoneda (op (obj yoneda X))) (colimit.ι F j))
have w : Eq (α := (obj yoneda X ⟶ F.obj j) ⟶ obj yoneda X ⟶ colimit F)
  (NatTrans.app (NatTrans.app (Iso.hom largeCurriedYonedaLemma) (op X)) (F.obj j) ≫
    CategoryStruct.comp (Y := ULift.{u₁, v₁} (colimit (F ⋙ obj (evaluation Cᵒᵖ (Type v₁)) (op X))))
      (↾fun (x : ULift.{u₁, v₁} ((F.obj j).obj (op X))) ↦
        {
          down :=
            (ConcreteCategory.hom (FC := TypeCat.Fun) (colimit.ι (F ⋙ obj (evaluation Cᵒᵖ (Type v₁)) (op X)) j) :
                (a : (F.obj j).obj (op X)) → colimit (F ⋙ (evaluation Cᵒᵖ (Type v₁)).obj (op X)))
              x.down })
      ((↾fun (x : ULift.{u₁, v₁} (colimit (F ⋙ obj (evaluation Cᵒᵖ (Type v₁)) (op X)))) ↦
          {
            down :=
              ((ConcreteCategory.hom (FC := TypeCat.Fun) (Iso.inv (colimitObjIsoColimitCompEvaluation F (op X))) :
                    TypeCat.Fun (colimit (F ⋙ obj (evaluation Cᵒᵖ (Type v₁)) (op X))) ((colimit F).obj (op X))) :
                  (a : colimit (F ⋙ (evaluation Cᵒᵖ (Type v₁)).obj (op X))) → (colimit F).obj (op X))
                x.down }) ≫
        (yonedaOpCompYonedaObj (colimit F)).inv.app (op X)))
  (↾fun (g : obj yoneda X ⟶ F.obj j) ↦ g ≫ colimit.ι F j)
Tactic: simp only [← comp_evaluation, comp_obj, evaluation_obj_obj, yoneda_obj_obj, uliftFunctor_obj,
    whiskerLeft_app, uliftFunctor_map, Functor.comp_map, evaluation_obj_map, yoneda_map_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Yoneda (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
inst_2 : HasColimitsOfShape.{v₂, u₂, v₁, v₁ + 1} J (Type v₁)
inst_3 : HasColimitsOfShape J (Type (max u₁ v₁))
F : J ⥤ Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)
X : C
j : J
η : obj yoneda X ⟶ F.obj j
Y : Cᵒᵖ
f : obj (obj yoneda X) Y
⊢ Eq (α := (colimit F).obj Y)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((colimit F).map (Quiver.Hom.op f)) :
          (a : (colimit F).obj (op X)) → (colimit F).obj Y)
        (((ConcreteCategory.hom (FC := TypeCat.Fun) (Iso.inv (colimitObjIsoColimitCompEvaluation F (op X))) :
                TypeCat.Fun (colimit (F ⋙ obj (evaluation Cᵒᵖ (Type v₁)) (op X))) ((colimit F).obj (op X))) :
              (a : colimit (F ⋙ (evaluation Cᵒᵖ (Type v₁)).obj (op X))) → (colimit F).obj (op X))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (colimit.ι (F ⋙ obj (evaluation Cᵒᵖ (Type v₁)) (op X)) j) :
                  (a : (F.obj j).obj (op X)) → colimit (F ⋙ (evaluation Cᵒᵖ (Type v₁)).obj (op X)))
                ((ConcreteCategory.hom (FC := TypeCat.Fun) (η.app (op X)) : (a : X ⟶ X) → (F.obj j).obj (op X)) (𝟙 X) :
                  (F.obj j).obj (op X)) :
              colimit (F ⋙ obj (evaluation Cᵒᵖ (Type v₁)) (op X))) :
          (colimit F).obj (op X)) :
      (colimit F).obj Y)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (colimit.ι F j) Y) :
          (a : (F.obj j).obj Y) → (colimit F).obj Y)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (η.app Y) : (a : unop Y ⟶ X) → (F.obj j).obj Y) f :
          (F.obj j).obj Y) :
      (colimit F).obj Y)
have w : Eq (α := (colimit F).obj Y)
  ((ConcreteCategory.hom (FC := TypeCat.Fun) ((↾fun (g : X ⟶ X) ↦ f ≫ g) ≫ η.app Y ≫ NatTrans.app (colimit.ι F j) Y) :
        (a : X ⟶ X) → (colimit F).obj Y)
      (𝟙 X) :
    (colimit F).obj Y)
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (η.app Y ≫ NatTrans.app (colimit.ι F j) Y) :
        (a : unop Y ⟶ X) → (colimit F).obj Y)
      f :
    (colimit F).obj Y)
Tactic: simp only [← comp_apply, Category.assoc, colimitObjIsoColimitCompEvaluation_ι_inv,
    ← NatTrans.naturality, ← NatTrans.naturality_assoc, yoneda_obj_obj, yoneda_obj_map,
    Quiver.Hom.unop_op]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Yoneda (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
inst_2 : HasColimitsOfShape.{v₂, u₂, v₁, v₁ + 1} J (Type v₁)
inst_3 : HasColimitsOfShape J (Type (max u₁ v₁))
F : J ⥤ Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)
X : C
⊢ PreservesColimit F (obj coyoneda (op (obj yoneda X)))
have suffices : IsIso (X := colimit (F ⋙ obj coyoneda (op (obj yoneda X)))) (Y := obj (obj coyoneda (op (obj yoneda X))) (colimit F))
  (colimit.post F (obj coyoneda (op (obj yoneda X))))
Tactic: suffices IsIso (colimit.post F (coyoneda.obj (op (yoneda.obj X)))) from
    preservesColimit_of_isIso_post _ _
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Presheaf (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
ℰ : Type u₂
inst_1 : Category.{v₂, u₂} ℰ
A : Functor.{v₁, v₂, u₁, u₂} C ℰ
E : ℰ
X Y : C
f : X ⟶ Y
g : Functor.obj uliftYoneda.{max w v₂, v₁, u₁} Y ⟶ (restrictedULiftYoneda A).obj E
⊢ Eq (α := A.obj X ⟶ E)
    (A.map f ≫
      ULift.down
        ((uliftYonedaEquiv :
            (a : uliftYoneda.{max v₂ w, v₁, u₁}.obj Y ⟶ (restrictedULiftYoneda A).obj E) →
              ((restrictedULiftYoneda A).obj E).obj (op Y))
          g))
    (ULift.down
      ((uliftYonedaEquiv :
          (a : uliftYoneda.{max v₂ w, v₁, u₁}.obj X ⟶ (restrictedULiftYoneda A).obj E) →
            ((restrictedULiftYoneda A).obj E).obj (op X))
        (Functor.map uliftYoneda.{max v₂ w, v₁, u₁} f ≫ g)))
have this : Eq (α := ((restrictedULiftYoneda A).obj E).obj (op X))
  ((hom (FC := TypeCat.Fun) (g.app (op X)) :
        (a : (uliftYoneda.{max w v₂, v₁, u₁}.obj Y).obj (op X)) → ((restrictedULiftYoneda A).obj E).obj (op X))
      ((hom (FC := TypeCat.Fun) (Functor.map (Functor.obj uliftYoneda.{max w v₂, v₁, u₁} Y) f.op) :
          (a : (uliftYoneda.{max w v₂, v₁, u₁}.obj Y).obj (op Y)) → (uliftYoneda.{max w v₂, v₁, u₁}.obj Y).obj (op X))
        { down := 𝟙 Y }) :
    ((restrictedULiftYoneda A).obj E).obj (op X))
  ((hom (FC := TypeCat.Fun) (((restrictedULiftYoneda A).obj E).map f.op) :
        (a : ((restrictedULiftYoneda A).obj E).obj (op Y)) → ((restrictedULiftYoneda A).obj E).obj (op X))
      ((hom (FC := TypeCat.Fun) (g.app (op Y)) :
          (a : (uliftYoneda.{max w v₂, v₁, u₁}.obj Y).obj (op Y)) → ((restrictedULiftYoneda A).obj E).obj (op Y))
        { down := 𝟙 Y }) :
    ((restrictedULiftYoneda A).obj E).obj (op X))
Tactic: have this := (g.naturality_apply f.op) (ULift.up (𝟙 Y))
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Presheaf (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
ℰ : Type u₂
inst_1 : Category.{v₂, u₂} ℰ
A : Functor.{v₁, v₂, u₁, u₂} C ℰ
E : ℰ
X Y : C
f : X ⟶ Y
g : Functor.obj uliftYoneda.{max w v₂, v₁, u₁} Y ⟶ (restrictedULiftYoneda A).obj E
this :
  Eq (α := ((restrictedULiftYoneda A).obj E).obj (op X))
    ((hom (FC := TypeCat.Fun) (g.app (op X)) :
          (a : (uliftYoneda.{max w v₂, v₁, u₁}.obj Y).obj (op X)) → ((restrictedULiftYoneda A).obj E).obj (op X))
        ((hom (FC := TypeCat.Fun) (Functor.map (Functor.obj uliftYoneda.{max w v₂, v₁, u₁} Y) f.op) :
            (a : (uliftYoneda.{max w v₂, v₁, u₁}.obj Y).obj (op Y)) → (uliftYoneda.{max w v₂, v₁, u₁}.obj Y).obj (op X))
          { down := 𝟙 Y }) :
      ((restrictedULiftYoneda A).obj E).obj (op X))
    ((hom (FC := TypeCat.Fun) (((restrictedULiftYoneda A).obj E).map f.op) :
          (a : ((restrictedULiftYoneda A).obj E).obj (op Y)) → ((restrictedULiftYoneda A).obj E).obj (op X))
        ((hom (FC := TypeCat.Fun) (g.app (op Y)) :
            (a : (uliftYoneda.{max w v₂, v₁, u₁}.obj Y).obj (op Y)) → ((restrictedULiftYoneda A).obj E).obj (op Y))
          { down := 𝟙 Y }) :
      ((restrictedULiftYoneda A).obj E).obj (op X))
⊢ Eq (α := A.obj X ⟶ E)
    (A.map f ≫
      ULift.down
        ((uliftYonedaEquiv :
            (a : uliftYoneda.{max v₂ w, v₁, u₁}.obj Y ⟶ (restrictedULiftYoneda A).obj E) →
              ((restrictedULiftYoneda A).obj E).obj (op Y))
          g))
    (ULift.down
      ((uliftYonedaEquiv :
          (a : uliftYoneda.{max v₂ w, v₁, u₁}.obj X ⟶ (restrictedULiftYoneda A).obj E) →
            ((restrictedULiftYoneda A).obj E).obj (op X))
        (Functor.map uliftYoneda.{max v₂ w, v₁, u₁} f ≫ g)))
have dsimp : Eq (α := A.obj X ⟶ E)
  (A.map f ≫
    ULift.down
      ((hom (FC := TypeCat.Fun) (g.app (op Y)) :
          (a : ULift.{max v₂ w, v₁} (Y ⟶ Y)) → ((restrictedULiftYoneda A).obj E).obj (op Y))
        { down := 𝟙 Y }))
  (ULift.down
    ((hom (FC := TypeCat.Fun) (g.app (op X)) :
        (a : ULift.{max v₂ w, v₁} (X ⟶ Y)) → ((restrictedULiftYoneda A).obj E).obj (op X))
      { down := 𝟙 X ≫ f }))
Tactic: dsimp [uliftYonedaEquiv, uliftYoneda] at this ⊢
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Presheaf (goal)
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
⊢ (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
have 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
Tactic: ext x
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Presheaf (goal)
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
⊢ 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))))
have 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))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Presheaf (goal)
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
⊢ 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))
have 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)
Tactic: rw [uliftYonedaEquiv_symm_map]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Presheaf (goal)
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 ⋯
⊢ 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
have 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))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Presheaf (goal)
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'
⊢ 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)
have 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
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Presheaf (goal)
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'
⊢ 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
have rw : Eq (α := A.obj y.left ⟶ E)
  (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)))
Tactic: rw [comp_id, ← CostructuredArrow.w f, assoc, map_comp_uliftYonedaEquiv_down]