-- 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))
suffices :
  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)))
    (NatTrans.app
      (PresheafedSpace.Hom.c
        (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))))
      (op (H.functor.obj U)))
⊢ IsIso (X := (colimit F).presheaf.obj (op (Functor.obj (IsOpenEmbedding.functor ⋯) U))) (Y :=
    Functor.obj (C := (Opens (↑(↑(colimit F).toPresheafedSpace : TopCat) : Type v))ᵒᵖ)
      (Functor.obj (TopCat.Presheaf.pushforward C (PresheafedSpace.Hom.base (InducedCategory.Hom.hom (colimit.ι F i))))
        (F.obj i).presheaf)
      (op (Functor.obj (IsOpenEmbedding.functor ⋯) U)))
    (NatTrans.app (PresheafedSpace.Hom.c (InducedCategory.Hom.hom (colimit.ι F i)))
      (op (Functor.obj (IsOpenEmbedding.functor ⋯) U)))

Tactic:
suffices IsIso <| (colimit.ι (F ⋙ SheafedSpace.forgetToPresheafedSpace) i ≫
        (preservesColimitIso SheafedSpace.forgetToPresheafedSpace F).inv).c.app <|
      op (H.functor.obj U) by
      convert! this