-- Module: Mathlib.CategoryTheory.Limits.Types.Products
Goal:
X Y : Type u
x : X ⟶ Y
x_1 : Type u
refine_2 :
  Eq (α := (binaryProductFunctor.obj X).obj x_1 ⟶ Y)
    (CategoryStruct.comp (Y := Y ⨯ x_1)
      (NatTrans.app
          (binaryProductFunctor.map x ≫
            Iso.hom
              ((fun (X : Type u) ↦
                  (NatIso.ofComponents
                      (fun (Y : Type u) ↦
                        Iso.symm (IsLimit.conePointUniqueUpToIso (limit.isLimit (pair X Y)) (binaryProductLimit X Y)))
                      ⋯ :
                    binaryProductFunctor.obj X ≅ Functor.obj prod.functor X))
                Y))
          x_1 :
        (binaryProductFunctor.obj X).obj x_1 ⟶ Functor.obj (Functor.obj prod.functor Y) x_1)
      prod.fst)
    (CategoryStruct.comp (Y := Y ⨯ x_1)
      (NatTrans.app
          (Iso.hom
              ((fun (X : Type u) ↦
                  (NatIso.ofComponents
                      (fun (Y : Type u) ↦
                        Iso.symm (IsLimit.conePointUniqueUpToIso (limit.isLimit (pair X Y)) (binaryProductLimit X Y)))
                      ⋯ :
                    binaryProductFunctor.obj X ≅ Functor.obj prod.functor X))
                X) ≫
            Functor.map prod.functor x)
          x_1 :
        (binaryProductFunctor.obj X).obj x_1 ⟶ Functor.obj (Functor.obj prod.functor Y) x_1)
      prod.fst)
refine_2₁ :
  Eq (α := (binaryProductFunctor.obj X).obj x_1 ⟶ x_1)
    (CategoryStruct.comp (Y := Y ⨯ x_1)
      (NatTrans.app
          (binaryProductFunctor.map x ≫
            Iso.hom
              ((fun (X : Type u) ↦
                  (NatIso.ofComponents
                      (fun (Y : Type u) ↦
                        Iso.symm (IsLimit.conePointUniqueUpToIso (limit.isLimit (pair X Y)) (binaryProductLimit X Y)))
                      ⋯ :
                    binaryProductFunctor.obj X ≅ Functor.obj prod.functor X))
                Y))
          x_1 :
        (binaryProductFunctor.obj X).obj x_1 ⟶ Functor.obj (Functor.obj prod.functor Y) x_1)
      prod.snd)
    (CategoryStruct.comp (Y := Y ⨯ x_1)
      (NatTrans.app
          (Iso.hom
              ((fun (X : Type u) ↦
                  (NatIso.ofComponents
                      (fun (Y : Type u) ↦
                        Iso.symm (IsLimit.conePointUniqueUpToIso (limit.isLimit (pair X Y)) (binaryProductLimit X Y)))
                      ⋯ :
                    binaryProductFunctor.obj X ≅ Functor.obj prod.functor X))
                X) ≫
            Functor.map prod.functor x)
          x_1 :
        (binaryProductFunctor.obj X).obj x_1 ⟶ Functor.obj (Functor.obj prod.functor Y) x_1)
      prod.snd)
⊢ Eq (α := (binaryProductFunctor.obj X).obj x_1 ⟶ Functor.obj (Functor.obj prod.functor Y) x_1)
    (NatTrans.app
      (binaryProductFunctor.map x ≫
        Iso.hom
          ((fun (X : Type u) ↦
              (NatIso.ofComponents
                  (fun (Y : Type u) ↦
                    Iso.symm (IsLimit.conePointUniqueUpToIso (limit.isLimit (pair X Y)) (binaryProductLimit X Y)))
                  ⋯ :
                binaryProductFunctor.obj X ≅ Functor.obj prod.functor X))
            Y))
      x_1)
    (NatTrans.app
      (Iso.hom
          ((fun (X : Type u) ↦
              (NatIso.ofComponents
                  (fun (Y : Type u) ↦
                    Iso.symm (IsLimit.conePointUniqueUpToIso (limit.isLimit (pair X Y)) (binaryProductLimit X Y)))
                  ⋯ :
                binaryProductFunctor.obj X ≅ Functor.obj prod.functor X))
            X) ≫
        Functor.map prod.functor x)
      x_1)

Tactic:
apply Limits.prod.hom_ext

Premises used: CategoryTheory.Limits.prod.hom_ext