-- Module: Mathlib.Topology.Gluing
Goal:
D : GlueData
α : Type u
inst : TopologicalSpace α
J : Type u
U : J → Opens α
i : J
h :
  ∀
    (x :
      (↑(Functor.obj (C := Opens (↑(Functor.obj (Opens.toTopCat (of α)) (U i)) : Type u))
            (Opens.toTopCat (Functor.obj (Opens.toTopCat (of α)) (U i)))
            (Functor.obj (Opens.map (U i).inclusion') (U i))) :
        Type u)),
    (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
            (ofHom
              {
                toFun := fun (x : ↥(Functor.obj (Opens.map (U i).inclusion') (U i))) ↦
                  Subtype.mk (p := fun (x : (↑(Functor.obj (Opens.toTopCat (of α)) (U i)) : Type u)) ↦
                    Membership.mem (γ := Opens (↑(Functor.obj (Opens.toTopCat (of α)) (U i)) : Type u))
                      (Functor.obj (Opens.map (U i).inclusion') (U i)) x)
                    (Subtype.mk (p := fun (x : (↑(of α) : Type u)) ↦ x ∈ U i)
                      (↑(↑x : (↑((Opens.toTopCat (of α)).obj (U i)) : Type u)) : (↑(of α) : Type u)) ⋯)
                    ⋯,
                continuous_toFun := ⋯ :
                C(↥(Functor.obj (Opens.map (U i).inclusion') (U i)),
                  ↥(Functor.obj (Opens.map (U i).inclusion') (U i))) }) :
          (a :
              (↑((Opens.toTopCat ((Opens.toTopCat (of α)).obj (U i))).obj ((Opens.map (U i).inclusion').obj (U i))) :
                Type u)) →
            (↑((Opens.toTopCat ((Opens.toTopCat (of α)).obj (U i))).obj ((Opens.map (U i).inclusion').obj (U i))) :
              Type u))
        x =
      id x
⊢ Eq (α :=
    (a :
        (↑(Functor.obj (C := Opens (↑(Functor.obj (Opens.toTopCat (of α)) (U i)) : Type u))
              (Opens.toTopCat (Functor.obj (Opens.toTopCat (of α)) (U i)))
              (Functor.obj (Opens.map (U i).inclusion') (U i))) :
          Type u)) →
      (↑(Functor.obj (C := Opens (↑(Functor.obj (Opens.toTopCat (of α)) (U i)) : Type u))
            (Opens.toTopCat (Functor.obj (Opens.toTopCat (of α)) (U i)))
            (Functor.obj (Opens.map (U i).inclusion') (U i))) :
        Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
          (ofHom
            {
              toFun := fun (x : ↥(Functor.obj (Opens.map (U i).inclusion') (U i))) ↦
                Subtype.mk (p := fun (x : (↑(Functor.obj (Opens.toTopCat (of α)) (U i)) : Type u)) ↦
                  Membership.mem (γ := Opens (↑(Functor.obj (Opens.toTopCat (of α)) (U i)) : Type u))
                    (Functor.obj (Opens.map (U i).inclusion') (U i)) x)
                  (Subtype.mk (p := fun (x : (↑(of α) : Type u)) ↦ x ∈ U i)
                    (↑(↑x : (↑((Opens.toTopCat (of α)).obj (U i)) : Type u)) : (↑(of α) : Type u)) ⋯)
                  ⋯,
              continuous_toFun := ⋯ :
              C(↥(Functor.obj (Opens.map (U i).inclusion') (U i)),
                ↥(Functor.obj (Opens.map (U i).inclusion') (U i))) })) :
      (a :
          (↑((Opens.toTopCat ((Opens.toTopCat (of α)).obj (U i))).obj ((Opens.map (U i).inclusion').obj (U i))) :
            Type u)) →
        (↑((Opens.toTopCat ((Opens.toTopCat (of α)).obj (U i))).obj ((Opens.map (U i).inclusion').obj (U i))) : Type u))
    id

Tactic:
ext