-- Module: Mathlib.Topology.Category.TopCat.Limits.Products
Goal:
X Y : TopCat
c : BinaryCofan X Y
h : IsColimit c
mp :
  Eq (α := Set (↑c.pt : Type u))
    (Set.image (α := (↑(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))
      (range (ι := (↑X : 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))))
    (Set.image (α := (↑(X.binaryCofan Y).pt : Type u))
      (⇑(homeoOfIso (h.coconePointUniqueUpToIso (X.binaryCofanIsColimit Y))).symm :
        (a : (↑(X.binaryCofan Y).pt : Type u)) → (↑c.pt : Type u))
      (range (ι := (↑Y : 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)))ᶜ)
mp₁ :
  Eq (α := Set (↑c.pt : Type u))
    (Set.image (α := (↑(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))
      (range (ι := (↑X : 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))))
    (Set.image (α := (↑(X.binaryCofan Y).pt : Type u))
      (⇑(homeoOfIso (h.coconePointUniqueUpToIso (X.binaryCofanIsColimit Y))).symm :
        (a : (↑(X.binaryCofan Y).pt : Type u)) → (↑c.pt : Type u))
      (range Sum.inl))
mp₂ mp₃ :
  Eq (α := Set (↑c.pt : Type u))
    (Set.image (α := (↑(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))
      ((fun (x : (↑(X.binaryCofan Y).pt : Type u)) ↦ x) ''
        range (ι := (↑X : 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))))
    (Set.image (α := (↑(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))
      ((fun (x : (↑(X.binaryCofan Y).pt : Type u)) ↦ x) ''
        range (ι := (↑X : 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))))
⊢ Eq (α := Set (↑c.pt : Type u))
    (Set.image (α := (↑(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))
      (range (ι := (↑X : 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))))
    (Set.image (α := (↑(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))
        (range (ι := (↑Y : 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:
erw [← Set.image_compl_eq (homeoOfIso <| h.coconePointUniqueUpToIso
            (binaryCofanIsColimit X Y)).symm.bijective, Set.compl_range_inr, Set.image_comp]

Premises used: Set.compl_range_inr, Set.image_compl_eq, TopCat.homeoOfIso, Homeomorph.symm, Set.image_comp, Homeomorph.bijective, TopCat.binaryCofanIsColimit, CategoryTheory.Limits.IsColimit.coconePointUniqueUpToIso