-- 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₁ :
  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)))
eq₂ :
  Eq (α := (Functor.obj F.op.lan (Functor.obj uliftYoneda.{max v₂ w, v₁, u₁} X)).obj (F.op.obj (op X)))
    ((hom (FC := TypeCat.Fun)
            ((uliftYonedaMap.{w, v₁, v₂, u₁, u₂} F X).app (op X) ≫
              NatTrans.app
                (Functor.descOfIsLeftKanExtension (Functor.obj uliftYoneda.{max w v₁, v₂, u₂} (F.obj X))
                  (uliftYonedaMap.{w, v₁, v₂, u₁, u₂} F X)
                  (Functor.obj F.op.lan (Functor.obj uliftYoneda.{max v₂ w, v₁, u₁} X))
                  (NatTrans.app F.op.lanUnit (Functor.obj uliftYoneda.{max v₂ w, v₁, u₁} X)))
                (F.op.obj (op X))) :
          (a : (uliftYoneda.{max w v₂, v₁, u₁}.obj X).obj (op X)) →
            (F.op.lan.obj (uliftYoneda.{max v₂ w, v₁, u₁}.obj X)).obj (F.op.obj (op X)))
        { down := 𝟙 (unop (op X)) } :
      (Functor.obj F.op.lan (Functor.obj uliftYoneda.{max v₂ w, v₁, u₁} X)).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₁} X)) (op X)) :
          (a : (uliftYoneda.{max w v₂, v₁, u₁}.obj X).obj (op X)) →
            (F.op.lan.obj (uliftYoneda.{max v₂ w, v₁, u₁}.obj X)).obj (F.op.obj (op X)))
        { down := 𝟙 (unop (op X)) } :
      (Functor.obj F.op.lan (Functor.obj uliftYoneda.{max v₂ w, v₁, u₁} X)).obj (F.op.obj (op X)))
eq₃ :
  Eq (α :=
    (Functor.obj (F.op.lan ⋙ Functor.obj (Functor.whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max (max w v₂) v₁))) F.op)
          (Functor.obj uliftYoneda.{max w v₂, v₁, u₁} Y)).obj
      (op X))
    ((hom (FC := TypeCat.Fun)
            (NatTrans.app
              (Functor.map (𝟭 (Cᵒᵖ ⥤ Type (max (max w v₂) v₁))) (Functor.map uliftYoneda.{max w v₂, v₁, u₁} f) ≫
                NatTrans.app F.op.lanUnit (Functor.obj uliftYoneda.{max w v₂, v₁, u₁} Y))
              (op X)) :
          (a : ((𝟭 (Cᵒᵖ ⥤ Type (max (max w v₂) v₁))).obj (uliftYoneda.{max w v₂, v₁, u₁}.obj X)).obj (op X)) →
            ((F.op.lan ⋙ (Functor.whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max (max w v₂) v₁))).obj F.op).obj
                  (uliftYoneda.{max w v₂, v₁, u₁}.obj Y)).obj
              (op X))
        { down := 𝟙 (unop (op X)) } :
      (Functor.obj (F.op.lan ⋙ Functor.obj (Functor.whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max (max w v₂) v₁))) F.op)
            (Functor.obj uliftYoneda.{max w v₂, v₁, u₁} Y)).obj
        (op X))
    ((hom (FC := TypeCat.Fun)
            (NatTrans.app
              (NatTrans.app F.op.lanUnit (Functor.obj uliftYoneda.{max w v₂, v₁, u₁} X) ≫
                Functor.map (F.op.lan ⋙ Functor.obj (Functor.whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max (max w v₂) v₁))) F.op)
                  (Functor.map uliftYoneda.{max w v₂, v₁, u₁} f))
              (op X)) :
          (a : ((𝟭 (Cᵒᵖ ⥤ Type (max (max w v₂) v₁))).obj (uliftYoneda.{max w v₂, v₁, u₁}.obj X)).obj (op X)) →
            ((F.op.lan ⋙ (Functor.whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max (max w v₂) v₁))).obj F.op).obj
                  (uliftYoneda.{max w v₂, v₁, u₁}.obj Y)).obj
              (op X))
        { down := 𝟙 (unop (op X)) } :
      (Functor.obj (F.op.lan ⋙ Functor.obj (Functor.whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max (max w v₂) v₁))) F.op)
            (Functor.obj uliftYoneda.{max w v₂, v₁, u₁} Y)).obj
        (op X))
