-- 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 (α := (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)))

Tactic:
have eq₂ := ConcreteCategory.congr_hom
        (((uliftYoneda.{max w v₁}.obj (F.obj X)).descOfIsLeftKanExtension_fac_app
        (uliftYonedaMap F X) (F.op.lan.obj (uliftYoneda.obj X))
          (F.op.lanUnit.app (uliftYoneda.obj X))) _) ⟨𝟙 _⟩