-- 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.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)))))
inst₁ :
  Mono (X :=
    (Functor.obj (TopCat.Presheaf.pushforward C (D.f j i).base) (D.V (j, i)).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).c.app
      (op
        ((Opens.map (D.f j i).base).obj
          (unop
            (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 :=
    (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.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)))) ≫
      (D.t i j).c.app
        (op
          ((Opens.map (D.f j i).base).obj
            (unop
              (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:
apply +allowSynthFailures mono_comp

Premises used: CategoryTheory.mono_comp