-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Products (goal)
Goal:
X Y : TopCat
c : BinaryCofan X Y
h : IsColimit c
⊢ IsOpenEmbedding (X := (↑(Functor.obj (pair X Y) { as := WalkingPair.left : Discrete WalkingPair }) : Type u)) (Y :=
      (↑(Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt)
            { 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 :=
            Functor.obj (pair X Y) { as := WalkingPair.left : Discrete WalkingPair })
            ((X.binaryCofan Y).ι.app { as := WalkingPair.left } ≫
              (h.coconePointUniqueUpToIso (X.binaryCofanIsColimit Y)).inv)) :
        (a : (↑((pair X Y).obj { as := WalkingPair.left }) : Type u)) →
          (↑(((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left }) : Type u)) ∧
    IsOpenEmbedding (X := (↑(Functor.obj (pair X Y) { as := WalkingPair.right : Discrete WalkingPair }) : Type u)) (Y :=
        (↑(Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt)
              { as := WalkingPair.right : Discrete WalkingPair }) :
          Type u))
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
              Functor.obj (pair X Y) { as := WalkingPair.right : Discrete WalkingPair })
              ((X.binaryCofan Y).ι.app { as := WalkingPair.right } ≫
                (h.coconePointUniqueUpToIso (X.binaryCofanIsColimit Y)).inv)) :
          (a : (↑((pair X Y).obj { as := WalkingPair.right }) : Type u)) →
            (↑(((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.right }) : Type u)) ∧
      IsCompl (α :=
        Set
          (↑(Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt)
                { as := WalkingPair.left : Discrete WalkingPair }) :
            Type u))
        (range (ι := (↑(Functor.obj (pair X Y) { 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 :=
                Functor.obj (pair X Y) { as := WalkingPair.left : Discrete WalkingPair })
                ((X.binaryCofan Y).ι.app { as := WalkingPair.left } ≫
                  (h.coconePointUniqueUpToIso (X.binaryCofanIsColimit Y)).inv)) :
            (a : (↑((pair X Y).obj { as := WalkingPair.left }) : Type u)) →
              (↑(((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left }) : Type u)))
        (range (ι := (↑(Functor.obj (pair X Y) { as := WalkingPair.right : Discrete WalkingPair }) : Type u))
          (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
                Functor.obj (pair X Y) { as := WalkingPair.right : Discrete WalkingPair })
                ((X.binaryCofan Y).ι.app { as := WalkingPair.right } ≫
                  (h.coconePointUniqueUpToIso (X.binaryCofanIsColimit Y)).inv)) :
            (a : (↑((pair X Y).obj { as := WalkingPair.right }) : Type u)) →
              (↑(((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.right }) : Type u)))
have mp : IsOpenEmbedding (X := (↑X : Type u)) (Y := (↑c.pt : Type u))
    (Function.comp (β := (↑(X.binaryCofan Y).pt : Type u))
      (⇑(Hom.hom (h.coconePointUniqueUpToIso (X.binaryCofanIsColimit Y)).inv) :
        (a : (↑(X.binaryCofan Y).pt : Type u)) → (↑c.pt : Type u))
      (⇑(Hom.hom ((X.binaryCofan Y).ι.app { as := WalkingPair.left }) :
            C((↑X : Type u), (↑(X.binaryCofan Y).pt : Type u))) :
        (a : (↑X : Type u)) → (↑(X.binaryCofan Y).pt : Type u))) ∧
  IsOpenEmbedding (X := (↑Y : Type u)) (Y := (↑c.pt : Type u))
      (Function.comp (β := (↑(X.binaryCofan Y).pt : Type u))
        (⇑(Hom.hom (h.coconePointUniqueUpToIso (X.binaryCofanIsColimit Y)).inv) :
          (a : (↑(X.binaryCofan Y).pt : Type u)) → (↑c.pt : Type u))
        (⇑(Hom.hom ((X.binaryCofan Y).ι.app { as := WalkingPair.right }) :
              C((↑Y : Type u), (↑(X.binaryCofan Y).pt : Type u))) :
          (a : (↑Y : Type u)) → (↑(X.binaryCofan Y).pt : Type u))) ∧
    IsCompl (α := Set (↑c.pt : Type u))
      (range (ι := (↑X : Type u))
        (Function.comp (β := (↑(X.binaryCofan Y).pt : Type u))
          (⇑(Hom.hom (h.coconePointUniqueUpToIso (X.binaryCofanIsColimit Y)).inv) :
            (a : (↑(X.binaryCofan Y).pt : Type u)) → (↑c.pt : Type u))
          (⇑(Hom.hom ((X.binaryCofan Y).ι.app { as := WalkingPair.left }) :
                C((↑X : Type u), (↑(X.binaryCofan Y).pt : Type u))) :
            (a : (↑X : Type u)) → (↑(X.binaryCofan Y).pt : Type u))))
      (range (ι := (↑Y : Type u))
        (Function.comp (β := (↑(X.binaryCofan Y).pt : Type u))
          (⇑(Hom.hom (h.coconePointUniqueUpToIso (X.binaryCofanIsColimit Y)).inv) :
            (a : (↑(X.binaryCofan Y).pt : Type u)) → (↑c.pt : Type u))
          (⇑(Hom.hom ((X.binaryCofan Y).ι.app { as := WalkingPair.right }) :
                C((↑Y : Type u), (↑(X.binaryCofan Y).pt : Type u))) :
            (a : (↑Y : Type u)) → (↑(X.binaryCofan Y).pt : Type u))))
Tactic: dsimp