a :
  Eq (α := (Functor.obj F.op.lan (Functor.obj yoneda Y ⋙ uliftFunctor.{max w v₂, v₁})).obj (op (F.obj X)))
    ((hom (FC := TypeCat.Fun)
            (NatTrans.app
              (Functor.descOfIsLeftKanExtension (Functor.obj yoneda (F.obj Y) ⋙ uliftFunctor.{max w v₁, v₂})
                {
                  app := fun (x : Cᵒᵖ) ↦
                    ↾fun (f : ULift.{max v₂ w, v₁} (unop x ⟶ Y)) ↦
                      { down := F.map f.down : ULift.{max v₁ w, v₂} (F.obj (unop x) ⟶ F.obj Y) },
                  naturality := ⋯ :
                  NatTrans (Functor.obj yoneda Y ⋙ uliftFunctor.{max w v₂, v₁})
                    (F.op ⋙ Functor.obj yoneda (F.obj Y) ⋙ uliftFunctor.{max w v₁, v₂}) }
                (Functor.obj F.op.lan (Functor.obj yoneda Y ⋙ uliftFunctor.{max w v₂, v₁}))
                (𝟙 (Functor.obj yoneda Y ⋙ uliftFunctor.{max w v₂, v₁}) ≫
                  NatTrans.app F.op.lanUnit (Functor.obj yoneda Y ⋙ uliftFunctor.{max v₂ w, v₁})))
              (op (F.obj X))) :
          (a : ULift.{max v₁ w, v₂} (F.obj X ⟶ F.obj Y)) →
            (F.op.lan.obj (yoneda.obj Y ⋙ uliftFunctor.{max w v₂, v₁})).obj (op (F.obj X)))
        { down := 𝟙 (F.obj X) ≫ F.map f } :
      (Functor.obj F.op.lan (Functor.obj yoneda Y ⋙ uliftFunctor.{max w v₂, v₁})).obj (op (F.obj X)))
    ((hom (FC := TypeCat.Fun)
            (NatTrans.app
              (Functor.map F.op.lan (Functor.whiskerRight (Functor.map yoneda f) uliftFunctor.{max w v₂, v₁}))
              (op (F.obj X))) :
          (a : (F.op.lan.obj (yoneda.obj X ⋙ uliftFunctor.{max w v₂, v₁})).obj (op (F.obj X))) →
            (F.op.lan.obj (yoneda.obj Y ⋙ uliftFunctor.{max w v₂, v₁})).obj (op (F.obj X)))
        ((hom (FC := TypeCat.Fun)
              (NatTrans.app
                (Functor.descOfIsLeftKanExtension (Functor.obj yoneda (F.obj X) ⋙ uliftFunctor.{max w v₁, v₂})
                  {
                    app := fun (x : Cᵒᵖ) ↦
                      ↾fun (f : ULift.{max v₂ w, v₁} (unop x ⟶ X)) ↦
                        { down := F.map f.down : ULift.{max v₁ w, v₂} (F.obj (unop x) ⟶ F.obj X) },
                    naturality := ⋯ :
                    NatTrans (Functor.obj yoneda X ⋙ uliftFunctor.{max w v₂, v₁})
                      (F.op ⋙ Functor.obj yoneda (F.obj X) ⋙ uliftFunctor.{max w v₁, v₂}) }
                  (Functor.obj F.op.lan (Functor.obj yoneda X ⋙ uliftFunctor.{max w v₂, v₁}))
                  (𝟙 (Functor.obj yoneda X ⋙ uliftFunctor.{max w v₂, v₁}) ≫
                    NatTrans.app F.op.lanUnit (Functor.obj yoneda X ⋙ uliftFunctor.{max v₂ w, v₁})))
                (op (F.obj X))) :
            (a : ULift.{max v₁ w, v₂} (F.obj X ⟶ F.obj X)) →
              (F.op.lan.obj (yoneda.obj X ⋙ uliftFunctor.{max w v₂, v₁})).obj (op (F.obj X)))
          { down := 𝟙 (F.obj X) }) :
      (Functor.obj F.op.lan (Functor.obj yoneda Y ⋙ uliftFunctor.{max w v₂, v₁})).obj (op (F.obj X)))
