-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Indization.LocallySmall (goal)
Goal:
C : Type u
inst : Category.{v, u} C
I : Type u₁
inst_1 : Category.{v₁, u₁} I
inst_2 : HasColimitsOfShape.{v₁, u₁, v, v + 1} I (Type v)
inst_3 : HasLimitsOfShape.{v₁, u₁, v, v + 1} Iᵒᵖ (Type v)
inst_4 : HasLimitsOfShape Iᵒᵖ (Type (max u v))
F : Functor.{v₁, v, u₁, u} I C
G : Functor.{v, v, u, v + 1} Cᵒᵖ (Type v)
η : colimit (F ⋙ yoneda) ⟶ G
i : Iᵒᵖ
this :
  ∀ (a : limit ((F.op ⋙ G) ⋙ uliftFunctor.{u, v})),
    Eq.{v + 1} (α := (F.op ⋙ G).obj i)
      (ULift.down.{u, v}
        (((ConcreteCategory.hom (FC := TypeCat.Fun)
                (CategoryStruct.comp (Y := uliftFunctor.{u, v}.obj (limit (F.op ⋙ G)))
                  (Iso.inv (preservesLimitIso uliftFunctor.{u, v} (F.op ⋙ G)))
                  (uliftFunctor.{u, v}.map (limit.π (F.op ⋙ G) i))) :
              TypeCat.Fun (limit ((F.op ⋙ G) ⋙ uliftFunctor.{u, v})) (uliftFunctor.{u, v}.obj ((F.op ⋙ G).obj i))) :
            (a : limit ((F.op ⋙ G) ⋙ uliftFunctor.{u, v})) → uliftFunctor.{u, v}.obj ((F.op ⋙ G).obj i))
          a))
      (ULift.down.{u, v}
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (limit.π ((F.op ⋙ G) ⋙ uliftFunctor.{u, v}) i) :
            (a : limit ((F.op ⋙ G) ⋙ uliftFunctor.{u, v})) → uliftFunctor.{u, v}.obj ((F.op ⋙ G).obj i))
          a))
⊢ Eq (α := G.obj (op (F.obj (unop i))))
    (ULift.down.{u, v}
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 (ULift.{u, v} (G.obj (op (F.obj (unop i)))))) :
            (a : ULift.{u, v} (G.obj (op (F.obj (unop i))))) → ULift.{u, v} (G.obj (op (F.obj (unop i)))))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (limit.π (F.op ⋙ G ⋙ uliftFunctor.{u, v}) i) :
              (a : limit (F.op ⋙ G ⋙ uliftFunctor.{u, v})) → ULift.{u, v} (G.obj (op (F.obj (unop i)))))
            (((ConcreteCategory.hom (FC := TypeCat.Fun) (Iso.hom (colimitYonedaHomIsoLimitOp F G)) :
                  TypeCat.Fun (colimit (F ⋙ yoneda) ⟶ G) (limit (F.op ⋙ G ⋙ uliftFunctor.{u, v}))) :
                (a : colimit (F ⋙ yoneda) ⟶ G) → limit (F.op ⋙ G ⋙ uliftFunctor.{u, v}))
              η))) :
      G.obj (op (F.obj (unop i))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (η.app (op (F.obj (unop i)))) :
          (a : (colimit (F ⋙ yoneda)).obj (op (F.obj (unop i)))) → G.obj (op (F.obj (unop i))))
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
                (NatTrans.app (colimit.ι (F ⋙ yoneda) (unop i)) (op (F.obj (unop i)))) :
              (a : F.obj (unop i) ⟶ F.obj (unop i)) → (colimit (F ⋙ yoneda)).obj (op (F.obj (unop i))))
            (𝟙 (F.obj (unop i))) :
          (colimit (F ⋙ yoneda)).obj (op (F.obj (unop i)))) :
      G.obj (op (F.obj (unop i))))
have rw : Eq (α := G.obj (op (F.obj (unop i))))
  (ULift.down.{u, v}
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (𝟙 (ULift.{u, v} (G.obj (op (F.obj (unop i)))))) :
          (a : ULift.{u, v} (G.obj (op (F.obj (unop i))))) → ULift.{u, v} (G.obj (op (F.obj (unop i)))))
        {
          down :=
            (ConcreteCategory.hom (FC := TypeCat.Fun) (η.app (op (F.obj (unop i)))) :
                (a : (colimit (F ⋙ yoneda)).obj (op (F.obj (unop i)))) → G.obj (op (F.obj (unop i))))
              ((ConcreteCategory.hom (FC := TypeCat.Fun)
                      (NatTrans.app (colimit.ι (F ⋙ yoneda) (unop i)) (op (F.obj (unop i)))) :
                    (a : F.obj (unop i) ⟶ F.obj (unop i)) → (colimit (F ⋙ yoneda)).obj (op (F.obj (unop i))))
                  (𝟙 (F.obj (unop i))) :
                (colimit (F ⋙ yoneda)).obj (op (F.obj (unop i)))) }) :
    G.obj (op (F.obj (unop i))))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (η.app (op (F.obj (unop i)))) :
        (a : (colimit (F ⋙ yoneda)).obj (op (F.obj (unop i)))) → G.obj (op (F.obj (unop i))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (NatTrans.app (colimit.ι (F ⋙ yoneda) (unop i)) (op (F.obj (unop i)))) :
            (a : F.obj (unop i) ⟶ F.obj (unop i)) → (colimit (F ⋙ yoneda)).obj (op (F.obj (unop i))))
          (𝟙 (F.obj (unop i))) :
        (colimit (F ⋙ yoneda)).obj (op (F.obj (unop i)))) :
    G.obj (op (F.obj (unop i))))
Tactic: rw [colimitYonedaHomIsoLimitOp_π_apply]