-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Products (goal)
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))
⊢ 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)))
have 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 := sorry : 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]