-- 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
x : (↑(Functor.obj (pair X Y) { as := WalkingPair.right : 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.inr ≫
              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.right }) : 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) g :
          (a : (↑((pair X Y).obj { as := WalkingPair.right }) : Type u)) → (↑T : Type u))
        x :
      (↑T : Type u))
have mpr : Eq (α := (↑T : Type u))
  (if h :
        Membership.mem (α := (↑c.1 : Type u)) (γ := Set (↑c.pt : Type u))
          (range (ι := (↑X : Type u))
            (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                  c.inl) :
              (a : (↑X : Type u)) → (↑c.pt : Type u)))
          ((Hom.hom c.inr : (a : (↑Y : Type u)) → (↑c.pt : Type u)) x : (↑c.pt : Type u)) 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 : (↑X : Type u)) → (↑c.pt : Type u))
                  sorry).symm :
              (a : (↑(range (⇑(ConcreteCategory.hom c.inl) : (a : (↑X : Type u)) → (↑c.pt : Type u))) : Type u)) →
                (↑X : Type u))
            (Subtype.mk (p := fun (x : (↑c.pt : Type u)) ↦
                Membership.mem (γ := Set (↑c.pt : Type u))
                  (range (ι := (↑X : Type u))
                    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                          carrier) c.inl) :
                      (a : (↑X : Type u)) → (↑c.pt : Type u)))
                  x)
                ((Hom.hom c.inr : (a : (↑Y : Type u)) → (↑c.pt : Type u)) x) h :
              { x : (↑c.pt : Type u) //
                Membership.mem (γ := Set (↑c.pt : Type u))
                  (range (ι := (↑X : Type u))
                    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                          carrier) c.inl) :
                      (a : (↑X : Type u)) → (↑c.pt : Type u)))
                  x }) :
          (↑X : 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 : (↑Y : Type u)) → (↑c.pt : Type u))
                  sorry).symm :
              (a : (↑(range (⇑(ConcreteCategory.hom c.inr) : (a : (↑Y : Type u)) → (↑c.pt : Type u))) : Type u)) →
                (↑Y : Type u))
            (Subtype.mk (p := fun (x : (↑c.pt : Type u)) ↦
                Membership.mem (γ := Set (↑c.pt : Type u))
                  (range (ι := (↑Y : Type u))
                    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                          carrier) c.inr) :
                      (a : (↑Y : Type u)) → (↑c.pt : Type u)))
                  x)
                ((Hom.hom c.inr : (a : (↑Y : Type u)) → (↑c.pt : Type u)) x) sorry :
              { x : (↑c.pt : Type u) //
                Membership.mem (γ := Set (↑c.pt : Type u))
                  (range (ι := (↑Y : Type u))
                    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                          carrier) c.inr) :
                      (a : (↑Y : Type u)) → (↑c.pt : Type u)))
                  x }) :
          (↑Y : Type u)) :
    (↑T : 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))
      x :
    (↑T : Type u))
Tactic: dsimp