-- Module: Mathlib.Algebra.Category.Ring.Constructions
Goal:
A B C : CommRingCat
f : A ⟶ C
g : B ⟶ C
lift :
  (s : PullbackCone f g) →
    s.pt ⟶
      of
        ↥(RingHom.eqLocus ((Hom.hom f).comp (RingHom.fst (↑A : Type u) (↑B : Type u)))
            ((Hom.hom g).comp (RingHom.snd (↑A : Type u) (↑B : Type u))))
fac_left :
  ∀ (s : PullbackCone f g),
    CategoryStruct.comp (Y :=
        of
          ↥(RingHom.eqLocus ((Hom.hom f).comp (RingHom.fst (↑A : Type u) (↑B : Type u)))
              ((Hom.hom g).comp (RingHom.snd (↑A : Type u) (↑B : Type u)))))
        (ofHom
          (((Hom.hom s.fst).prod (Hom.hom s.snd)).codRestrict
            (RingHom.eqLocus ((Hom.hom f).comp (RingHom.fst (↑A : Type u) (↑B : Type u)))
              ((Hom.hom g).comp (RingHom.snd (↑A : Type u) (↑B : Type u))))
            ⋯))
        (ofHom
          (RingHom.comp (RingHom.fst (↑A : Type u) (↑B : Type u))
            (Subring.subtype
              (RingHom.eqLocus ((Hom.hom f).comp (RingHom.fst (↑A : Type u) (↑B : Type u)))
                ((Hom.hom g).comp (RingHom.snd (↑A : Type u) (↑B : Type u))))))) =
      s.fst
fac_right :
  ∀ (s : PullbackCone f g),
    CategoryStruct.comp (Y :=
        of
          ↥(RingHom.eqLocus ((Hom.hom f).comp (RingHom.fst (↑A : Type u) (↑B : Type u)))
              ((Hom.hom g).comp (RingHom.snd (↑A : Type u) (↑B : Type u)))))
        (ofHom
          (((Hom.hom s.fst).prod (Hom.hom s.snd)).codRestrict
            (RingHom.eqLocus ((Hom.hom f).comp (RingHom.fst (↑A : Type u) (↑B : Type u)))
              ((Hom.hom g).comp (RingHom.snd (↑A : Type u) (↑B : Type u))))
            ⋯))
        (ofHom
          (RingHom.comp (RingHom.snd (↑A : Type u) (↑B : Type u))
            (Subring.subtype
              (RingHom.eqLocus ((Hom.hom f).comp (RingHom.fst (↑A : Type u) (↑B : Type u)))
                ((Hom.hom g).comp (RingHom.snd (↑A : Type u) (↑B : Type u))))))) =
      s.snd
uniq :
  ∀ (s : PullbackCone f g)
    (m :
      s.pt ⟶
        of
          ↥(RingHom.eqLocus ((Hom.hom f).comp (RingHom.fst (↑A : Type u) (↑B : Type u)))
              ((Hom.hom g).comp (RingHom.snd (↑A : Type u) (↑B : Type u))))),
    m ≫
          ofHom
            (RingHom.comp (RingHom.fst (↑A : Type u) (↑B : Type u))
              (Subring.subtype
                (RingHom.eqLocus ((Hom.hom f).comp (RingHom.fst (↑A : Type u) (↑B : Type u)))
                  ((Hom.hom g).comp (RingHom.snd (↑A : Type u) (↑B : Type u)))))) =
        s.fst →
      m ≫
            ofHom
              (RingHom.comp (RingHom.snd (↑A : Type u) (↑B : Type u))
                (Subring.subtype
                  (RingHom.eqLocus ((Hom.hom f).comp (RingHom.fst (↑A : Type u) (↑B : Type u)))
                    ((Hom.hom g).comp (RingHom.snd (↑A : Type u) (↑B : Type u)))))) =
          s.snd →
        m =
          ofHom
            (((Hom.hom s.fst).prod (Hom.hom s.snd)).codRestrict
              (RingHom.eqLocus ((Hom.hom f).comp (RingHom.fst (↑A : Type u) (↑B : Type u)))
                ((Hom.hom g).comp (RingHom.snd (↑A : Type u) (↑B : Type u))))
              ⋯)
⊢ IsLimit (pullbackCone f g)

Tactic:
fapply PullbackCone.IsLimit.mk

Premises used: CategoryTheory.Limits.PullbackCone.IsLimit.mk