-- Mathlib/Algebra/Category/Ring/Constructions.lean
theorem equalizer_ι_isLocalHom (F : WalkingParallelPair ⥤ CommRingCat.{u}) :
    IsLocalHom (limit.π F WalkingParallelPair.zero).hom

Proof state:
F : WalkingParallelPair ⥤ CommRingCat
this :
  limMap (diagramIsoParallelPair F).hom ≫
      limit.π (parallelPair (F.map WalkingParallelPairHom.left) (F.map WalkingParallelPairHom.right))
        WalkingParallelPair.zero =
    limit.π F WalkingParallelPair.zero ≫ (diagramIsoParallelPair F).hom.app WalkingParallelPair.zero
⊢ IsLocalHom (Hom.hom (limit.π F WalkingParallelPair.zero))

Tactic:
rw [← IsIso.comp_inv_eq] at this

Result:
F : WalkingParallelPair ⥤ CommRingCat
this :
  (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 (Hom.hom (limit.π F WalkingParallelPair.zero))

Proof state:
F : WalkingParallelPair ⥤ CommRingCat
this :
  (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 (Hom.hom (limit.π F WalkingParallelPair.zero))

Tactic:
rw [← this]

Result:
F : WalkingParallelPair ⥤ CommRingCat
this :
  (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
    (Hom.hom
      ((limMap (diagramIsoParallelPair F).hom ≫
          limit.π (parallelPair (F.map WalkingParallelPairHom.left) (F.map WalkingParallelPairHom.right))
            WalkingParallelPair.zero) ≫
        inv ((diagramIsoParallelPair F).hom.app WalkingParallelPair.zero)))

Proof state:
F : WalkingParallelPair ⥤ CommRingCat
this :
  (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
    (Hom.hom
      ((lim.map (diagramIsoParallelPair F).hom ≫
          (limit.isoLimitCone
                { cone := equalizerFork (F.map WalkingParallelPairHom.left) (F.map WalkingParallelPairHom.right),
                  isLimit :=
                    equalizerForkIsLimit (F.map WalkingParallelPairHom.left)
                      (F.map WalkingParallelPairHom.right) }).hom ≫
            (equalizerFork (F.map WalkingParallelPairHom.left) (F.map WalkingParallelPairHom.right)).ι) ≫
        inv ((diagramIsoParallelPair F).hom.app WalkingParallelPair.zero)))

Tactic:
infer_instance

Result:
no goals

Proof state:
F : WalkingParallelPair ⥤ CommRingCat
this :
  (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
    (Hom.hom
      ((limMap (diagramIsoParallelPair F).hom ≫
          limit.π (parallelPair (F.map WalkingParallelPairHom.left) (F.map WalkingParallelPairHom.right))
            WalkingParallelPair.zero) ≫
        inv ((diagramIsoParallelPair F).hom.app WalkingParallelPair.zero)))

Tactic:
rw [← limit.isoLimitCone_hom_π
    ⟨_,
      equalizerForkIsLimit (F.map WalkingParallelPairHom.left)
        (F.map WalkingParallelPairHom.right)⟩
    WalkingParallelPair.zero]

Result:
F : WalkingParallelPair ⥤ CommRingCat
this :
  (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
    (Hom.hom
      ((limMap (diagramIsoParallelPair F).hom ≫
          (limit.isoLimitCone
                { cone := equalizerFork (F.map WalkingParallelPairHom.left) (F.map WalkingParallelPairHom.right),
                  isLimit :=
                    equalizerForkIsLimit (F.map WalkingParallelPairHom.left)
                      (F.map WalkingParallelPairHom.right) }).hom ≫
            { cone := equalizerFork (F.map WalkingParallelPairHom.left) (F.map WalkingParallelPairHom.right),
                      isLimit :=
                        equalizerForkIsLimit (F.map WalkingParallelPairHom.left)
                          (F.map WalkingParallelPairHom.right) }.cone.π.app
              WalkingParallelPair.zero) ≫
        inv ((diagramIsoParallelPair F).hom.app WalkingParallelPair.zero)))

Proof state:
F : WalkingParallelPair ⥤ CommRingCat
⊢ IsLocalHom (Hom.hom (limit.π F WalkingParallelPair.zero))

Tactic:
have := limMap_π (diagramIsoParallelPair F).hom WalkingParallelPair.zero

Result:
F : WalkingParallelPair ⥤ CommRingCat
this :
  limMap (diagramIsoParallelPair F).hom ≫
      limit.π (parallelPair (F.map WalkingParallelPairHom.left) (F.map WalkingParallelPairHom.right))
        WalkingParallelPair.zero =
    limit.π F WalkingParallelPair.zero ≫ (diagramIsoParallelPair F).hom.app WalkingParallelPair.zero
⊢ IsLocalHom (Hom.hom (limit.π F WalkingParallelPair.zero))

Proof state:
F : WalkingParallelPair ⥤ CommRingCat
this :
  (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
    (Hom.hom
      ((limMap (diagramIsoParallelPair F).hom ≫
          (limit.isoLimitCone
                { cone := equalizerFork (F.map WalkingParallelPairHom.left) (F.map WalkingParallelPairHom.right),
                  isLimit :=
                    equalizerForkIsLimit (F.map WalkingParallelPairHom.left)
                      (F.map WalkingParallelPairHom.right) }).hom ≫
            { cone := equalizerFork (F.map WalkingParallelPairHom.left) (F.map WalkingParallelPairHom.right),
                      isLimit :=
                        equalizerForkIsLimit (F.map WalkingParallelPairHom.left)
                          (F.map WalkingParallelPairHom.right) }.cone.π.app
              WalkingParallelPair.zero) ≫
        inv ((diagramIsoParallelPair F).hom.app WalkingParallelPair.zero)))

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

Result:
F : WalkingParallelPair ⥤ CommRingCat
this :
  (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
    (Hom.hom
      ((lim.map (diagramIsoParallelPair F).hom ≫
          (limit.isoLimitCone
                { cone := equalizerFork (F.map WalkingParallelPairHom.left) (F.map WalkingParallelPairHom.right),
                  isLimit :=
                    equalizerForkIsLimit (F.map WalkingParallelPairHom.left)
                      (F.map WalkingParallelPairHom.right) }).hom ≫
            (equalizerFork (F.map WalkingParallelPairHom.left) (F.map WalkingParallelPairHom.right)).ι) ≫
        inv ((diagramIsoParallelPair F).hom.app WalkingParallelPair.zero)))