-- Module: Mathlib.Topology.Gluing
Goal:
α : Type u
inst : TopologicalSpace α
J : Type u
U : J → Opens α
i : (ofOpenSubsets U).J
x : (↑(of α) : Type u)
hx : x ∈ U i
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) (X :=
            (ofOpenSubsets U).U i) (U i).inclusion' :
          (a : (↑((ofOpenSubsets U).U i) : Type u)) → α)
        (Subtype.mk (p := fun (x : (↑(of α) : Type u)) ↦ x ∈ U i) x hx) :
      α)
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
            (ofOpenSubsets U).U j) (U j).inclusion' :
          (a : (↑((ofOpenSubsets U).U j) : Type u)) → α)
        (Subtype.mk (p := fun (x : (↑(of α) : Type u)) ↦ x ∈ U j) y hy) :
      α)
subst :
  ∀
    (hy :
      Membership.mem (α := (↑(of α) : Type u)) (U j)
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
                (ofOpenSubsets U).U i) (U i).inclusion' :
              (a : (↑((ofOpenSubsets U).U i) : Type u)) → α)
            (Subtype.mk (p := fun (x : (↑(of α) : Type u)) ↦ x ∈ U i) x hx) :
          α)),
    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)
              ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                    (X := (ofOpenSubsets U).U i) (U i).inclusion' :
                  (a : (↑((ofOpenSubsets U).U i) : Type u)) → α)
                (Subtype.mk (p := fun (x : (↑(of α) : Type u)) ↦ x ∈ U i) x hx))
              hy :
            ↥(U j)) :
        (↑(ofOpenSubsets U).glued : 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:
subst e