-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Products (goal)
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 : (↑c.1 : Type u) → (↑T : Type u)
⊢ c.pt ⟶ T
have mpr₁ : Continuous (Y := (↑T : 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))
                sorry).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))
                sorry).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 sorry) :
        (↑(Functor.obj (pair X Y) { as := WalkingPair.right : Discrete WalkingPair }) : Type u))
Tactic: refine ofHom (ContinuousMap.mk ?_ ?_)