-- Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
Goal:
C : Type u
inst : Category.{v, u} C
J : Type u₁
inst_1 : Category.{v₁, u₁} J
K : Type u₂
inst_2 : Category.{v₂, u₂} K
inst_3 : HasColimitsOfShape.{v₁, u₁, v, u} J C
F : J ⥤ Functor.{v₂, v, u₂, u} K C
i j : K
f : i ⟶ j
rw :
  Eq (α := colimit (F ⋙ obj (evaluation K C) i) ⟶ colimit (F ⋙ obj (evaluation K C) j))
    (CategoryStruct.comp (Y := (colimit F).obj i)
        (Iso.inv (colimitObjIsoColimitCompEvaluation F i) : colimit (F ⋙ obj (evaluation K C) i) ⟶ (colimit F).obj i)
        ((colimit F).map f ≫ Iso.hom (colimitObjIsoColimitCompEvaluation F j) :
          (colimit F).obj i ⟶ colimit (F ⋙ obj (evaluation K C) j)) :
      colimit (F ⋙ obj (evaluation K C) i) ⟶ colimit (F ⋙ obj (evaluation K C) j))
    (colimMap (F.whiskerLeft (map (evaluation K C) f)) :
      colimit (F ⋙ obj (evaluation K C) i) ⟶ colimit (F ⋙ obj (evaluation K C) j))
rw₁ :
  Eq (α := colimit (F ⋙ obj (evaluation K C) i) ⟶ colimit (F ⋙ obj (evaluation K C) j))
    ((Iso.inv (colimitObjIsoColimitCompEvaluation F i) ≫ (colimit F).map f) ≫
        Iso.hom (colimitObjIsoColimitCompEvaluation F j) :
      colimit (F ⋙ obj (evaluation K C) i) ⟶ colimit (F ⋙ obj (evaluation K C) j))
    (colimMap (F.whiskerLeft (map (evaluation K C) f)) :
      colimit (F ⋙ obj (evaluation K C) i) ⟶ colimit (F ⋙ obj (evaluation K C) j))
rw₂ :
  Eq (α := colimit (F ⋙ obj (evaluation K C) i) ⟶ (colimit F).obj j)
    (Iso.inv (colimitObjIsoColimitCompEvaluation F i) ≫ (colimit F).map f :
      colimit (F ⋙ obj (evaluation K C) i) ⟶ (colimit F).obj j)
    (CategoryStruct.comp (Y := colimit (F ⋙ obj (evaluation K C) j))
        (colimMap (F.whiskerLeft (map (evaluation K C) f)) :
          colimit (F ⋙ obj (evaluation K C) i) ⟶ colimit (F ⋙ obj (evaluation K C) j))
        (Iso.inv (colimitObjIsoColimitCompEvaluation F j) : colimit (F ⋙ obj (evaluation K C) j) ⟶ (colimit F).obj j) :
      colimit (F ⋙ obj (evaluation K C) i) ⟶ (colimit F).obj j)
rw₃ rw₄ :
  Eq (α := colimit (F ⋙ obj (evaluation K C) i) ⟶ (colimit F).obj j)
    (CategoryStruct.comp (Y := colimit (F ⋙ obj (evaluation K C) j))
        (colimMap (F.whiskerLeft (map (evaluation K C) f)) :
          colimit (F ⋙ obj (evaluation K C) i) ⟶ colimit (F ⋙ obj (evaluation K C) j))
        (Iso.inv (colimitObjIsoColimitCompEvaluation F j) : colimit (F ⋙ obj (evaluation K C) j) ⟶ (colimit F).obj j) :
      colimit (F ⋙ obj (evaluation K C) i) ⟶ (colimit F).obj j)
    (CategoryStruct.comp (Y := colimit (F ⋙ obj (evaluation K C) j))
        (colimMap (F.whiskerLeft (map (evaluation K C) f)) :
          colimit (F ⋙ obj (evaluation K C) i) ⟶ colimit (F ⋙ obj (evaluation K C) j))
        (Iso.inv (colimitObjIsoColimitCompEvaluation F j) : colimit (F ⋙ obj (evaluation K C) j) ⟶ (colimit F).obj j) :
      colimit (F ⋙ obj (evaluation K C) i) ⟶ (colimit F).obj j)
⊢ Eq (α := (colimit F).obj i ⟶ colimit (F ⋙ obj (evaluation K C) j))
    ((colimit F).map f ≫ Iso.hom (colimitObjIsoColimitCompEvaluation F j) :
      (colimit F).obj i ⟶ colimit (F ⋙ obj (evaluation K C) j))
    (CategoryStruct.comp (Y := colimit (F ⋙ obj (evaluation K C) i))
        (Iso.hom (colimitObjIsoColimitCompEvaluation F i) : (colimit F).obj i ⟶ colimit (F ⋙ obj (evaluation K C) i))
        (colimMap (F.whiskerLeft (map (evaluation K C) f)) :
          colimit (F ⋙ obj (evaluation K C) i) ⟶ colimit (F ⋙ obj (evaluation K C) j)) :
      (colimit F).obj i ⟶ colimit (F ⋙ obj (evaluation K C) j))

Tactic:
rw [← Iso.inv_comp_eq, ← Category.assoc, ← Iso.eq_comp_inv,
    colimitObjIsoColimitCompEvaluation_inv_colimit_map]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.eq_comp_inv, CategoryTheory.Limits.colimitObjIsoColimitCompEvaluation_inv_colimit_map, CategoryTheory.Iso.inv_comp_eq