-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
Goal:
C : Type u
inst : Category.{v, u} C
D : GlueData.{v, u} C
inst_1 : HasLimits.{v, u} C
i : D.J
U : Opens (↑(↑(D.U i) : TopCat) : Type v)
erw :
  IsIso (X :=
    D.glued.presheaf.obj
      (op
        (Functor.obj
          (IsOpenEmbedding.functor (f := Hom.base (D.ι i)) ⋯ :
            Opens (↑(↑(D.U i) : TopCat) : Type v) ⥤ Opens (↑(↑D.glued : TopCat) : Type v))
          U)))
    (Y :=
    Functor.obj (C := (Opens (↑(↑D.glued : TopCat) : Type v))ᵒᵖ)
      (Functor.obj (TopCat.Presheaf.pushforward C (Hom.base (D.ι i))) (D.U i).presheaf :
        TopCat.Presheaf.{v, v, u} C (↑D.glued : TopCat))
      (op
          (Functor.obj
            (IsOpenEmbedding.functor (f := Hom.base (D.ι i)) ⋯ :
              Opens (↑(↑(D.U i) : TopCat) : Type v) ⥤ Opens (↑(↑D.glued : TopCat) : Type v))
            U) :
        (Opens (↑(↑D.glued : TopCat) : Type v))ᵒᵖ))
    (CategoryStruct.comp (Y :=
        limit
          (componentwiseDiagram D.diagram.multispan
            (Functor.obj
                (IsOpenEmbedding.functor (f := Hom.base (D.ι i)) ⋯ :
                  Opens (↑(↑(D.U i) : TopCat) : Type v) ⥤ Opens (↑(↑D.glued : TopCat) : Type v))
                U :
              Opens (↑(↑D.glued : TopCat) : Type v))))
        (Iso.hom
            (colimitPresheafObjIsoComponentwiseLimit D.diagram.multispan
              (Functor.obj
                (IsOpenEmbedding.functor (f := Hom.base (D.ι i)) ⋯ :
                  Opens (↑(↑(D.U i) : TopCat) : Type v) ⥤ Opens (↑(↑D.glued : TopCat) : Type v))
                U)) :
          (Limits.colimit D.diagram.multispan).presheaf.obj
              (op
                (Functor.obj
                  (IsOpenEmbedding.functor (f := Hom.base (D.ι i)) ⋯ :
                    Opens (↑(↑(D.U i) : TopCat) : Type v) ⥤ Opens (↑(↑D.glued : TopCat) : Type v))
                  U)) ⟶
            limit
              (componentwiseDiagram D.diagram.multispan
                (Functor.obj
                    (IsOpenEmbedding.functor (f := Hom.base (D.ι i)) ⋯ :
                      Opens (↑(↑(D.U i) : TopCat) : Type v) ⥤ Opens (↑(↑D.glued : TopCat) : Type v))
                    U :
                  Opens (↑(↑D.glued : TopCat) : Type v))))
        (limit.π
            (componentwiseDiagram D.diagram.multispan
              (Functor.obj
                  (IsOpenEmbedding.functor (f := Hom.base (D.ι i)) ⋯ :
                    Opens (↑(↑(D.U i) : TopCat) : Type v) ⥤ Opens (↑(↑D.glued : TopCat) : Type v))
                  U :
                Opens (↑(↑D.glued : TopCat) : Type v)))
            (op (WalkingMultispan.right i)) :
          limit
              (componentwiseDiagram D.diagram.multispan
                (Functor.obj
                    (IsOpenEmbedding.functor (f := Hom.base (D.ι i)) ⋯ :
                      Opens (↑(↑(D.U i) : TopCat) : Type v) ⥤ Opens (↑(↑D.glued : TopCat) : Type v))
                    U :
                  Opens (↑(↑D.glued : TopCat) : Type v))) ⟶
            (componentwiseDiagram D.diagram.multispan
                  (Functor.obj
                      (IsOpenEmbedding.functor (f := Hom.base (D.ι i)) ⋯ :
                        Opens (↑(↑(D.U i) : TopCat) : Type v) ⥤ Opens (↑(↑D.glued : TopCat) : Type v))
                      U :
                    Opens (↑(↑D.glued : TopCat) : Type v))).obj
              (op (WalkingMultispan.right i))) :
      (Limits.colimit D.diagram.multispan).presheaf.obj
          (op
            (Functor.obj
              (IsOpenEmbedding.functor (f := Hom.base (D.ι i)) ⋯ :
                Opens (↑(↑(D.U i) : TopCat) : Type v) ⥤ Opens (↑(↑D.glued : TopCat) : Type v))
              U)) ⟶
        (componentwiseDiagram D.diagram.multispan
              (Functor.obj
                  (IsOpenEmbedding.functor (f := Hom.base (D.ι i)) ⋯ :
                    Opens (↑(↑(D.U i) : TopCat) : Type v) ⥤ Opens (↑(↑D.glued : TopCat) : Type v))
                  U :
                Opens (↑(↑D.glued : TopCat) : Type v))).obj
          (op (WalkingMultispan.right i)))
