-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.Constructions (hypothesis)
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))
⊢ 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))
have 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))
Tactic: have eq2 : (m ≫ (A.prodFan B).snd) x = (BinaryFan.snd s) x :=
      ConcreteCategory.congr_hom (h ⟨WalkingPair.right⟩) x