-- Module: Mathlib.Topology.Category.TopCat.Limits.Products
Goal:
J : Type v
inst : Category.{w, v} J
X Y : TopCat
refine_1 :
  ∀ (s : BinaryCofan X Y),
    Continuous (X := (↑X : Type u) ⊕ (↑Y : Type u)) (Y := (↑s.1 : Type u))
      (Sum.elim
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
              s.inl) :
          (a : (↑((pair X Y).obj { as := WalkingPair.left }) : Type u)) →
            (↑(((Functor.const (Discrete WalkingPair)).obj s.pt).obj { as := WalkingPair.left }) : Type u))
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
              s.inr) :
          (a : (↑((pair X Y).obj { as := WalkingPair.right }) : Type u)) →
            (↑(((Functor.const (Discrete WalkingPair)).obj s.pt).obj { as := WalkingPair.right }) : Type u)))
refine_2 :
  ∀ (s : BinaryCofan X Y),
    ofHom { toFun := Sum.inl, continuous_toFun := ⋯ : C((↑X : Type u), (↑X : Type u) ⊕ (↑Y : Type u)) } ≫
        (fun (s : BinaryCofan X Y) ↦
            (ofHom
                {
                  toFun :=
                    Sum.elim
                      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                            carrier) s.inl) :
                        (a : (↑((pair X Y).obj { as := WalkingPair.left }) : Type u)) →
                          (↑(((Functor.const (Discrete WalkingPair)).obj s.pt).obj { as := WalkingPair.left }) :
                            Type u))
                      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                            carrier) s.inr) :
                        (a : (↑((pair X Y).obj { as := WalkingPair.right }) : Type u)) →
                          (↑(((Functor.const (Discrete WalkingPair)).obj s.pt).obj { as := WalkingPair.right }) :
                            Type u)),
                  continuous_toFun := ⋯ } :
              of ((↑X : Type u) ⊕ (↑Y : Type u)) ⟶ of (↑s.1 : Type u)))
          s =
      s.inl
refine_3 :
  ∀ (s : BinaryCofan X Y),
    ofHom { toFun := Sum.inr, continuous_toFun := ⋯ : C((↑Y : Type u), (↑X : Type u) ⊕ (↑Y : Type u)) } ≫
        (fun (s : BinaryCofan X Y) ↦
            (ofHom
                {
                  toFun :=
                    Sum.elim
                      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                            carrier) s.inl) :
                        (a : (↑((pair X Y).obj { as := WalkingPair.left }) : Type u)) →
                          (↑(((Functor.const (Discrete WalkingPair)).obj s.pt).obj { as := WalkingPair.left }) :
                            Type u))
                      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                            carrier) s.inr) :
                        (a : (↑((pair X Y).obj { as := WalkingPair.right }) : Type u)) →
                          (↑(((Functor.const (Discrete WalkingPair)).obj s.pt).obj { as := WalkingPair.right }) :
                            Type u)),
                  continuous_toFun := ⋯ } :
              of ((↑X : Type u) ⊕ (↑Y : Type u)) ⟶ of (↑s.1 : Type u)))
          s =
      s.inr
refine_4 :
  ∀ (s : BinaryCofan X Y) (m : of ((↑X : Type u) ⊕ (↑Y : Type u)) ⟶ s.pt),
    ofHom { toFun := Sum.inl, continuous_toFun := ⋯ : C((↑X : Type u), (↑X : Type u) ⊕ (↑Y : Type u)) } ≫ m = s.inl →
      ofHom { toFun := Sum.inr, continuous_toFun := ⋯ : C((↑Y : Type u), (↑X : Type u) ⊕ (↑Y : Type u)) } ≫ m = s.inr →
        m =
          (fun (s : BinaryCofan X Y) ↦
              (ofHom
                  {
                    toFun :=
                      Sum.elim
                        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                              carrier) s.inl) :
                          (a : (↑((pair X Y).obj { as := WalkingPair.left }) : Type u)) →
                            (↑(((Functor.const (Discrete WalkingPair)).obj s.pt).obj { as := WalkingPair.left }) :
                              Type u))
                        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                              carrier) s.inr) :
                          (a : (↑((pair X Y).obj { as := WalkingPair.right }) : Type u)) →
                            (↑(((Functor.const (Discrete WalkingPair)).obj s.pt).obj { as := WalkingPair.right }) :
                              Type u)),
                    continuous_toFun := ⋯ } :
                of ((↑X : Type u) ⊕ (↑Y : Type u)) ⟶ of (↑s.1 : Type u)))
            s
⊢ IsColimit (X.binaryCofan Y)

Tactic:
refine Limits.BinaryCofan.isColimitMk (fun s => ofHom
    { toFun := Sum.elim s.inl s.inr, continuous_toFun := ?_ }) ?_ ?_ ?_

Premises used: CategoryTheory.Limits.BinaryCofan.inr, CategoryTheory.ConcreteCategory.hom, CategoryTheory.Limits.BinaryCofan.isColimitMk, ContinuousMap.mk, TopCat.ofHom, CategoryTheory.Limits.BinaryCofan.inl, DFunLike.coe, Sum.elim