⊢ IsIso (X :=
    D.glued.presheaf.obj
      (op
        (Functor.obj
          (IsOpenEmbedding.functor (f := Hom.base (D.ι i)) ⋯ :
            Opens (↑(↑(D.U i) : TopCat) : Type v) ⥤ Opens (↑(↑D.glued : TopCat) : Type v))
          U)))
    (Y :=
    Functor.obj (C := (Opens (↑(↑D.glued : TopCat) : Type v))ᵒᵖ)
      (Functor.obj (TopCat.Presheaf.pushforward C (Hom.base (D.ι i))) (D.U i).presheaf :
        TopCat.Presheaf.{v, v, u} C (↑D.glued : TopCat))
      (op
          (Functor.obj
            (IsOpenEmbedding.functor (f := Hom.base (D.ι i)) ⋯ :
              Opens (↑(↑(D.U i) : TopCat) : Type v) ⥤ Opens (↑(↑D.glued : TopCat) : Type v))
            U) :
        (Opens (↑(↑D.glued : TopCat) : Type v))ᵒᵖ))
    (NatTrans.app (Hom.c (D.ι i))
        (op
          (Functor.obj
            (IsOpenEmbedding.functor (f := Hom.base (D.ι i)) ⋯ :
              Opens (↑(↑(D.U i) : TopCat) : Type v) ⥤ Opens (↑(↑D.glued : TopCat) : Type v))
            U)) :
      D.glued.presheaf.obj
          (op
            (Functor.obj
              (IsOpenEmbedding.functor (f := Hom.base (D.ι i)) ⋯ :
                Opens (↑(↑(D.U i) : TopCat) : Type v) ⥤ Opens (↑(↑D.glued : TopCat) : Type v))
              U)) ⟶
        Functor.obj (C := (Opens (↑(↑D.glued : TopCat) : Type v))ᵒᵖ)
          (Functor.obj (TopCat.Presheaf.pushforward C (Hom.base (D.ι i))) (D.U i).presheaf :
            TopCat.Presheaf.{v, v, u} C (↑D.glued : TopCat))
          (op
              (Functor.obj
                (IsOpenEmbedding.functor (f := Hom.base (D.ι i)) ⋯ :
                  Opens (↑(↑(D.U i) : TopCat) : Type v) ⥤ Opens (↑(↑D.glued : TopCat) : Type v))
                U) :
            (Opens (↑(↑D.glued : TopCat) : Type v))ᵒᵖ))

Tactic:
erw [← colimitPresheafObjIsoComponentwiseLimit_hom_π]

Premises used: AlgebraicGeometry.PresheafedSpace.colimitPresheafObjIsoComponentwiseLimit_hom_π