-- Lean 4 proof step from Mathlib.Topology.Gluing (goal)
Goal:
α : Type u
inst : TopologicalSpace α
J : Type u
U : J → Opens α
s : Set (↑(ofOpenSubsets U).glued : Type u)
hs :
  ∀ (i : (ofOpenSubsets U).J),
    IsOpen (X := (↑((ofOpenSubsets U).U i) : 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)) ⁻¹'
        s)
i : (ofOpenSubsets U).J
x : (↑(of α) : Type u)
hx' : x ∈ U i
hx :
  Membership.mem (α := (↑(ofOpenSubsets U).glued : Type u)) s
    ((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))
⊢ Subset (α := Set (↑(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)) ''
          s ∩
        Set.range (ι := (↑(Functor.obj (Opens.toTopCat (of α)) (U i)) : Type u))
          (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
                Functor.obj (Opens.toTopCat (of α)) (U i)) (U i).inclusion') :
            (a : (↑((Opens.toTopCat (of α)).obj (U i)) : 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)) ''
        s) ∧
    IsOpen[inst]
        ((⇑(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)) ''
            s ∩
          Set.range (ι := (↑(Functor.obj (Opens.toTopCat (of α)) (U i)) : Type u))
            (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                  (X := Functor.obj (Opens.toTopCat (of α)) (U i)) (U i).inclusion') :
              (a : (↑((Opens.toTopCat (of α)).obj (U i)) : Type u)) → (↑(of α) : Type u))) ∧
      Membership.mem (α := (↑(of α) : Type u)) (γ := Set (↑(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)) ''
            s ∩
          Set.range (ι := (↑(Functor.obj (Opens.toTopCat (of α)) (U i)) : Type u))
            (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                  (X := Functor.obj (Opens.toTopCat (of α)) (U i)) (U i).inclusion') :
              (a : (↑((Opens.toTopCat (of α)).obj (U i)) : 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).ι 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))
have right : IsOpen[inst]
    ((⇑(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)) ''
        s ∩
      Set.range (ι := (↑(Functor.obj (Opens.toTopCat (of α)) (U i)) : Type u))
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
              Functor.obj (Opens.toTopCat (of α)) (U i)) (U i).inclusion') :
          (a : (↑((Opens.toTopCat (of α)).obj (U i)) : Type u)) → (↑(of α) : Type u))) ∧
  Membership.mem (α := (↑(of α) : Type u)) (γ := Set (↑(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)) ''
        s ∩
      Set.range (ι := (↑(Functor.obj (Opens.toTopCat (of α)) (U i)) : Type u))
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
              Functor.obj (Opens.toTopCat (of α)) (U i)) (U i).inclusion') :
          (a : (↑((Opens.toTopCat (of α)).obj (U i)) : 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).ι 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))
Tactic: use Set.inter_subset_left