-- Module: Mathlib.Topology.Category.TopCat.Limits.Products
Goal:
X Y : TopCat
c : BinaryCofan X Y
h₁ :
  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))
h₂ :
  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))
h₃ :
  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)))
this :
  ∀
    (x :
      (↑(Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt)
            { as := WalkingPair.left : Discrete WalkingPair }) :
        Type u)),
    Membership.mem (γ :=
        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)))
        x ∨
      Membership.mem (γ :=
        Set
          (↑(Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt)
                { as := WalkingPair.right : Discrete WalkingPair }) :
            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)))
        x
mpr : {T : TopCat.{u}} → (X ⟶ T) → (Y ⟶ T) → (c.pt ⟶ T)
mpr₁ :
  ∀ {T : TopCat.{u}} (f : X ⟶ T) (g : Y ⟶ T),
    c.inl ≫
        ofHom
          {
            toFun := fun (x : (↑c.1 : Type u)) ↦
              if h :
                  Membership.mem (γ :=
                    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)))
                    x then
                (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                      f :
                    (a : (↑X : Type u)) → (↑T : Type u))
                  (((Equiv.ofInjective
                            (⇑(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))
                            ⋯).symm :
                        (a :
                            (↑(range
                                  (⇑(ConcreteCategory.hom 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))) :
                              Type u)) →
                          (↑((pair X Y).obj { as := WalkingPair.left }) : Type u))
                      (Subtype.mk (p :=
                        fun
                          (x :
                            (↑(Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt)
                                  { as := WalkingPair.left : Discrete WalkingPair }) :
                              Type u)) ↦
                        Membership.mem (γ :=
                          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)))
                          x)
                        x h) :
                    (↑(Functor.obj (pair X Y) { as := WalkingPair.left : Discrete WalkingPair }) : Type u))
              else
                (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                      g :
                    (a : (↑Y : Type u)) → (↑T : Type u))
                  (((Equiv.ofInjective
                            (⇑(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))
                            ⋯).symm :
                        (a :
                            (↑(range
                                  (⇑(ConcreteCategory.hom 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))) :
                              Type u)) →
                          (↑((pair X Y).obj { as := WalkingPair.right }) : Type u))
                      (Subtype.mk (p :=
                        fun
                          (x :
                            (↑(Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt)
                                  { as := WalkingPair.right : Discrete WalkingPair }) :
                              Type u)) ↦
                        Membership.mem (γ :=
                          Set
                            (↑(Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt)
                                  { as := WalkingPair.right : Discrete WalkingPair }) :
                              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)))
                          x)
                        x ⋯) :
                    (↑(Functor.obj (pair X Y) { as := WalkingPair.right : Discrete WalkingPair }) : Type u)),
            continuous_toFun := ⋯ } =
      f
mpr₂ :
  ∀ {T : TopCat.{u}} (f : X ⟶ T) (g : Y ⟶ T),
    c.inr ≫
        ofHom
          {
            toFun := fun (x : (↑c.1 : Type u)) ↦
              if h :
                  Membership.mem (γ :=
                    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)))
                    x then
                (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                      f :
                    (a : (↑X : Type u)) → (↑T : Type u))
                  (((Equiv.ofInjective
                            (⇑(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))
                            ⋯).symm :
                        (a :
                            (↑(range
                                  (⇑(ConcreteCategory.hom 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))) :
                              Type u)) →
                          (↑((pair X Y).obj { as := WalkingPair.left }) : Type u))
                      (Subtype.mk (p :=
                        fun
                          (x :
                            (↑(Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt)
                                  { as := WalkingPair.left : Discrete WalkingPair }) :
                              Type u)) ↦
                        Membership.mem (γ :=
                          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)))
                          x)
                        x h) :
                    (↑(Functor.obj (pair X Y) { as := WalkingPair.left : Discrete WalkingPair }) : Type u))
              else
                (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                      g :
                    (a : (↑Y : Type u)) → (↑T : Type u))
                  (((Equiv.ofInjective
                            (⇑(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))
                            ⋯).symm :
                        (a :
                            (↑(range
                                  (⇑(ConcreteCategory.hom 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))) :
                              Type u)) →
                          (↑((pair X Y).obj { as := WalkingPair.right }) : Type u))
                      (Subtype.mk (p :=
                        fun
                          (x :
                            (↑(Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt)
                                  { as := WalkingPair.right : Discrete WalkingPair }) :
                              Type u)) ↦
                        Membership.mem (γ :=
                          Set
                            (↑(Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt)
                                  { as := WalkingPair.right : Discrete WalkingPair }) :
                              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)))
                          x)
                        x ⋯) :
                    (↑(Functor.obj (pair X Y) { as := WalkingPair.right : Discrete WalkingPair }) : Type u)),
            continuous_toFun := ⋯ } =
      g
mpr₃ :
  ∀ {T : TopCat.{u}} (f : X ⟶ T) (g : Y ⟶ T) (m : c.pt ⟶ T),
    c.inl ≫ m = f →
      c.inr ≫ m = g →
        m =
          ofHom
            {
              toFun := fun (x : (↑c.1 : Type u)) ↦
                if h :
                    Membership.mem (γ :=
                      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)))
                      x then
                  (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                        f :
                      (a : (↑X : Type u)) → (↑T : Type u))
                    (((Equiv.ofInjective
                              (⇑(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))
                              ⋯).symm :
                          (a :
                              (↑(range
                                    (⇑(ConcreteCategory.hom 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))) :
                                Type u)) →
                            (↑((pair X Y).obj { as := WalkingPair.left }) : Type u))
                        (Subtype.mk (p :=
                          fun
                            (x :
                              (↑(Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt)
                                    { as := WalkingPair.left : Discrete WalkingPair }) :
                                Type u)) ↦
                          Membership.mem (γ :=
                            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)))
                            x)
                          x h) :
                      (↑(Functor.obj (pair X Y) { as := WalkingPair.left : Discrete WalkingPair }) : Type u))
                else
                  (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                        g :
                      (a : (↑Y : Type u)) → (↑T : Type u))
                    (((Equiv.ofInjective
                              (⇑(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))
                              ⋯).symm :
                          (a :
                              (↑(range
                                    (⇑(ConcreteCategory.hom 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))) :
                                Type u)) →
                            (↑((pair X Y).obj { as := WalkingPair.right }) : Type u))
                        (Subtype.mk (p :=
                          fun
                            (x :
                              (↑(Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt)
                                    { as := WalkingPair.right : Discrete WalkingPair }) :
                                Type u)) ↦
                          Membership.mem (γ :=
                            Set
                              (↑(Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt)
                                    { as := WalkingPair.right : Discrete WalkingPair }) :
                                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)))
                            x)
                          x ⋯) :
                      (↑(Functor.obj (pair X Y) { as := WalkingPair.right : Discrete WalkingPair }) : Type u)),
              continuous_toFun := ⋯ }
⊢ Nonempty (IsColimit c)

Tactic:
refine ⟨BinaryCofan.IsColimit.mk _ ?_ ?_ ?_ ?_⟩