-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Constructions (goal)
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)
⊢ 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)))
have 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)))
Tactic: change IsLocalHom ((lim.map _ ≫ _ ≫ (equalizerFork _ _).ι) ≫ _).hom