-- 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
h :
  (↑(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)))ᶜ :
        Type u) =
      { 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)) } →
    Eq (α :=
      (↑(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)))ᶜ :
          Type u) →
        (↑T : Type u))
      (restrict (π := fun (a : (↑c.1 : Type u)) ↦ (↑T : 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)))ᶜ
          fun (x : (↑c.1 : Type u)) ↦
          if h :
              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 then
            (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f :
                (a : (↑X : Type u)) → (↑T : Type u))
              (((Equiv.ofInjective
                        (⇑(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))
                        ⋯).symm :
                    (a :
                        (↑(range
                              (⇑(ConcreteCategory.hom 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))) :
                          Type u)) →
                      (↑((pair X Y).obj { as := WalkingPair.left }) : Type u))
                  (Subtype.mk (p :=
                    fun
                      (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)
                    x ⋯) :
                (↑(Functor.obj (pair X Y) { as := WalkingPair.left : Discrete WalkingPair }) : Type u))
          else
            (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) g :
                (a : (↑Y : Type u)) → (↑T : Type u))
              (((Equiv.ofInjective
                        (⇑(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))
                        ⋯).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.mk (p :=
                    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)
                    x ⋯) :
                (↑(Functor.obj (pair X Y) { as := WalkingPair.right : 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)))ᶜ :
              Type u)) →
          (↑T : Type u))
      (Function.comp (β := (↑Y : Type u))
          (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) g) :
            (a : (↑Y : Type u)) → (↑T : 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) :
        { 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)) } →
          (↑T : Type u))
neg :
  Continuous (Y := (↑T : Type u))
    (Function.comp (β := (↑Y : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) g) :
        (a : (↑Y : Type u)) → (↑T : 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))
⊢ Continuous.{u, u} (X :=
    (↑(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)))ᶜ :
      Type u))
    (Y := (↑T : Type u))
    (restrict (π := fun (a : (↑c.1 : Type u)) ↦ (↑T : 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)))ᶜ
      fun (x : (↑c.1 : Type u)) ↦
      if h :
          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 then
        (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f :
            (a : (↑X : Type u)) → (↑T : Type u))
          (((Equiv.ofInjective
                    (⇑(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))
                    ⋯).symm :
                (a :
                    (↑(range
                          (⇑(ConcreteCategory.hom 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))) :
                      Type u)) →
                  (↑((pair X Y).obj { as := WalkingPair.left }) : Type u))
              (Subtype.mk (p :=
                fun
                  (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)
                x ⋯) :
            (↑(Functor.obj (pair X Y) { as := WalkingPair.left : Discrete WalkingPair }) : Type u))
      else
        (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) g :
            (a : (↑Y : Type u)) → (↑T : Type u))
          (((Equiv.ofInjective
                    (⇑(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))
                    ⋯).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.mk (p :=
                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)
                x ⋯) :
            (↑(Functor.obj (pair X Y) { as := WalkingPair.right : Discrete WalkingPair }) : Type u)))

Tactic:
convert_to Continuous
                (g ∘ h₂.isEmbedding.toHomeomorph.symm ∘ Subtype.map _ this)

Premises used: Subtype.map, Continuous, CategoryTheory.ConcreteCategory.hom, Topology.IsOpenEmbedding.isEmbedding, Function.comp, Homeomorph.symm, DFunLike.coe, Topology.IsEmbedding.toHomeomorph