-- Module: Mathlib.Geometry.RingedSpace.OpenImmersion
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasLimits.{v, u} C
ι : Type v
F : Discrete ι ⥤ SheafedSpace.{u, v, v} C
inst_2 : HasColimit F
i : Discrete ι
inst_3 : HasStrictTerminalObjects.{v, u} C
U : Opens (↑(↑(F.obj i).toPresheafedSpace : TopCat) : Type v)
h₁ :
  Eq (α := (F ⋙ forgetToPresheafedSpace).obj i ⟶ Functor.obj forgetToPresheafedSpace (colimit F))
    (CategoryStruct.comp (Y := colimit (F ⋙ forgetToPresheafedSpace))
      (colimit.ι (F ⋙ forgetToPresheafedSpace) i :
        (F ⋙ forgetToPresheafedSpace).obj i ⟶ colimit (F ⋙ forgetToPresheafedSpace))
      (Iso.inv (preservesColimitIso forgetToPresheafedSpace F) :
        colimit (F ⋙ forgetToPresheafedSpace) ⟶ Functor.obj forgetToPresheafedSpace (colimit F)))
    (CategoryTheory.Functor.map forgetToPresheafedSpace (colimit.ι F i))
h₂ :
  Eq (α := F.obj i ⟶ colimit F) (colimit.ι F i)
    {
      hom :=
        CategoryStruct.comp (Y := colimit (F ⋙ forgetToPresheafedSpace))
          (colimit.ι (F ⋙ forgetToPresheafedSpace) i :
            (F ⋙ forgetToPresheafedSpace).obj i ⟶ colimit (F ⋙ forgetToPresheafedSpace))
          (Iso.inv (preservesColimitIso forgetToPresheafedSpace F) :
            colimit (F ⋙ forgetToPresheafedSpace) ⟶ Functor.obj forgetToPresheafedSpace (colimit F)) }
H :
  IsOpenEmbedding (X := (↑(↑((F ⋙ forgetToPresheafedSpace).obj i) : TopCat) : Type v)) (Y :=
    (↑(↑(Functor.obj forgetToPresheafedSpace (colimit F)) : TopCat) : Type v))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
          (Y := (↑(Functor.obj forgetToPresheafedSpace (colimit F)) : TopCat))
          (PresheafedSpace.Hom.base
            (CategoryStruct.comp (Y := colimit (F ⋙ forgetToPresheafedSpace))
              (colimit.ι (F ⋙ forgetToPresheafedSpace) i :
                (F ⋙ forgetToPresheafedSpace).obj i ⟶ colimit (F ⋙ forgetToPresheafedSpace))
              (Iso.inv (preservesColimitIso forgetToPresheafedSpace F) :
                colimit (F ⋙ forgetToPresheafedSpace) ⟶ Functor.obj forgetToPresheafedSpace (colimit F))))) :
      (a : (↑(↑((F ⋙ forgetToPresheafedSpace).obj i) : TopCat) : Type v)) →
        (↑(↑(forgetToPresheafedSpace.obj (colimit F)) : TopCat) : Type v))
this :
  IsIso (C := TopCat.Presheaf.{v, v, u} C (↑(Functor.obj forgetToPresheafedSpace (colimit F)) : TopCat)) (Y :=
    Functor.obj
      (TopCat.Presheaf.pushforward C
          (PresheafedSpace.Hom.base (Iso.inv (preservesColimitIso forgetToPresheafedSpace F))) :
        TopCat.Presheaf.{v, v, u} C (↑(colimit (F ⋙ forgetToPresheafedSpace)) : TopCat) ⥤
          TopCat.Presheaf.{v, v, u} C (↑(Functor.obj forgetToPresheafedSpace (colimit F)) : TopCat))
      (colimit (F ⋙ forgetToPresheafedSpace)).presheaf)
    (PresheafedSpace.Hom.c (Iso.inv (preservesColimitIso forgetToPresheafedSpace F)) :
      (Functor.obj forgetToPresheafedSpace (colimit F)).presheaf ⟶
        Functor.obj
          (TopCat.Presheaf.pushforward C
              (PresheafedSpace.Hom.base (Iso.inv (preservesColimitIso forgetToPresheafedSpace F))) :
            TopCat.Presheaf.{v, v, u} C (↑(colimit (F ⋙ forgetToPresheafedSpace)) : TopCat) ⥤
              TopCat.Presheaf.{v, v, u} C (↑(Functor.obj forgetToPresheafedSpace (colimit F)) : TopCat))
          (colimit (F ⋙ forgetToPresheafedSpace)).presheaf)
