-- Module: Mathlib.Algebra.Category.Ring.Constructions
Goal:
A B : CommRingCat
s : Cone (pair A B)
m : s.pt ⟶ (A.prodFan B).pt
h : ∀ (j : Discrete WalkingPair), m ≫ (A.prodFan B).π.app j = s.π.app j
x : (↑s.pt : Type u)
eq1 :
  Eq (α := (↑(Functor.obj (pair A B) { as := WalkingPair.left : Discrete WalkingPair }) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier)
            (m ≫ (A.prodFan B).fst) :
          (a : (↑s.pt : Type u)) → (↑((pair A B).obj { as := WalkingPair.left }) : Type u))
        x :
      (↑(Functor.obj (pair A B) { as := WalkingPair.left : Discrete WalkingPair }) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier)
            (BinaryFan.fst s) :
          (a : (↑(((Functor.const (Discrete WalkingPair)).obj s.pt).obj { as := WalkingPair.left }) : Type u)) →
            (↑((pair A B).obj { as := WalkingPair.left }) : Type u))
        x :
      (↑(Functor.obj (pair A B) { as := WalkingPair.left : Discrete WalkingPair }) : Type u))
eq2 :
  Eq (α := (↑(Functor.obj (pair A B) { as := WalkingPair.right : Discrete WalkingPair }) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier)
            (m ≫ (A.prodFan B).snd) :
          (a : (↑s.pt : Type u)) → (↑((pair A B).obj { as := WalkingPair.right }) : Type u))
        x :
      (↑(Functor.obj (pair A B) { as := WalkingPair.right : Discrete WalkingPair }) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier)
            (BinaryFan.snd s) :
          (a : (↑(((Functor.const (Discrete WalkingPair)).obj s.pt).obj { as := WalkingPair.right }) : Type u)) →
            (↑((pair A B).obj { as := WalkingPair.right }) : Type u))
        x :
      (↑(Functor.obj (pair A B) { as := WalkingPair.right : Discrete WalkingPair }) : Type u))
hf :
  Eq (α := (↑(A.prodFan B).pt : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier) m :
          (a : (↑s.pt : Type u)) → (↑(A.prodFan B).pt : Type u))
        x :
      (↑(A.prodFan B).pt : Type u))
    (((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier)
              (m ≫ (A.prodFan B).fst) :
            (a : (↑s.pt : Type u)) → (↑((pair A B).obj { as := WalkingPair.left }) : Type u))
          x,
        (ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier)
              (m ≫ (A.prodFan B).snd) :
            (a : (↑s.pt : Type u)) → (↑((pair A B).obj { as := WalkingPair.right }) : Type u))
          x) :
      (↑(Functor.obj (pair A B) { as := WalkingPair.left : Discrete WalkingPair }) : Type u) ×
        (↑(Functor.obj (pair A B) { as := WalkingPair.right : Discrete WalkingPair }) : Type u))
⊢ Eq (α := (↑(A.prodFan B).pt : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier) m :
          (a : (↑s.pt : Type u)) → (↑(A.prodFan B).pt : Type u))
        x :
      (↑(A.prodFan B).pt : Type u))
    (((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier)
              (BinaryFan.fst s) :
            (a : (↑(((Functor.const (Discrete WalkingPair)).obj s.pt).obj { as := WalkingPair.left }) : Type u)) →
              (↑((pair A B).obj { as := WalkingPair.left }) : Type u))
          x,
        (ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier)
              (BinaryFan.snd s) :
            (a : (↑(((Functor.const (Discrete WalkingPair)).obj s.pt).obj { as := WalkingPair.right }) : Type u)) →
              (↑((pair A B).obj { as := WalkingPair.right }) : Type u))
          x) :
      (↑(Functor.obj (pair A B) { as := WalkingPair.left : Discrete WalkingPair }) : Type u) ×
        (↑(Functor.obj (pair A B) { as := WalkingPair.right : Discrete WalkingPair }) : Type u))

Tactic:
rw [← eq1, ← eq2]