-- Module: Mathlib.CategoryTheory.Limits.Indization.LocallySmall
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))
refine :
  Eq (α := G.obj (op (F.obj (unop i))))
    (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))
          ((ConcreteCategory.hom (FC := TypeCat.Fun)
                (Iso.hom (HasLimit.isoOfNatIso (F.op.associator G uliftFunctor.{u, v}).symm)) :
              (a : limit (F.op ⋙ G ⋙ uliftFunctor.{u, v})) → limit ((F.op ⋙ G) ⋙ uliftFunctor.{u, v}))
            (((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}))
              η))) :
      (F.op ⋙ G).obj 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))))
⊢ Eq (α := G.obj (op (F.obj (unop i))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (limit.π (F.op ⋙ G) i) :
          (a : limit (F.op ⋙ G)) → G.obj (op (F.obj (unop i))))
        (ULift.down.{u, v}
          (((ConcreteCategory.hom (FC := TypeCat.Fun) (Iso.inv (preservesLimitIso uliftFunctor.{u, v} (F.op ⋙ G))) :
                TypeCat.Fun (limit ((F.op ⋙ G) ⋙ uliftFunctor.{u, v})) (ULift.{u, v} (limit (F.op ⋙ G)))) :
              (a : limit ((F.op ⋙ G) ⋙ uliftFunctor.{u, v})) → ULift.{u, v} (limit (F.op ⋙ G)))
            ((ConcreteCategory.hom (FC := TypeCat.Fun)
                  (Iso.hom (HasLimit.isoOfNatIso (F.op.associator G uliftFunctor.{u, v}).symm)) :
                (a : limit (F.op ⋙ G ⋙ uliftFunctor.{u, v})) → limit ((F.op ⋙ G) ⋙ uliftFunctor.{u, v}))
              (((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))))

Tactic:
refine Eq.trans (dsimp% this _) ?_

Premises used: id, Eq.trans