-- 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 j : D.J
U : Opens (↑(↑(D.U i) : 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 :=
    (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.left (i, j))))
    ((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))).map
      (Quiver.Hom.op (WalkingMultispan.Hom.snd (i, j))))
have inst : Mono (X :=
  (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 ((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)) sorry :
              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)) sorry :
              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