suffices :
  IsIso (X :=
    limit
      (PresheafedSpace.componentwiseDiagram (F ⋙ forgetToPresheafedSpace)
        (Functor.obj
            (Opens.map (PresheafedSpace.Hom.base (Iso.inv (preservesColimitIso forgetToPresheafedSpace F))) :
              Opens (↑(↑(Functor.obj forgetToPresheafedSpace (colimit F)) : TopCat) : Type v) ⥤
                Opens (↑(↑(colimit (F ⋙ forgetToPresheafedSpace)) : TopCat) : Type v))
            (H.functor.obj U) :
          Opens (↑(↑(colimit (F ⋙ forgetToPresheafedSpace)) : TopCat) : Type v))))
    (Y :=
    (PresheafedSpace.componentwiseDiagram (F ⋙ forgetToPresheafedSpace)
          (Functor.obj
              (Opens.map (PresheafedSpace.Hom.base (Iso.inv (preservesColimitIso forgetToPresheafedSpace F))) :
                Opens (↑(↑(Functor.obj forgetToPresheafedSpace (colimit F)) : TopCat) : Type v) ⥤
                  Opens (↑(↑(colimit (F ⋙ forgetToPresheafedSpace)) : TopCat) : Type v))
              (H.functor.obj U) :
            Opens (↑(↑(colimit (F ⋙ forgetToPresheafedSpace)) : TopCat) : Type v))).obj
      (op i))
    (limit.π
      (PresheafedSpace.componentwiseDiagram (F ⋙ forgetToPresheafedSpace)
        (Functor.obj
            (Opens.map (PresheafedSpace.Hom.base (Iso.inv (preservesColimitIso forgetToPresheafedSpace F))) :
              Opens (↑(↑(Functor.obj forgetToPresheafedSpace (colimit F)) : TopCat) : Type v) ⥤
                Opens (↑(↑(colimit (F ⋙ forgetToPresheafedSpace)) : TopCat) : Type v))
            (H.functor.obj U) :
          Opens (↑(↑(colimit (F ⋙ forgetToPresheafedSpace)) : TopCat) : Type v)))
      (op i))
