-- Lean 4 proof step from Mathlib.Topology.Gluing (goal)
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) :
      α)
⊢ 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))
have 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))
Tactic: subst e
Cleared hypotheses: y, hy, e