-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
Goal:
C : Type u
inst_1 : Category.{v, u} C
D : GlueData.{v, u} C
inst_2 : HasLimits.{v, u} C
i j : D.J
U : Opens (↑(↑(D.U i) : TopCat) : Type v)
inst :
  Mono (X :=
    (D.U j).presheaf.obj
      (op
        (Functor.obj (C := Opens (↑(↑(Limits.colimit D.diagram.multispan) : TopCat) : Type v))
          (Opens.map
              (Hom.base
                (colimit.ι D.diagram.multispan
                  (unop (op (WalkingMultispan.right ((MultispanShape.prod D.J).snd (i, j))))))) :
            Opens (↑(↑(Limits.colimit D.diagram.multispan) : TopCat) : Type v) ⥤
              Opens
                (↑(↑(D.diagram.multispan.obj
                          (unop (op (WalkingMultispan.right ((MultispanShape.prod D.J).snd (i, j)))))) :
                      TopCat) :
                  Type v))
          (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)))))
    ((D.t i j ≫ D.f j i).c.app
      (op
        (Functor.obj (C := Opens (↑(↑(Limits.colimit D.diagram.multispan) : TopCat) : Type v))
          (Opens.map
              (Hom.base
                (colimit.ι D.diagram.multispan
                  (unop (op (WalkingMultispan.right ((MultispanShape.prod D.J).snd (i, j))))))) :
            Opens (↑(↑(Limits.colimit D.diagram.multispan) : TopCat) : Type v) ⥤
              Opens
                (↑(↑(D.diagram.multispan.obj
                          (unop (op (WalkingMultispan.right ((MultispanShape.prod D.J).snd (i, j)))))) :
                      TopCat) :
                  Type v))
          (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)))))
⊢ Mono (X :=
    (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 ((MultispanShape.prod D.J).snd (i, j)))))
    (Y :=
    Functor.obj (C :=
      (Opens
          (↑(↑(D.diagram.multispan.obj (unop (op (WalkingMultispan.right ((MultispanShape.prod D.J).snd (i, j)))))) :
                TopCat) :
            Type v))ᵒᵖ)
      (Functor.obj
        (TopCat.Presheaf.pushforward C
          (Hom.base (D.diagram.multispan.map (Quiver.Hom.unop (Quiver.Hom.op (WalkingMultispan.Hom.snd (i, j)))))))
        (D.diagram.multispan.obj (unop (op (WalkingMultispan.left (i, j))))).presheaf)
      (op
        (Functor.obj (C := Opens (↑(↑(Limits.colimit D.diagram.multispan) : TopCat) : Type v))
          (Opens.map
              (Hom.base
                (colimit.ι D.diagram.multispan
                  (unop (op (WalkingMultispan.right ((MultispanShape.prod D.J).snd (i, j))))))) :
            Opens (↑(↑(Limits.colimit D.diagram.multispan) : TopCat) : Type v) ⥤
              Opens
                (↑(↑(D.diagram.multispan.obj
                          (unop (op (WalkingMultispan.right ((MultispanShape.prod D.J).snd (i, j)))))) :
                      TopCat) :
                  Type v))
          (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.diagram.multispan.map (Quiver.Hom.unop (Quiver.Hom.op (WalkingMultispan.Hom.snd (i, j))))))
      (op
        (Functor.obj (C := Opens (↑(↑(Limits.colimit D.diagram.multispan) : TopCat) : Type v))
          (Opens.map
              (Hom.base
                (colimit.ι D.diagram.multispan
                  (unop (op (WalkingMultispan.right ((MultispanShape.prod D.J).snd (i, j))))))) :
            Opens (↑(↑(Limits.colimit D.diagram.multispan) : TopCat) : Type v) ⥤
              Opens
                (↑(↑(D.diagram.multispan.obj
                          (unop (op (WalkingMultispan.right ((MultispanShape.prod D.J).snd (i, j)))))) :
                      TopCat) :
                  Type v))
          (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:
change Mono ((_ ≫ D.f j i).c.app _)

Premises used: CategoryTheory.Mono, CategoryTheory.GlueData.f, CategoryTheory.CategoryStruct.comp, AlgebraicGeometry.PresheafedSpace.Hom.c, CategoryTheory.NatTrans.app, AlgebraicGeometry.PresheafedSpace.GlueData.toGlueData