-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Products (goal)
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))
⊢ 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))
have 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))
Tactic: rw [ConcreteCategory.comp_apply, TopCat.prodIsoProd_inv_fst_apply]