⊢ IsIso (Y :=
    Functor.obj
      (Functor.obj
        (TopCat.Presheaf.pushforward C
          (PresheafedSpace.Hom.base
            (CategoryStruct.comp (Y := colimit (F ⋙ forgetToPresheafedSpace))
              (colimit.ι (F ⋙ forgetToPresheafedSpace) i :
                (F ⋙ forgetToPresheafedSpace).obj i ⟶ colimit (F ⋙ forgetToPresheafedSpace))
              (Iso.inv (preservesColimitIso forgetToPresheafedSpace F) :
                colimit (F ⋙ forgetToPresheafedSpace) ⟶ Functor.obj forgetToPresheafedSpace (colimit F)))))
        ((F ⋙ forgetToPresheafedSpace).obj i).presheaf)
      (op (H.functor.obj U)))
    (CategoryStruct.comp (Y :=
      Functor.obj
        (Functor.obj
          (TopCat.Presheaf.pushforward C
              (PresheafedSpace.Hom.base (Iso.inv (preservesColimitIso forgetToPresheafedSpace F))) :
            TopCat.Presheaf.{v, v, u} C (↑(colimit (F ⋙ forgetToPresheafedSpace)) : TopCat) ⥤
              TopCat.Presheaf.{v, v, u} C (↑(Functor.obj forgetToPresheafedSpace (colimit F)) : TopCat))
          (colimit (F ⋙ forgetToPresheafedSpace)).presheaf)
        (op (H.functor.obj U)))
      (NatTrans.app (PresheafedSpace.Hom.c (Iso.inv (preservesColimitIso forgetToPresheafedSpace F)))
          (op (H.functor.obj U)) :
        (Functor.obj forgetToPresheafedSpace (colimit F)).presheaf.obj (op (H.functor.obj U)) ⟶
          Functor.obj
            (Functor.obj
              (TopCat.Presheaf.pushforward C
                  (PresheafedSpace.Hom.base (Iso.inv (preservesColimitIso forgetToPresheafedSpace F))) :
                TopCat.Presheaf.{v, v, u} C (↑(colimit (F ⋙ forgetToPresheafedSpace)) : TopCat) ⥤
                  TopCat.Presheaf.{v, v, u} C (↑(Functor.obj forgetToPresheafedSpace (colimit F)) : TopCat))
              (colimit (F ⋙ forgetToPresheafedSpace)).presheaf)
            (op (H.functor.obj U)))
      (CategoryStruct.comp (Y :=
          limit
            (PresheafedSpace.componentwiseDiagram (F ⋙ forgetToPresheafedSpace)
              (Functor.obj
                  (Opens.map (PresheafedSpace.Hom.base (Iso.inv (preservesColimitIso forgetToPresheafedSpace F))) :
                    Opens (↑(↑(Functor.obj forgetToPresheafedSpace (colimit F)) : TopCat) : Type v) ⥤
                      Opens (↑(↑(colimit (F ⋙ forgetToPresheafedSpace)) : TopCat) : Type v))
                  (unop (op (H.functor.obj U))) :
                Opens (↑(↑(colimit (F ⋙ forgetToPresheafedSpace)) : TopCat) : Type v))))
          (Iso.hom
              (PresheafedSpace.colimitPresheafObjIsoComponentwiseLimit (F ⋙ forgetToPresheafedSpace)
                (Functor.obj
                  (Opens.map (PresheafedSpace.Hom.base (Iso.inv (preservesColimitIso forgetToPresheafedSpace F))) :
                    Opens (↑(↑(Functor.obj forgetToPresheafedSpace (colimit F)) : TopCat) : Type v) ⥤
                      Opens (↑(↑(colimit (F ⋙ forgetToPresheafedSpace)) : TopCat) : Type v))
                  (unop (op (H.functor.obj U))))) :
            (colimit (F ⋙ forgetToPresheafedSpace)).presheaf.obj
                (op
                  (Functor.obj
                    (Opens.map (PresheafedSpace.Hom.base (Iso.inv (preservesColimitIso forgetToPresheafedSpace F))) :
                      Opens (↑(↑(Functor.obj forgetToPresheafedSpace (colimit F)) : TopCat) : Type v) ⥤
                        Opens (↑(↑(colimit (F ⋙ forgetToPresheafedSpace)) : TopCat) : Type v))
                    (unop (op (H.functor.obj U))))) ⟶
              limit
                (PresheafedSpace.componentwiseDiagram (F ⋙ forgetToPresheafedSpace)
                  (Functor.obj
                      (Opens.map (PresheafedSpace.Hom.base (Iso.inv (preservesColimitIso forgetToPresheafedSpace F))) :
                        Opens (↑(↑(Functor.obj forgetToPresheafedSpace (colimit F)) : TopCat) : Type v) ⥤
                          Opens (↑(↑(colimit (F ⋙ forgetToPresheafedSpace)) : TopCat) : Type v))
                      (unop (op (H.functor.obj U))) :
                    Opens (↑(↑(colimit (F ⋙ forgetToPresheafedSpace)) : TopCat) : Type v))))
          (limit.π
              (PresheafedSpace.componentwiseDiagram (F ⋙ forgetToPresheafedSpace)
                (Functor.obj
                    (Opens.map (PresheafedSpace.Hom.base (Iso.inv (preservesColimitIso forgetToPresheafedSpace F))) :
                      Opens (↑(↑(Functor.obj forgetToPresheafedSpace (colimit F)) : TopCat) : Type v) ⥤
                        Opens (↑(↑(colimit (F ⋙ forgetToPresheafedSpace)) : TopCat) : Type v))
                    (unop (op (H.functor.obj U))) :
                  Opens (↑(↑(colimit (F ⋙ forgetToPresheafedSpace)) : TopCat) : Type v)))
              (op i) :
            limit
                (PresheafedSpace.componentwiseDiagram (F ⋙ forgetToPresheafedSpace)
                  (Functor.obj
                      (Opens.map (PresheafedSpace.Hom.base (Iso.inv (preservesColimitIso forgetToPresheafedSpace F))) :
                        Opens (↑(↑(Functor.obj forgetToPresheafedSpace (colimit F)) : TopCat) : Type v) ⥤
                          Opens (↑(↑(colimit (F ⋙ forgetToPresheafedSpace)) : TopCat) : Type v))
                      (unop (op (H.functor.obj U))) :
                    Opens (↑(↑(colimit (F ⋙ forgetToPresheafedSpace)) : TopCat) : Type v))) ⟶
              (PresheafedSpace.componentwiseDiagram (F ⋙ forgetToPresheafedSpace)
                    (Functor.obj
                        (Opens.map
                            (PresheafedSpace.Hom.base (Iso.inv (preservesColimitIso forgetToPresheafedSpace F))) :
                          Opens (↑(↑(Functor.obj forgetToPresheafedSpace (colimit F)) : TopCat) : Type v) ⥤
                            Opens (↑(↑(colimit (F ⋙ forgetToPresheafedSpace)) : TopCat) : Type v))
                        (unop (op (H.functor.obj U))) :
                      Opens (↑(↑(colimit (F ⋙ forgetToPresheafedSpace)) : TopCat) : Type v))).obj
                (op i)) :
        (colimit (F ⋙ forgetToPresheafedSpace)).presheaf.obj
            (op
              (Functor.obj
                (Opens.map (PresheafedSpace.Hom.base (Iso.inv (preservesColimitIso forgetToPresheafedSpace F))) :
                  Opens (↑(↑(Functor.obj forgetToPresheafedSpace (colimit F)) : TopCat) : Type v) ⥤
                    Opens (↑(↑(colimit (F ⋙ forgetToPresheafedSpace)) : TopCat) : Type v))
                (unop (op (H.functor.obj U))))) ⟶
          (PresheafedSpace.componentwiseDiagram (F ⋙ forgetToPresheafedSpace)
                (Functor.obj
                    (Opens.map (PresheafedSpace.Hom.base (Iso.inv (preservesColimitIso forgetToPresheafedSpace F))) :
                      Opens (↑(↑(Functor.obj forgetToPresheafedSpace (colimit F)) : TopCat) : Type v) ⥤
                        Opens (↑(↑(colimit (F ⋙ forgetToPresheafedSpace)) : TopCat) : Type v))
                    (unop (op (H.functor.obj U))) :
                  Opens (↑(↑(colimit (F ⋙ forgetToPresheafedSpace)) : TopCat) : Type v))).obj
            (op i)))

Tactic:
suffices IsIso (limit.π (PresheafedSpace.componentwiseDiagram
      (F ⋙ SheafedSpace.forgetToPresheafedSpace) ((Opens.map
        (preservesColimitIso SheafedSpace.forgetToPresheafedSpace F).inv.base).obj
          (H.functor.obj U))) (op i)) from inferInstance