-- 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 : HasLimitsOfShape.{v₁, u₁, v, u} J C
i j : K
F : J ⥤ Functor.{v₂, v, u₂, u} K C
f : i ⟶ j
rw :
  (limit F).map f =
    CategoryStruct.comp (Y := limit (F ⋙ obj (evaluation K C) i))
      (Iso.hom (limitObjIsoLimitCompEvaluation F i) : (limit F).obj i ⟶ limit (F ⋙ obj (evaluation K C) i))
      (CategoryStruct.comp (Y := limit (F ⋙ obj (evaluation K C) j))
          (limMap (F.whiskerLeft (map (evaluation K C) f)) :
            limit (F ⋙ obj (evaluation K C) i) ⟶ limit (F ⋙ obj (evaluation K C) j))
          (Iso.inv (limitObjIsoLimitCompEvaluation F j) : limit (F ⋙ obj (evaluation K C) j) ⟶ (limit F).obj j) :
        limit (F ⋙ obj (evaluation K C) i) ⟶ (limit F).obj j)
rw₁ :
  (limit F).map f =
    CategoryStruct.comp (Y := limit (F ⋙ obj (evaluation K C) j))
      (CategoryStruct.comp (Y := limit (F ⋙ obj (evaluation K C) i))
          (Iso.hom (limitObjIsoLimitCompEvaluation F i) : (limit F).obj i ⟶ limit (F ⋙ obj (evaluation K C) i))
          (limMap (F.whiskerLeft (map (evaluation K C) f)) :
            limit (F ⋙ obj (evaluation K C) i) ⟶ limit (F ⋙ obj (evaluation K C) j)) :
        (limit F).obj i ⟶ limit (F ⋙ obj (evaluation K C) j))
      (Iso.inv (limitObjIsoLimitCompEvaluation F j) : limit (F ⋙ obj (evaluation K C) j) ⟶ (limit F).obj j)
rw₂ :
  Eq (α := (limit F).obj i ⟶ limit (F ⋙ obj (evaluation K C) j))
    ((limit F).map f ≫ Iso.hom (limitObjIsoLimitCompEvaluation F j) :
      (limit F).obj i ⟶ limit (F ⋙ obj (evaluation K C) j))
    (CategoryStruct.comp (Y := limit (F ⋙ obj (evaluation K C) i))
        (Iso.hom (limitObjIsoLimitCompEvaluation F i) : (limit F).obj i ⟶ limit (F ⋙ obj (evaluation K C) i))
        (limMap (F.whiskerLeft (map (evaluation K C) f)) :
          limit (F ⋙ obj (evaluation K C) i) ⟶ limit (F ⋙ obj (evaluation K C) j)) :
      (limit F).obj i ⟶ limit (F ⋙ obj (evaluation K C) j))
rw₃ rw₄ :
  Eq (α := (limit F).obj i ⟶ limit (F ⋙ obj (evaluation K C) j))
    (CategoryStruct.comp (Y := limit (F ⋙ obj (evaluation K C) i))
        (Iso.hom (limitObjIsoLimitCompEvaluation F i) : (limit F).obj i ⟶ limit (F ⋙ obj (evaluation K C) i))
        (limMap (F.whiskerLeft (map (evaluation K C) f)) :
          limit (F ⋙ obj (evaluation K C) i) ⟶ limit (F ⋙ obj (evaluation K C) j)) :
      (limit F).obj i ⟶ limit (F ⋙ obj (evaluation K C) j))
    (CategoryStruct.comp (Y := limit (F ⋙ obj (evaluation K C) i))
        (Iso.hom (limitObjIsoLimitCompEvaluation F i) : (limit F).obj i ⟶ limit (F ⋙ obj (evaluation K C) i))
        (limMap (F.whiskerLeft (map (evaluation K C) f)) :
          limit (F ⋙ obj (evaluation K C) i) ⟶ limit (F ⋙ obj (evaluation K C) j)) :
      (limit F).obj i ⟶ limit (F ⋙ obj (evaluation K C) j))
⊢ Eq (α := limit (F ⋙ obj (evaluation K C) i) ⟶ (limit F).obj j)
    (Iso.inv (limitObjIsoLimitCompEvaluation F i) ≫ (limit F).map f :
      limit (F ⋙ obj (evaluation K C) i) ⟶ (limit F).obj j)
    (CategoryStruct.comp (Y := limit (F ⋙ obj (evaluation K C) j))
        (limMap (F.whiskerLeft (map (evaluation K C) f)) :
          limit (F ⋙ obj (evaluation K C) i) ⟶ limit (F ⋙ obj (evaluation K C) j))
        (Iso.inv (limitObjIsoLimitCompEvaluation F j) : limit (F ⋙ obj (evaluation K C) j) ⟶ (limit F).obj j) :
      limit (F ⋙ obj (evaluation K C) i) ⟶ (limit F).obj j)

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

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