-- 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_1 :
  ∀
    (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
T : TopCat
f : X ⟶ T
g : Y ⟶ T
this :
  ∀
    a ∉
      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)),
    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)))
      a
neg :
  Continuous
    (Subtype.map (p :=
      fun
        (a :
          (↑(Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt)
                { as := WalkingPair.left : Discrete WalkingPair }) :
            Type u)) ↦
      a ∉
        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)))
      (q :=
      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)
      (fun
          (a :
            (↑(Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt)
                  { as := WalkingPair.left : Discrete WalkingPair }) :
              Type u)) ↦
        a)
      this)
⊢ Continuous (Y := (↑Y : Type u))
    ((⇑⋯.toHomeomorph.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.map (p :=
        fun
          (a :
            (↑(Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt)
                  { as := WalkingPair.left : Discrete WalkingPair }) :
              Type u)) ↦
        a ∉
          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)))
        (q :=
        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)
        (fun
            (a :
              (↑(Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt)
                    { as := WalkingPair.left : Discrete WalkingPair }) :
                Type u)) ↦
          a)
        this)

Tactic:
apply Continuous.comp (by fun_prop)

Premises used: Continuous.comp