-- Module: Mathlib.Topology.Gluing
Goal:
α : Type u
inst : TopologicalSpace α
J : Type u
U : J → Opens α
y : (↑(ofOpenSubsets U).glued : Type u)
i : (ofOpenSubsets U).J
x : (↑(of α) : Type u)
hx : x ∈ U i
e :
  Eq (α := (↑(of α) : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
            (fromOpenSubsetsGlue U) :
          (a : (↑(ofOpenSubsets U).glued : Type u)) → (↑(of α) : Type u))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (Y :=
                (ofOpenSubsets U).glued) ((ofOpenSubsets U).ι i) :
              (a : (↑((ofOpenSubsets U).U i) : Type u)) → (↑(ofOpenSubsets U).glued : Type u))
            (Subtype.mk (p := fun (x : (↑(of α) : Type u)) ↦ x ∈ U i) x hx) :
          (↑(ofOpenSubsets U).glued : Type u)) :
      (↑(of α) : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
            (fromOpenSubsetsGlue U) :
          (a : (↑(ofOpenSubsets U).glued : Type u)) → (↑(of α) : Type u))
        y :
      (↑(of α) : Type u))
obtain :
  ∀ (j : (ofOpenSubsets U).J) (y : (↑(of α) : Type u)) (hy : y ∈ U j)
    (e :
      Eq (α := (↑(of α) : Type u))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                (fromOpenSubsetsGlue U) :
              (a : (↑(ofOpenSubsets U).glued : Type u)) → (↑(of α) : Type u))
            ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                    (Y := (ofOpenSubsets U).glued) ((ofOpenSubsets U).ι i) :
                  (a : (↑((ofOpenSubsets U).U i) : Type u)) → (↑(ofOpenSubsets U).glued : Type u))
                (Subtype.mk (p := fun (x : (↑(of α) : Type u)) ↦ x ∈ U i) x hx) :
              (↑(ofOpenSubsets U).glued : Type u)) :
          (↑(of α) : Type u))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                (fromOpenSubsetsGlue U) :
              (a : (↑(ofOpenSubsets U).glued : Type u)) → (↑(of α) : Type u))
            ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                    (Y := (ofOpenSubsets U).glued) ((ofOpenSubsets U).ι j) :
                  (a : (↑((ofOpenSubsets U).U j) : Type u)) → (↑(ofOpenSubsets U).glued : Type u))
                (Subtype.mk (p := fun (x : (↑(of α) : Type u)) ↦ x ∈ U j) y hy) :
              (↑(ofOpenSubsets U).glued : Type u)) :
          (↑(of α) : Type u))),
    Eq (α := (↑(ofOpenSubsets U).glued : Type u))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (Y :=
              (ofOpenSubsets U).glued) ((ofOpenSubsets U).ι i) :
            (a : (↑((ofOpenSubsets U).U i) : Type u)) → (↑(ofOpenSubsets U).glued : Type u))
          (Subtype.mk (p := fun (x : (↑(of α) : Type u)) ↦ x ∈ U i) x hx) :
        (↑(ofOpenSubsets U).glued : Type u))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (Y :=
              (ofOpenSubsets U).glued) ((ofOpenSubsets U).ι j) :
            (a : (↑((ofOpenSubsets U).U j) : Type u)) → (↑(ofOpenSubsets U).glued : Type u))
          (Subtype.mk (p := fun (x : (↑(of α) : Type u)) ↦ x ∈ U j) y hy) :
        (↑(ofOpenSubsets U).glued : Type u))
⊢ (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (Y :=
          (ofOpenSubsets U).glued) ((ofOpenSubsets U).ι i) :
        (a : (↑((ofOpenSubsets U).U i) : Type u)) → (↑(ofOpenSubsets U).glued : Type u))
      (Subtype.mk (p := fun (x : (↑(of α) : Type u)) ↦ x ∈ U i) x hx) =
    y

Tactic:
obtain ⟨j, ⟨y, hy⟩, rfl⟩ := (ofOpenSubsets U).ι_jointly_surjective y

Premises used: TopCat.GlueData.ofOpenSubsets, TopCat.GlueData.ι_jointly_surjective, rfl