-- Module: Mathlib.CategoryTheory.Limits.Preserves.Yoneda
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
inst_2 : HasColimitsOfShape.{v₂, u₂, v₁, v₁ + 1} J (Type v₁)
inst_3 : HasColimitsOfShape J (Type (max u₁ v₁))
F : J ⥤ Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)
X : C
rw :
  Eq (α := colimit (F ⋙ obj coyoneda (op (obj yoneda X))) ⟶ obj (obj coyoneda (op (obj yoneda X))) (colimit F))
    (colimit.post F (obj coyoneda (op (obj yoneda X))) :
      colimit (F ⋙ obj coyoneda (op (obj yoneda X))) ⟶ obj (obj coyoneda (op (obj yoneda X))) (colimit F))
    (CategoryStruct.comp (Y := (colimit (F ⋙ yoneda)).obj (obj (Functor.op yoneda) (op X)))
        (Iso.inv (colimitObjIsoColimitCompEvaluation (F ⋙ yoneda) (obj (Functor.op yoneda) (op X))) :
          colimit
              ((F ⋙ yoneda) ⋙
                obj (evaluation (Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁))ᵒᵖ (Type (max u₁ v₁)))
                  (obj (Functor.op yoneda) (op X))) ⟶
            (colimit (F ⋙ yoneda)).obj (obj (Functor.op yoneda) (op X)))
        (CategoryStruct.comp (Y :=
            colimit
              ((F ⋙ yoneda) ⋙
                obj (evaluation (Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁))ᵒᵖ (Type (max u₁ v₁)))
                  (obj (Functor.op yoneda) (op X))))
            (Iso.hom (colimitObjIsoColimitCompEvaluation (F ⋙ yoneda) (obj (Functor.op yoneda) (op X))) :
              (colimit (F ⋙ yoneda)).obj (obj (Functor.op yoneda) (op X)) ⟶
                colimit
                  ((F ⋙ yoneda) ⋙
                    obj (evaluation (Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁))ᵒᵖ (Type (max u₁ v₁)))
                      (obj (Functor.op yoneda) (op X))))
            (colimit.post F (obj coyoneda (op (obj yoneda X))) :
              colimit (F ⋙ obj coyoneda (op (obj yoneda X))) ⟶ obj (obj coyoneda (op (obj yoneda X))) (colimit F)) :
          (colimit (F ⋙ yoneda)).obj (obj (Functor.op yoneda) (op X)) ⟶
            (Functor.op yoneda ⋙ obj yoneda (colimit F)).obj (op X)) :
      colimit
          ((F ⋙ yoneda) ⋙
            obj (evaluation (Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁))ᵒᵖ (Type (max u₁ v₁)))
              (obj (Functor.op yoneda) (op X))) ⟶
        (Functor.op yoneda ⋙ obj yoneda (colimit F)).obj (op X))
rw₁ rw₂ :
  Eq (α := colimit (F ⋙ obj coyoneda (op (obj yoneda X))) ⟶ obj (obj coyoneda (op (obj yoneda X))) (colimit F))
    (colimit.post F (obj coyoneda (op (obj yoneda X)))) (colimit.post F (obj coyoneda (op (obj yoneda X))))
⊢ Eq (α := colimit (F ⋙ obj coyoneda (op (obj yoneda X))) ⟶ obj (obj coyoneda (op (obj yoneda X))) (colimit F))
    (colimit.post F (obj coyoneda (op (obj yoneda X))) :
      colimit (F ⋙ obj coyoneda (op (obj yoneda X))) ⟶ obj (obj coyoneda (op (obj yoneda X))) (colimit F))
    (CategoryStruct.comp (Y := (colimit (F ⋙ yoneda)).obj (obj (Functor.op yoneda) (op X)))
        (Iso.inv (colimitObjIsoColimitCompEvaluation (F ⋙ yoneda) (obj (Functor.op yoneda) (op X))) :
          colimit
              ((F ⋙ yoneda) ⋙
                obj (evaluation (Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁))ᵒᵖ (Type (max u₁ v₁)))
                  (obj (Functor.op yoneda) (op X))) ⟶
            (colimit (F ⋙ yoneda)).obj (obj (Functor.op yoneda) (op X)))
        (Iso.inv (Iso.app (yonedaYonedaColimit F) (op X)) :
          (Functor.op yoneda ⋙ colimit (F ⋙ yoneda)).obj (op X) ⟶
            (Functor.op yoneda ⋙ obj yoneda (colimit F)).obj (op X)) :
      colimit
          ((F ⋙ yoneda) ⋙
            obj (evaluation (Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁))ᵒᵖ (Type (max u₁ v₁)))
              (obj (Functor.op yoneda) (op X))) ⟶
        (Functor.op yoneda ⋙ obj yoneda (colimit F)).obj (op X))

Tactic:
rw [yonedaYonedaColimit_app_inv, Iso.inv_hom_id_assoc]

Premises used: CategoryTheory.Iso.inv_hom_id_assoc, CategoryTheory.yonedaYonedaColimit_app_inv