-- Module: Mathlib.Topology.Category.TopCat.Limits.Products
Goal:
X Y : TopCat
c : BinaryCofan X Y
mp :
  Nonempty (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)
              c.inl) :
          (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)
                c.inr) :
            (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)
                  c.inl) :
              (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)
                  c.inr) :
              (a : (↑((pair X Y).obj { as := WalkingPair.right }) : Type u)) →
                (↑(((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.right }) : Type u)))
mpr :
  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)
              c.inl) :
          (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)
                c.inr) :
            (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)
                  c.inl) :
              (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)
                  c.inr) :
              (a : (↑((pair X Y).obj { as := WalkingPair.right }) : Type u)) →
                (↑(((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.right }) : Type u))) →
    Nonempty (IsColimit c)
⊢ Nonempty (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)
              c.inl) :
          (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)
                c.inr) :
            (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)
                  c.inl) :
              (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)
                  c.inr) :
              (a : (↑((pair X Y).obj { as := WalkingPair.right }) : Type u)) →
                (↑(((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.right }) : Type u)))

Tactic:
constructor