∀ {A B C : CommRingCat} (f : A ⟶ C) (g : B ⟶ C) (s : CategoryTheory.Limits.PullbackCone f g)
  (m :
    s.pt ⟶
      {
        carrier :=
          ↥(((CommRingCat.Hom.hom f).comp (RingHom.fst ↑A ↑B)).eqLocus
              ((CommRingCat.Hom.hom g).comp (RingHom.snd ↑A ↑B))),
        commRing :=
          (((CommRingCat.Hom.hom f).comp (RingHom.fst ↑A ↑B)).eqLocus
              ((CommRingCat.Hom.hom g).comp (RingHom.snd ↑A ↑B))).toCommRing }),
  CategoryTheory.CategoryStruct.comp m
        (CommRingCat.ofHom
          ((RingHom.fst ↑A ↑B).comp
            (((CommRingCat.Hom.hom f).comp (RingHom.fst ↑A ↑B)).eqLocus
                ((CommRingCat.Hom.hom g).comp (RingHom.snd ↑A ↑B))).subtype)) =
      s.fst →
    CategoryTheory.CategoryStruct.comp m
          (CommRingCat.ofHom
            ((RingHom.snd ↑A ↑B).comp
              (((CommRingCat.Hom.hom f).comp (RingHom.fst ↑A ↑B)).eqLocus
                  ((CommRingCat.Hom.hom g).comp (RingHom.snd ↑A ↑B))).subtype)) =
        s.snd →
      m =
        CommRingCat.ofHom
          (((CommRingCat.Hom.hom s.fst).prod (CommRingCat.Hom.hom s.snd)).codRestrict
            (((CommRingCat.Hom.hom f).comp (RingHom.fst ↑A ↑B)).eqLocus
              ((CommRingCat.Hom.hom g).comp (RingHom.snd ↑A ↑B)))
            ⋯)