-- Module: Mathlib.Algebra.Category.Ring.Constructions
Goal:
A B C : CommRingCat
f : A ⟶ C
g : B ⟶ C
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))))
e₁ :
  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
e₂ :
  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
x : (↑s.pt : Type u)
eq1 :
  Eq (α := (↑A : Type u))
    ((Hom.hom
            (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))))))) :
          (a : (↑s.pt : Type u)) → (↑A : Type u))
        x :
      (↑A : Type u))
    ((Hom.hom s.fst : (a : (↑s.pt : Type u)) → (↑A : Type u)) x : (↑A : Type u))
eq2 :
  Eq (α := (↑B : Type u))
    ((Hom.hom
            (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))))))) :
          (a : (↑s.pt : Type u)) → (↑B : Type u))
        x :
      (↑B : Type u))
    ((Hom.hom s.snd : (a : (↑s.pt : Type u)) → (↑B : Type u)) x : (↑B : Type u))
⊢ Eq (α := (↑A : Type u) × (↑B : Type u))
    ((↑((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier) m :
              (a : (↑s.pt : Type u)) →
                (↑(of
                      ↥(((Hom.hom f).comp (RingHom.fst (↑A : Type u) (↑B : Type u))).eqLocus
                          ((Hom.hom g).comp (RingHom.snd (↑A : Type u) (↑B : Type u))))) :
                  Type u))
            x) :
        (↑A : Type u) × (↑B : Type u)) :
      (↑A : Type u) × (↑B : Type u))
    (((Hom.hom
              (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))))))) :
            (a : (↑s.pt : Type u)) → (↑A : Type u))
          x,
        (Hom.hom
              (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))))))) :
            (a : (↑s.pt : Type u)) → (↑B : Type u))
          x) :
      (↑A : Type u) × (↑B : Type u))

Tactic:
rfl