-- 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 := (↑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))))
have mp : 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: refine ⟨(homeoOfIso <| h.coconePointUniqueUpToIso
        (binaryCofanIsColimit X Y)).symm.isOpenEmbedding.comp .inl,
          (homeoOfIso <| h.coconePointUniqueUpToIso
            (binaryCofanIsColimit X Y)).symm.isOpenEmbedding.comp .inr, ?_⟩