-- Lean 4 proof step from Mathlib.Topology.Gluing (goal)
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))
⊢ (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
have 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))
Tactic: obtain ⟨j, ⟨y, hy⟩, rfl⟩ := (ofOpenSubsets U).ι_jointly_surjective y
Cleared hypotheses: y, e