-- Module: Mathlib.Algebra.Category.Ring.EqualizerPushout
Goal:
R S : CommRingCat
f : R ⟶ S
hf : (Hom.hom f).FaithfullyFlat
algInst : Algebra (↑R : Type u) (↑S : Type u) := (Hom.hom f).toAlgebra
algebraizeInst : Module.FaithfullyFlat.{u, u} (↑R : Type u) (↑S : Type u)
fork : Fork (X := of (↑S : Type u)) (Y :=
  Cocone.pt (F :=
    span (X := of (↑R : Type u)) (Y := of (↑S : Type u)) (Z := of (↑S : Type u))
      (ofHom (algebraMap (↑R : Type u) (↑S : Type u))) (ofHom (algebraMap (↑R : Type u) (↑S : Type u))))
    (pushoutCocone (↑R : Type u) (↑S : Type u) (↑S : Type u)))
  (PushoutCocone.inl (pushoutCocone (↑R : Type u) (↑S : Type u) (↑S : Type u)))
  (PushoutCocone.inr (pushoutCocone (↑R : Type u) (↑S : Type u) (↑S : Type u))) :=
  Fork.ofι (ofHom (algebraMap (↑R : Type u) (↑S : Type u))) ⋯
isPushout : IsPushout.{u, u + 1} (Z := of (↑R : Type u)) (X := of (↑S : Type u)) (Y := of (↑S : Type u)) (P :=
  Cocone.pt (F :=
    span (X := of (↑R : Type u)) (Y := of (↑S : Type u)) (Z := of (↑S : Type u))
      (ofHom (algebraMap (↑R : Type u) (↑S : Type u))) (ofHom (algebraMap (↑R : Type u) (↑S : Type u))))
    (pushoutCocone (↑R : Type u) (↑S : Type u) (↑S : Type u)))
  (ofHom (algebraMap (↑R : Type u) (↑S : Type u))) (ofHom (algebraMap (↑R : Type u) (↑S : Type u)))
  (PushoutCocone.inl (pushoutCocone (↑R : Type u) (↑S : Type u) (↑S : Type u)))
  (PushoutCocone.inr (pushoutCocone (↑R : Type u) (↑S : Type u) (↑S : Type u))) :=
  ⋯
isLimit : IsLimit fork :=
  ((fork.isLimitEquivOfIsos
          (equalizerFork (PushoutCocone.inl (pushoutCocone (↑R : Type u) (↑S : Type u) (↑S : Type u)))
            (PushoutCocone.inr (pushoutCocone (↑R : Type u) (↑S : Type u) (↑S : Type u))))
          (Iso.refl (of (↑S : Type u)))
          (Iso.refl
            (Cocone.pt (F :=
              span (X := of (↑R : Type u)) (Y := of (↑S : Type u)) (Z := of (↑S : Type u))
                (ofHom (algebraMap (↑R : Type u) (↑S : Type u))) (ofHom (algebraMap (↑R : Type u) (↑S : Type u))))
              (pushoutCocone (↑R : Type u) (↑S : Type u) (↑S : Type u))))
          (RingEquiv.toCommRingCatIso
            (RingEquiv.ofBijective (Algebra.codRestrictEqLocusPushoutCocone (↑R : Type u) (↑S : Type u)) ⋯))
          ⋯ ⋯ ⋯).symm :
      (a :
          IsLimit
            (equalizerFork (pushoutCocone (↑R : Type u) (↑S : Type u) (↑S : Type u)).inl
              (pushoutCocone (↑R : Type u) (↑S : Type u) (↑S : Type u)).inr)) →
        IsLimit fork)
    (equalizerForkIsLimit (PushoutCocone.inl (pushoutCocone (↑R : Type u) (↑S : Type u) (↑S : Type u)))
      (PushoutCocone.inr (pushoutCocone (↑R : Type u) (↑S : Type u) (↑S : Type u))))
⊢ IsLimit (F := parallelPair (Y := pushout f f) (pushout.inl f f) (pushout.inr f f)) (Fork.ofι f ⋯)

Tactic:
exact Fork.isLimitEquivOfIsos fork (Fork.ofι f pushout.condition) (Iso.refl _)
    (IsPushout.isoPushout isPushout) (Iso.refl _) (IsPushout.inl_isoPushout_hom isPushout).symm
    (IsPushout.inr_isoPushout_hom isPushout).symm rfl isLimit

Premises used: CategoryTheory.Limits.Fork.ofι, CategoryTheory.IsPushout.isoPushout, CategoryTheory.Limits.pushout.condition, CategoryTheory.Iso.refl, CategoryTheory.IsPushout.inl_isoPushout_hom, CategoryTheory.Limits.Fork.isLimitEquivOfIsos, Eq.symm, CategoryTheory.IsPushout.inr_isoPushout_hom, DFunLike.coe, rfl