-- 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 :
  ∀
    (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
mpr :
  ∀ (x : (↑(Functor.obj (pair X Y) { as := WalkingPair.left : Discrete WalkingPair }) : Type u)),
    Eq (α := (↑T : Type u))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (Y := T)
              (c.inl ≫
                ofHom
                  {
                    toFun := 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 h) :
                            (↑(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)),
                    continuous_toFun := ⋯ }) :
            (a : (↑((pair X Y).obj { as := WalkingPair.left }) : Type u)) → (↑T : Type u))
          x :
        (↑T : Type u))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f :
            (a : (↑((pair X Y).obj { as := WalkingPair.left }) : Type u)) → (↑T : Type u))
          x :
        (↑T : Type u))
⊢ c.inl ≫
      ofHom
        {
          toFun := 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 h) :
                  (↑(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)),
          continuous_toFun := ⋯ } =
    f

Tactic:
ext x