-- 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_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 yoneda Y ⋙ uliftFunctor.{max v₂ w, 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 v₂ w, 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 v₂ w, v₁})).obj (op (F.obj X)))
        { down := F.map f } :
      (Functor.obj F.op.lan (Functor.obj yoneda Y ⋙ uliftFunctor.{max v₂ w, v₁})).obj (op (F.obj X)))
    ((hom (FC := TypeCat.Fun)
            (NatTrans.app (NatTrans.app F.op.lanUnit (Functor.obj yoneda Y ⋙ uliftFunctor.{max v₂ w, v₁})) (op X)) :
          (a : ULift.{max v₂ w, v₁} (X ⟶ Y)) →
            (F.op.lan.obj (yoneda.obj Y ⋙ uliftFunctor.{max v₂ w, v₁})).obj (op (F.obj X)))
        { down := f } :
      (Functor.obj F.op.lan (Functor.obj yoneda Y ⋙ uliftFunctor.{max v₂ w, v₁})).obj (op (F.obj X)))
eq₃ :
  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 (NatTrans.app F.op.lanUnit (Functor.obj yoneda Y ⋙ uliftFunctor.{max w v₂, v₁})) (op X)) :
          (a : ULift.{max v₂ w, v₁} (X ⟶ Y)) →
            (F.op.lan.obj (yoneda.obj Y ⋙ uliftFunctor.{max w v₂, v₁})).obj (op (F.obj X)))
        { down := 𝟙 X ≫ 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 (NatTrans.app F.op.lanUnit (Functor.obj yoneda X ⋙ uliftFunctor.{max w v₂, v₁})) (op X)) :
            (a : ULift.{max v₂ w, v₁} (X ⟶ X)) →
              (F.op.lan.obj (yoneda.obj X ⋙ uliftFunctor.{max w v₂, v₁})).obj (op (F.obj X)))
          { down := 𝟙 X }) :
      (Functor.obj F.op.lan (Functor.obj yoneda Y ⋙ uliftFunctor.{max w v₂, v₁})).obj (op (F.obj X)))
eq₂ :
  Eq (α := (Functor.obj F.op.lan (Functor.obj yoneda X ⋙ uliftFunctor.{max v₂ w, 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 v₂ w, 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 v₂ w, v₁})).obj (op (F.obj X)))
        { down := 𝟙 (F.obj X) } :
      (Functor.obj F.op.lan (Functor.obj yoneda X ⋙ uliftFunctor.{max v₂ w, v₁})).obj (op (F.obj X)))
    ((hom (FC := TypeCat.Fun)
            (NatTrans.app (NatTrans.app F.op.lanUnit (Functor.obj yoneda X ⋙ uliftFunctor.{max v₂ w, v₁})) (op X)) :
          (a : ULift.{max v₂ w, v₁} (X ⟶ X)) →
            (F.op.lan.obj (yoneda.obj X ⋙ uliftFunctor.{max v₂ w, v₁})).obj (op (F.obj X)))
        { down := 𝟙 X } :
      (Functor.obj F.op.lan (Functor.obj yoneda X ⋙ uliftFunctor.{max v₂ w, v₁})).obj (op (F.obj X)))
⊢ 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)))
have eq₄ : 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 (NatTrans.app F.op.lanUnit (Functor.obj yoneda Y ⋙ uliftFunctor.{max w v₂, v₁})) (op X)) :
        (a : ULift.{max v₂ w, v₁} (X ⟶ Y)) →
          (F.op.lan.obj (yoneda.obj Y ⋙ uliftFunctor.{max w v₂, v₁})).obj (op (F.obj X)))
      { down := 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 (NatTrans.app F.op.lanUnit (Functor.obj yoneda X ⋙ uliftFunctor.{max w v₂, v₁})) (op X)) :
          (a : ULift.{max v₂ w, v₁} (X ⟶ X)) →
            (F.op.lan.obj (yoneda.obj X ⋙ uliftFunctor.{max w v₂, v₁})).obj (op (F.obj X)))
        { down := 𝟙 X }) :
    (Functor.obj F.op.lan (Functor.obj yoneda Y ⋙ uliftFunctor.{max w v₂, v₁})).obj (op (F.obj X)))
Tactic: simp only [id_comp] at eq₃
Cleared hypotheses: eq₃