-- Module: Mathlib.Topology.Category.TopCat.Limits.Products
Goal:
J : Type v
inst : Category.{w, v} J
ι : Type v
β : ι → TopCat
S : Cocone (Discrete.functor β)
m : (sigmaCofan.{v, u} β).pt ⟶ S.pt
h : ∀ (j : Discrete ι), (sigmaCofan.{v, u} β).ι.app j ≫ m = S.ι.app j
i : ι
x : (↑(β i) : Type (max u v))
w :
  Eq (α := (↑S.pt : Type (max u v)))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CC := carrier)
            m :
          (a : (↑(sigmaCofan β).pt : Type (max u v))) → (↑S.pt : Type (max u v)))
        (Sigma.mk (β := fun (i : ι) ↦ (↑(β i) : Type (max u v))) i x) :
      (↑S.pt : Type (max u v)))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CC := carrier)
            (ofHom
              {
                toFun := fun (s : (i : ι) × (↑(β i) : Type (max u v))) ↦
                  (ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v))))
                        (CC := carrier) (X :=
                        Functor.obj (Discrete.functor β)
                          { as := s.fst (β := fun (i : ι) ↦ (↑(β i) : Type (max u v))) : Discrete ι })
                        ((sigmaCofan.{v, u} β).ι.app
                            { as := s.fst (β := fun (i : ι) ↦ (↑(β i) : Type (max u v))) : Discrete ι } ≫
                          m) :
                      (a : (↑((Discrete.functor β).obj { as := s.fst }) : Type (max u v))) →
                        (↑(((Functor.const (Discrete ι)).obj S.pt).obj { as := s.fst }) : Type (max u v)))
                    (s.snd (β := fun (i : ι) ↦ (↑(β i) : Type (max u v)))),
                continuous_toFun := ⋯ : C((i : ι) × (↑(β i) : Type (max u v)), (↑S.1 : Type (max u v))) }) :
          (a : (↑(sigmaCofan β).pt : Type (max u v))) → (↑S.pt : Type (max u v)))
        (Sigma.mk (β := fun (i : ι) ↦ (↑(β i) : Type (max u v))) i x) :
      (↑S.pt : Type (max u v)))
⊢ Eq (α := (↑S.pt : Type (max u v)))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CC := carrier)
            m :
          (a : (↑(sigmaCofan β).pt : Type (max u v))) → (↑S.pt : Type (max u v)))
        (Sigma.mk (β := fun (i : ι) ↦ (↑(β i) : Type (max u v))) i x) :
      (↑S.pt : Type (max u v)))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CC := carrier)
            (ofHom
              {
                toFun := fun (s : (↑(of ((i : ι) × (↑(β i) : Type (max u v)))) : Type (max u v))) ↦
                  (ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v))))
                        (CC := carrier) (X :=
                        Functor.obj (Discrete.functor β)
                          { as := s.fst (β := fun (i : ι) ↦ (↑(β i) : Type (max u v))) : Discrete ι })
                        (S.ι.app { as := s.fst (β := fun (i : ι) ↦ (↑(β i) : Type (max u v))) : Discrete ι }) :
                      (a : (↑((Discrete.functor β).obj { as := s.fst }) : Type (max u v))) →
                        (↑(((Functor.const (Discrete ι)).obj S.pt).obj { as := s.fst }) : Type (max u v)))
                    (s.snd (β := fun (i : ι) ↦ (↑(β i) : Type (max u v)))),
                continuous_toFun := ⋯ : C((i : ι) × (↑(β i) : Type (max u v)), (↑S.1 : Type (max u v))) }) :
          (a : (↑(sigmaCofan β).pt : Type (max u v))) → (↑S.pt : Type (max u v)))
        (Sigma.mk (β := fun (i : ι) ↦ (↑(β i) : Type (max u v))) i x) :
      (↑S.pt : Type (max u v)))

Tactic:
simp only [← h]