-- Module: Mathlib.Topology.Category.TopCat.Limits.Products
Goal:
W X Y Z : TopCat
f : W ⟶ Y
g : X ⟶ Z
x : (↑(Y ⨯ Z) : Type u)
x₁ : (↑W : Type u)
hx₁ :
  Eq (α := (↑Y : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f :
          (a : (↑W : Type u)) → (↑Y : Type u))
        x₁ :
      (↑Y : Type u))
    ((@ConcreteCategory.hom _ instCategory (fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) carrier _ _
            (Y ⨯ Z) _ prod.fst :
          (a : (↑(Y ⨯ Z) : Type u)) → (↑Y : Type u))
        x :
      (↑Y : Type u))
x₂ : (↑X : Type u)
hx₂ :
  Eq (α := (↑Z : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) g :
          (a : (↑X : Type u)) → (↑Z : Type u))
        x₂ :
      (↑Z : Type u))
    ((@ConcreteCategory.hom _ instCategory (fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) carrier _ _
            (Y ⨯ Z) _ prod.snd :
          (a : (↑(Y ⨯ Z) : Type u)) → (↑Z : Type u))
        x :
      (↑Z : Type u))
h :
  Eq (α := (↑(Functor.obj (pair Y Z) { as := WalkingPair.left : Discrete WalkingPair }) : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f :
          (a : (↑W : Type u)) → (↑((pair Y Z).obj { as := WalkingPair.left }) : Type u))
        (x₁, x₂).1 :
      (↑(Functor.obj (pair Y Z) { as := WalkingPair.left : Discrete WalkingPair }) : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
            limit (pair Y Z)) (Y := Functor.obj (pair Y Z) { as := WalkingPair.left : Discrete WalkingPair })
            (limit.π (pair Y Z) { as := WalkingPair.left }) :
          (a : (↑(limit (pair Y Z)) : Type u)) → (↑((pair Y Z).obj { as := WalkingPair.left }) : Type u))
        x :
      (↑(Functor.obj (pair Y Z) { as := WalkingPair.left : Discrete WalkingPair }) : Type u))
⊢ Eq (α := (↑(Functor.obj (pair Y Z) { as := WalkingPair.left : Discrete WalkingPair }) : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X := W ⨯ X)
            (prod.fst ≫ f) :
          (a : (↑(W ⨯ X) : Type u)) → (↑((pair Y Z).obj { as := WalkingPair.left }) : Type u))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                (W.prodIsoProd X).inv :
              (a : (↑(of ((↑W : Type u) × (↑X : Type u))) : Type u)) → (↑(W ⨯ X) : Type u))
            (x₁, x₂) :
          (↑(W ⨯ X) : Type u)) :
      (↑(Functor.obj (pair Y Z) { as := WalkingPair.left : Discrete WalkingPair }) : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
            limit (pair Y Z)) (Y := Functor.obj (pair Y Z) { as := WalkingPair.left : Discrete WalkingPair })
            (limit.π (pair Y Z) { as := WalkingPair.left }) :
          (a : (↑(limit (pair Y Z)) : Type u)) → (↑((pair Y Z).obj { as := WalkingPair.left }) : Type u))
        x :
      (↑(Functor.obj (pair Y Z) { as := WalkingPair.left : Discrete WalkingPair }) : Type u))

Tactic:
rw [ConcreteCategory.comp_apply, TopCat.prodIsoProd_inv_fst_apply]

Premises used: CategoryTheory.ConcreteCategory.comp_apply, TopCat.prodIsoProd_inv_fst_apply