-- Module: Mathlib.Algebra.Category.Ring.Constructions
Goal:
A B C : CommRingCat
f : A ⟶ C
g : B ⟶ C
hf :
  ∀ (x : (↑A : Type u) × (↑B : Type u))
    (e :
      Membership.mem (γ := Subring ((↑A : Type u) × (↑B : Type u)))
        (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))))
        x),
    Eq (α := (↑C : Type u))
      ((Hom.hom
              (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)))))) ≫
                f) :
            (a :
                (↑(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)) →
              (↑C : Type u))
          (Subtype.mk (p := fun (x : (↑A : Type u) × (↑B : Type u)) ↦
            Membership.mem (γ := Subring ((↑A : Type u) × (↑B : Type u)))
              (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))))
              x)
            x e) :
        (↑C : Type u))
      ((Hom.hom
              (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)))))) ≫
                g) :
            (a :
                (↑(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)) →
              (↑C : Type u))
          (Subtype.mk (p := fun (x : (↑A : Type u) × (↑B : Type u)) ↦
            Membership.mem (γ := Subring ((↑A : Type u) × (↑B : Type u)))
              (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))))
              x)
            x e) :
        (↑C : Type u))
⊢ Eq (α :=
    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)))) ⟶
      C)
    (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)))))) ≫
      f)
    (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)))))) ≫
      g)

Tactic:
ext ⟨x, e⟩