-- 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
m : c.pt ⟶ T
⊢ m =
    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)
                  (c.inl ≫ m) :
                (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)
                  (c.inr ≫ m) :
                (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 := ⋯ }
have mpr : ∀ (x : (↑c.pt : Type u)),
  Eq (α := (↑T : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) m :
          (a : (↑c.pt : 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) (X := c.pt)
            (Y := T)
            (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) (c.inl ≫ m) :
                        (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) (c.inr ≫ m) :
                        (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)),
                continuous_toFun := sorry }) :
          (a : (↑c.pt : Type u)) → (↑T : Type u))
        x :
      (↑T : Type u))
Tactic: ext x