-- Lean 4 proof step from Mathlib.Topology.Gluing (goal)
Goal:
D : GlueData
α : Type u
inst : TopologicalSpace α
J : Type u
U : J → Opens α
i : J
⊢ 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
have 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)) sorry)
                  sorry,
              continuous_toFun := sorry :
              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
Tactic: ext