-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Presheaf (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G : (Cᵒᵖ ⥤ Type (max w v₁ v₂)) ⥤ Dᵒᵖ ⥤ Type (max w v₁ v₂)
φ : F ⋙ uliftYoneda.{max w v₁, v₂, u₂} ⟶ uliftYoneda.{max w v₂, v₁, u₁} ⋙ G
P : Cᵒᵖ ⥤ Type (max w v₁ v₂)
x y : P.Elements
f : x ⟶ y
eq₁ :
  Eq (α := Functor.obj uliftYoneda.{max v₂ w, v₁, u₁} (unop (y.fst (β := fun (c : Cᵒᵖ) ↦ P.obj c))) ⟶ P)
    (Functor.map uliftYoneda.{max v₂ w, v₁, u₁} (↑f : x.fst ⟶ y.fst).unop ≫
      (Equiv.symm uliftYonedaEquiv :
          (a : P.obj (op (unop x.fst))) → uliftYoneda.{max v₂ w, v₁, u₁}.obj (unop x.fst) ⟶ P)
        (x.snd (β := fun (c : Cᵒᵖ) ↦ P.obj c)))
    ((Equiv.symm uliftYonedaEquiv : (a : P.obj (op (unop y.1))) → uliftYoneda.{max w v₂, v₁, u₁}.obj (unop y.1) ⟶ P)
      (y.snd (β := fun (c : Cᵒᵖ) ↦ P.obj c)))
⊢ Functor.map uliftYoneda.{max v₂ w, v₁, u₁} (↑f : x.fst ⟶ y.fst).unop ≫ coconeApp.{w, v₁, v₂, u₁, u₂} φ x =
    coconeApp.{w, v₁, v₂, u₁, u₂} φ y
have eq₂ : Eq (α := (G.obj P).obj (op (F.obj (unop (y.fst (β := fun (c : Cᵒᵖ) ↦ P.obj c))))))
  ((hom (FC := TypeCat.Fun)
          ((G.obj (Functor.obj uliftYoneda.{max w v₂, v₁, u₁} (unop x.1))).map (F.map (↑f : x.fst ⟶ y.fst).unop).op ≫
            NatTrans.app
              (G.map
                ((Equiv.symm uliftYonedaEquiv :
                    (a : P.obj (op (unop x.1))) → uliftYoneda.{max w v₂, v₁, u₁}.obj (unop x.1) ⟶ P)
                  (x.snd (β := fun (c : Cᵒᵖ) ↦ P.obj c))))
              (op (F.obj (unop (y.fst (β := fun (c : Cᵒᵖ) ↦ P.obj c)))))) :
        (a : (G.obj (uliftYoneda.{max w v₂, v₁, u₁}.obj (unop x.1))).obj (op (F.obj (unop x.fst)))) →
          (G.obj P).obj (op (F.obj (unop y.fst))))
      ((hom (FC := TypeCat.Fun)
            (NatTrans.app (φ.app (unop (x.fst (β := fun (c : Cᵒᵖ) ↦ P.obj c))))
              (op (F.1 (unop (x.fst (β := fun (c : Cᵒᵖ) ↦ P.obj c)))))) :
          (a :
              (fun (X : Type (max (max v₁ v₂) w)) ↦ X)
                (((F ⋙ uliftYoneda.{max w v₁, v₂, u₂}).obj (unop x.fst)).obj (op (F.1 (unop x.fst))))) →
            (fun (X : Type (max (max v₁ v₂) w)) ↦ X)
              (((uliftYoneda.{max w v₂, v₁, u₁} ⋙ G).obj (unop x.fst)).obj (op (F.1 (unop x.fst)))))
        { down := 𝟙 (unop (op (F.1 (unop (x.fst (β := fun (c : Cᵒᵖ) ↦ P.obj c)))))) }) :
    (G.obj P).obj (op (F.obj (unop (y.fst (β := fun (c : Cᵒᵖ) ↦ P.obj c))))))
  ((hom (FC := TypeCat.Fun)
          (NatTrans.app
              (G.map
                ((Equiv.symm uliftYonedaEquiv :
                    (a : P.obj (op (unop x.1))) → uliftYoneda.{max w v₂, v₁, u₁}.obj (unop x.1) ⟶ P)
                  (x.snd (β := fun (c : Cᵒᵖ) ↦ P.obj c))))
              (op (F.obj (unop (x.fst (β := fun (c : Cᵒᵖ) ↦ P.obj c))))) ≫
            (G.obj P).map (F.map (↑f : x.fst ⟶ y.fst).unop).op) :
        (a : (G.obj (uliftYoneda.{max w v₂, v₁, u₁}.obj (unop x.1))).obj (op (F.obj (unop x.fst)))) →
          (G.obj P).obj (op (F.obj (unop y.fst))))
      ((hom (FC := TypeCat.Fun)
            (NatTrans.app (φ.app (unop (x.fst (β := fun (c : Cᵒᵖ) ↦ P.obj c))))
              (op (F.1 (unop (x.fst (β := fun (c : Cᵒᵖ) ↦ P.obj c)))))) :
          (a :
              (fun (X : Type (max (max v₁ v₂) w)) ↦ X)
                (((F ⋙ uliftYoneda.{max w v₁, v₂, u₂}).obj (unop x.fst)).obj (op (F.1 (unop x.fst))))) →
            (fun (X : Type (max (max v₁ v₂) w)) ↦ X)
              (((uliftYoneda.{max w v₂, v₁, u₁} ⋙ G).obj (unop x.fst)).obj (op (F.1 (unop x.fst)))))
        { down := 𝟙 (unop (op (F.1 (unop (x.fst (β := fun (c : Cᵒᵖ) ↦ P.obj c)))))) }) :
    (G.obj P).obj (op (F.obj (unop (y.fst (β := fun (c : Cᵒᵖ) ↦ P.obj c))))))
Tactic: have eq₂ := ConcreteCategory.congr_hom ((G.map (uliftYonedaEquiv.{max w v₂}.symm x.2)).naturality
    (F.map f.1.unop).op) ((φ.app x.1.unop).app _ (ULift.up (𝟙 _)))