⊢ Eq (α := ((uliftYoneda.{max w v₂, v₁, u₁} ⋙ F.op.lan).obj Y).obj (op (F.obj X)))
    ((uliftYonedaEquiv :
          (a : uliftYoneda.{max v₁ w, v₂, u₂}.obj (F.obj X) ⟶ (uliftYoneda.{max w v₂, v₁, u₁} ⋙ F.op.lan).obj Y) →
            ((uliftYoneda.{max w v₂, v₁, u₁} ⋙ F.op.lan).obj Y).obj (op (F.obj X)))
        ((F ⋙ uliftYoneda.{max w v₁, v₂, u₂}).map f ≫
          Iso.hom
            ((fun (X : C) ↦
                (Functor.leftKanExtensionUnique (Functor.obj uliftYoneda.{max w v₁, v₂, u₂} (F.obj X))
                    (uliftYonedaMap.{w, v₁, v₂, u₁, u₂} F X)
                    (Functor.obj F.op.lan (Functor.obj uliftYoneda.{max w v₂, v₁, u₁} X))
                    (NatTrans.app F.op.lanUnit (Functor.obj uliftYoneda.{max v₂ w, v₁, u₁} X)) :
                  Functor.obj uliftYoneda.{max w v₁, v₂, u₂} (F.obj X) ≅
                    Functor.obj F.op.lan (Functor.obj uliftYoneda.{max w v₂, v₁, u₁} X)))
              Y)) :
      ((uliftYoneda.{max w v₂, v₁, u₁} ⋙ F.op.lan).obj Y).obj (op (F.obj X)))
    ((uliftYonedaEquiv :
          (a : uliftYoneda.{max v₁ w, v₂, u₂}.obj (F.obj X) ⟶ (uliftYoneda.{max w v₂, v₁, u₁} ⋙ F.op.lan).obj Y) →
            ((uliftYoneda.{max w v₂, v₁, u₁} ⋙ F.op.lan).obj Y).obj (op (F.obj X)))
        (Iso.hom
            ((fun (X : C) ↦
                (Functor.leftKanExtensionUnique (Functor.obj uliftYoneda.{max w v₁, v₂, u₂} (F.obj X))
                    (uliftYonedaMap.{w, v₁, v₂, u₁, u₂} F X)
                    (Functor.obj F.op.lan (Functor.obj uliftYoneda.{max w v₂, v₁, u₁} X))
                    (NatTrans.app F.op.lanUnit (Functor.obj uliftYoneda.{max v₂ w, v₁, u₁} X)) :
                  Functor.obj uliftYoneda.{max w v₁, v₂, u₂} (F.obj X) ≅
                    Functor.obj F.op.lan (Functor.obj uliftYoneda.{max w v₂, v₁, u₁} X)))
              X) ≫
          (uliftYoneda.{max w v₂, v₁, u₁} ⋙ F.op.lan).map f) :
      ((uliftYoneda.{max w v₂, v₁, u₁} ⋙ F.op.lan).obj Y).obj (op (F.obj X)))

Tactic:
dsimp [uliftYoneda, uliftYonedaMap, uliftYonedaEquiv,
        Functor.leftKanExtensionUnique] at eq₁ eq₂ eq₃ ⊢

Premises used: CategoryTheory.Functor.leftKanExtensionUnique, CategoryTheory.uliftYonedaMap, CategoryTheory.uliftYoneda, CategoryTheory.uliftYonedaEquiv