-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing (goal)
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)
⊢ 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))ᵒᵖ))
have erw : IsIso (X :=
  D.glued.presheaf.obj
    (op
      (Functor.obj
        (IsOpenEmbedding.functor (f := Hom.base (D.ι i)) sorry :
          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)) sorry :
            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)) sorry :
                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)) sorry :
                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)) sorry :
                  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)) sorry :
                    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)) sorry :
                  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)) sorry :
                    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)) sorry :
                      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)) sorry :
              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)) sorry :
                  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)))
Tactic: erw [← colimitPresheafObjIsoComponentwiseLimit_hom_π]