-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Products (goal)
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
⊢ IsColimit (X.binaryCofan Y)
have refine_4 : ∀ (s : BinaryCofan X Y) (m : of ((↑X : Type u) ⊕ (↑Y : Type u)) ⟶ s.pt),
  ofHom { toFun := Sum.inl, continuous_toFun := sorry : C((↑X : Type u), (↑X : Type u) ⊕ (↑Y : Type u)) } ≫ m = s.inl →
    ofHom { toFun := Sum.inr, continuous_toFun := sorry : 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 := sorry } :
              of ((↑X : Type u) ⊕ (↑Y : Type u)) ⟶ of (↑s.1 : Type u)))
          s
Tactic: refine Limits.BinaryCofan.isColimitMk (fun s => ofHom
    { toFun := Sum.elim s.inl s.inr, continuous_toFun := ?_ }) ?_ ?_ ?_