-- Module: Mathlib.Algebra.Category.Ring.Constructions
Goal:
F : WalkingParallelPair ⥤ CommRingCat
this :
  Eq (α := limit F ⟶ F.obj WalkingParallelPair.zero)
    (CategoryStruct.comp (Y :=
        limit (parallelPair (F.map WalkingParallelPairHom.left) (F.map WalkingParallelPairHom.right)))
        (limMap (diagramIsoParallelPair F).hom)
        (limit.π (parallelPair (F.map WalkingParallelPairHom.left) (F.map WalkingParallelPairHom.right))
          WalkingParallelPair.zero) ≫
      inv ((diagramIsoParallelPair F).hom.app WalkingParallelPair.zero))
    (limit.π F WalkingParallelPair.zero)
change :
  IsLocalHom (R := (↑(Functor.obj lim F) : Type u)) (S := (↑(F.obj WalkingParallelPair.zero) : Type u)) (F :=
    (↑(Functor.obj lim F) : Type u) →+* (↑(F.obj WalkingParallelPair.zero) : Type u))
    (Hom.hom
      ((CategoryTheory.Functor.map lim (diagramIsoParallelPair F).hom ≫
          CategoryStruct.comp (Y :=
            Cone.pt (F := parallelPair (F.map WalkingParallelPairHom.left) (F.map WalkingParallelPairHom.right))
              (equalizerFork (F.map WalkingParallelPairHom.left) (F.map WalkingParallelPairHom.right)))
            (Iso.hom
                (limit.isoLimitCone
                  { cone := equalizerFork (F.map WalkingParallelPairHom.left) (F.map WalkingParallelPairHom.right),
                    isLimit :=
                      equalizerForkIsLimit (F.map WalkingParallelPairHom.left) (F.map WalkingParallelPairHom.right) }) :
              limit (parallelPair (F.map WalkingParallelPairHom.left) (F.map WalkingParallelPairHom.right)) ⟶
                Cone.pt (F := parallelPair (F.map WalkingParallelPairHom.left) (F.map WalkingParallelPairHom.right))
                  (LimitCone.cone
                    { cone := equalizerFork (F.map WalkingParallelPairHom.left) (F.map WalkingParallelPairHom.right),
                      isLimit :=
                        equalizerForkIsLimit (F.map WalkingParallelPairHom.left)
                          (F.map WalkingParallelPairHom.right) }))
            (Fork.ι (equalizerFork (F.map WalkingParallelPairHom.left) (F.map WalkingParallelPairHom.right)))) ≫
        inv ((diagramIsoParallelPair F).hom.app WalkingParallelPair.zero)))
⊢ IsLocalHom (R := (↑(limit F) : Type u)) (S := (↑(F.obj WalkingParallelPair.zero) : Type u)) (F :=
    (↑(limit F) : Type u) →+* (↑(F.obj WalkingParallelPair.zero) : Type u))
    (Hom.hom
      (CategoryStruct.comp (Y :=
          limit (parallelPair (F.map WalkingParallelPairHom.left) (F.map WalkingParallelPairHom.right)))
          (limMap (diagramIsoParallelPair F).hom)
          (CategoryStruct.comp (Y :=
            Cone.pt (F := parallelPair (F.map WalkingParallelPairHom.left) (F.map WalkingParallelPairHom.right))
              (LimitCone.cone
                { cone := equalizerFork (F.map WalkingParallelPairHom.left) (F.map WalkingParallelPairHom.right),
                  isLimit :=
                    equalizerForkIsLimit (F.map WalkingParallelPairHom.left) (F.map WalkingParallelPairHom.right) }))
            (Iso.hom
              (limit.isoLimitCone
                { cone := equalizerFork (F.map WalkingParallelPairHom.left) (F.map WalkingParallelPairHom.right),
                  isLimit :=
                    equalizerForkIsLimit (F.map WalkingParallelPairHom.left) (F.map WalkingParallelPairHom.right) }))
            (NatTrans.app
              (Cone.π
                (LimitCone.cone
                  { cone := equalizerFork (F.map WalkingParallelPairHom.left) (F.map WalkingParallelPairHom.right),
                    isLimit :=
                      equalizerForkIsLimit (F.map WalkingParallelPairHom.left) (F.map WalkingParallelPairHom.right) }))
              WalkingParallelPair.zero)) ≫
        inv ((diagramIsoParallelPair F).hom.app WalkingParallelPair.zero)))

Tactic:
change IsLocalHom ((lim.map _ ≫ _ ≫ (equalizerFork _ _).ι) ≫ _).hom

Premises used: CommRingCat.Hom.hom, CategoryTheory.Limits.lim, CategoryTheory.Functor.map, CategoryTheory.Limits.Fork.ι, CategoryTheory.CategoryStruct.comp, IsLocalHom, CommRingCat.equalizerFork