-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Constructions (goal)
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 s.fst : (a : (↑s.pt : Type u)) → (↑A : Type u)) x,
        (Hom.hom s.snd : (a : (↑s.pt : Type u)) → (↑B : Type u)) x) :
      (↑A : Type u) × (↑B : Type u))
have uniq : 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: rw [← eq1, ← eq2]