-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Products (goal)
Goal:
J : Type v
inst : Category.{w, v} J
X Y : TopCat
S : Cone (pair X Y)
left left₁ :
  Eq (α := S.pt ⟶ X)
    (ofHom
          {
            toFun := fun (s : (↑S.1 : Type u)) ↦
              ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                      (BinaryFan.fst S) :
                    (a : (↑S.pt : Type u)) → (↑X : Type u))
                  s,
                (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                      (BinaryFan.snd S) :
                    (a : (↑S.pt : Type u)) → (↑Y : Type u))
                  s),
            continuous_toFun := ⋯ : C((↑S.1 : Type u), (↑X : Type u) × (↑Y : Type u)) } ≫
        (X.prodBinaryFan Y).π.app { as := WalkingPair.left } :
      S.pt ⟶ X)
    (S.π.app { as := WalkingPair.left } :
      Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) S.pt)
          { as := WalkingPair.left : Discrete WalkingPair } ⟶
        Functor.obj (pair X Y) { as := WalkingPair.left : Discrete WalkingPair })
⊢ Eq (α := S.pt ⟶ Functor.obj (pair X Y) { as := WalkingPair.left : Discrete WalkingPair })
    (ofHom
        {
          toFun := fun (s : (↑S.1 : Type u)) ↦
            ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                    (BinaryFan.fst S) :
                  (a : (↑(((Functor.const (Discrete WalkingPair)).obj S.pt).obj { as := WalkingPair.left }) : Type u)) →
                    (↑((pair X Y).obj { as := WalkingPair.left }) : Type u))
                s,
              (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                    (BinaryFan.snd S) :
                  (a :
                      (↑(((Functor.const (Discrete WalkingPair)).obj S.pt).obj { as := WalkingPair.right }) : Type u)) →
                    (↑((pair X Y).obj { as := WalkingPair.right }) : Type u))
                s),
          continuous_toFun := ⋯ : C((↑S.1 : Type u), (↑X : Type u) × (↑Y : Type u)) } ≫
      (X.prodBinaryFan Y).π.app { as := WalkingPair.left })
    (S.π.app { as := WalkingPair.left })
have left₂ : ∀ (x : (↑S.pt : Type u)),
  Eq (α := (↑X : Type u))
    (((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (Y := X)
              (ofHom
                    {
                      toFun := fun (s : (↑S.1 : Type u)) ↦
                        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                                carrier) (BinaryFan.fst S) :
                              (a : (↑S.pt : Type u)) → (↑X : Type u))
                            s,
                          (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                                carrier) (BinaryFan.snd S) :
                              (a : (↑S.pt : Type u)) → (↑Y : Type u))
                            s),
                      continuous_toFun := sorry : C((↑S.1 : Type u), (↑X : Type u) × (↑Y : Type u)) } ≫
                  (X.prodBinaryFan Y).π.app { as := WalkingPair.left } :
                S.pt ⟶ X) :
            C((↑S.pt : Type u), (↑X : Type u))) :
          (a : (↑S.pt : Type u)) → (↑X : Type u))
        x :
      (↑X : Type u))
    (((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X := S.pt)
              (Y := X)
              (S.π.app { as := WalkingPair.left } :
                Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) S.pt)
                    { as := WalkingPair.left : Discrete WalkingPair } ⟶
                  Functor.obj (pair X Y) { as := WalkingPair.left : Discrete WalkingPair }) :
            C((↑S.pt : Type u), (↑X : Type u))) :
          (a : (↑S.pt : Type u)) → (↑X : Type u))
        x :
      (↑X : Type u))
Tactic: {dsimp; ext; rfl}