-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits
Goal:
J : Type u'
inst : Category.{v', u'} J
C : Type u
inst_1 : Category.{v, u} C
inst_2 : HasColimitsOfShape.{v', u', v, v + 1} J TopCat
inst_3 : ∀ (X : TopCat.{v}), HasLimitsOfShape Jᵒᵖ (Presheaf C X)
inst_4 : HasLimitsOfShape.{v', u', v, u} Jᵒᵖ C
F : J ⥤ PresheafedSpace.{v, u, v} C
inst_5 : HasColimit F
U : Opens (↑(↑(Limits.colimit F) : TopCat) : Type v)
X : Jᵒᵖ
app :
  ∀ (x : (↑((F ⋙ forget C).obj (unop X)) : Type v)),
    Eq (α := (↑(↑(Limits.colimit F) : TopCat) : Type v))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
              (Y := (↑(Limits.colimit F) : TopCat))
              (Hom.base
                (Iso.hom
                  (Iso.symm
                    (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F })))) :
            (a : (↑(↑(colimitCocone F).pt : TopCat) : Type v)) → (↑(↑(Limits.colimit F) : TopCat) : Type v))
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
                  (X := (F ⋙ forget C).obj (unop X)) (Y := Limits.colimit (F ⋙ forget C))
                  (colimit.ι (F ⋙ forget C) (unop X)) :
                (a : (↑((F ⋙ forget C).obj (unop X)) : Type v)) → (↑(Limits.colimit (F ⋙ forget C)) : Type v))
              x :
            (↑(Limits.colimit (F ⋙ forget C)) : Type v)) :
        (↑(↑(Limits.colimit F) : TopCat) : Type v))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
              (X := (↑(F.obj (unop X)) : TopCat)) (Y := (↑(Limits.colimit F) : TopCat))
              (Hom.base (colimit.ι F (unop X))) :
            (a : (↑(↑(F.obj (unop X)) : TopCat) : Type v)) → (↑(↑(Limits.colimit F) : TopCat) : Type v))
          x :
        (↑(↑(Limits.colimit F) : TopCat) : Type v))
⊢ Eq (α := Set (↑((F ⋙ forget C).obj (unop X)) : Type v))
    ((fun (x : (↑((F ⋙ forget C).obj (unop X)) : Type v)) ↦
        (ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
              (Y := (↑(Limits.colimit F) : TopCat))
              (Hom.base
                (Iso.hom
                  (Iso.symm
                    (colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F })))) :
            (a : (↑(↑(colimitCocone F).pt : TopCat) : Type v)) → (↑(↑(Limits.colimit F) : TopCat) : Type v))
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
                  (X := (F ⋙ forget C).obj (unop X)) (Y := Limits.colimit (F ⋙ forget C))
                  (colimit.ι (F ⋙ forget C) (unop X)) :
                (a : (↑((F ⋙ forget C).obj (unop X)) : Type v)) → (↑(Limits.colimit (F ⋙ forget C)) : Type v))
              x :
            (↑(Limits.colimit (F ⋙ forget C)) : Type v))) ⁻¹'
      (↑U : Set (↑(↑(Limits.colimit F) : TopCat) : Type v)))
    ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
            (X := (↑(F.obj (unop X)) : TopCat)) (Y := (↑(Limits.colimit F) : TopCat))
            (Hom.base (colimit.ι F (unop X)))) :
        (a : (↑(↑(F.obj (unop X)) : TopCat) : Type v)) → (↑(↑(Limits.colimit F) : TopCat) : Type v)) ⁻¹'
      (↑U : Set (↑(↑(Limits.colimit F) : TopCat) : Type v)))

Tactic:
refine congr_arg (Set.preimage · U.1) (funext fun x => ?_)

Premises used: TopologicalSpace.Opens.carrier, congr_arg, funext, Set.preimage