-- Mathlib/Geometry/RingedSpace/PresheafedSpace/Gluing.lean
theorem π_ιInvApp_π (i j : D.J) (U : Opens (D.U i).carrier) :
    D.diagramOverOpenπ U i ≫ D.ιInvAppπEqMap U ≫ D.ιInvApp U ≫ D.diagramOverOpenπ U j =
      D.diagramOverOpenπ U j

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i j : D.J
U : Opens ↑↑(D.U i)
⊢ D.diagramOverOpenπ U i ≫ D.ιInvAppπEqMap U ≫ D.ιInvApp U ≫ D.diagramOverOpenπ U j = D.diagramOverOpenπ U j

Tactic:
rw [← @cancel_mono
        (f := (componentwiseDiagram 𝖣.diagram.multispan _).map
          (Quiver.Hom.op (WalkingMultispan.Hom.snd (i, j))) ≫ 𝟙 _) ..]

Result:
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i j : D.J
U : Opens ↑↑(D.U i)
⊢ (D.diagramOverOpenπ U i ≫ D.ιInvAppπEqMap U ≫ D.ιInvApp U ≫ D.diagramOverOpenπ U j) ≫
      (componentwiseDiagram D.diagram.multispan (⋯.functor.obj U)).map
          (Quiver.Hom.op (WalkingMultispan.Hom.snd (i, j))) ≫
        𝟙 ((componentwiseDiagram D.diagram.multispan (⋯.functor.obj U)).obj (op (WalkingMultispan.left (i, j)))) =
    D.diagramOverOpenπ U j ≫
      (componentwiseDiagram D.diagram.multispan (⋯.functor.obj U)).map
          (Quiver.Hom.op (WalkingMultispan.Hom.snd (i, j))) ≫
        𝟙 ((componentwiseDiagram D.diagram.multispan (⋯.functor.obj U)).obj (op (WalkingMultispan.left (i, j))))

C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i j : D.J
U : Opens ↑↑(D.U i)
⊢ Mono
    ((componentwiseDiagram D.diagram.multispan (⋯.functor.obj U)).map
        (Quiver.Hom.op (WalkingMultispan.Hom.snd (i, j))) ≫
      𝟙 ((componentwiseDiagram D.diagram.multispan (⋯.functor.obj U)).obj (op (WalkingMultispan.left (i, j)))))

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i j : D.J
U : Opens ↑↑(D.U i)
⊢ D.diagramOverOpenπ U i ≫
      (D.U i).presheaf.map
          ((((eqToIso ⋯).inv ≫ (homOfLE ⋯).op) ≫
              (opensFunctor (D.f i i)).op.map (𝟙 ((Opens.map (D.f i i).base).op.obj (op U)) ≫ eqToHom ⋯)) ≫
            (eqToHom ⋯).op) ≫
        (D.f i j).c.app (op ((Opens.map (D.ι i).base).obj (⋯.functor.obj U))) ≫ (D.V (i, j)).presheaf.map (eqToHom ⋯) =
    limit.π (D.diagramOverOpen U) (op (WalkingMultispan.left (i, j)))

Tactic:
rw [NatTrans.naturality_assoc]

Result:
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i j : D.J
U : Opens ↑↑(D.U i)
⊢ D.diagramOverOpenπ U i ≫
      (D.f i j).c.app
          (op
            ((Opens.map (colimit.ι D.diagram.multispan (unop (op (WalkingMultispan.right i)))).base).obj
              (⋯.functor.obj U))) ≫
        ((TopCat.Presheaf.pushforward C (D.f i j).base).obj (D.V (i, j)).presheaf).map
            ((((eqToIso ⋯).inv ≫ (homOfLE ⋯).op) ≫
                (opensFunctor (D.f i i)).op.map (𝟙 ((Opens.map (D.f i i).base).op.obj (op U)) ≫ eqToHom ⋯)) ≫
              (eqToHom ⋯).op) ≫
          (D.V (i, j)).presheaf.map (eqToHom ⋯) =
    limit.π (D.diagramOverOpen U) (op (WalkingMultispan.left (i, j)))

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i j : D.J
U : Opens ↑↑(D.U i)
⊢ D.diagramOverOpenπ U i ≫
      D.ιInvAppπEqMap U ≫
        D.ιInvApp U ≫
          D.diagramOverOpenπ U j ≫
            (componentwiseDiagram D.diagram.multispan (⋯.functor.obj U)).map
                (Quiver.Hom.op (WalkingMultispan.Hom.snd (i, j))) ≫
              𝟙 ((componentwiseDiagram D.diagram.multispan (⋯.functor.obj U)).obj (op (WalkingMultispan.left (i, j)))) =
    D.diagramOverOpenπ U j ≫
      (componentwiseDiagram D.diagram.multispan (⋯.functor.obj U)).map
          (Quiver.Hom.op (WalkingMultispan.Hom.snd (i, j))) ≫
        𝟙 ((componentwiseDiagram D.diagram.multispan (⋯.functor.obj U)).obj (op (WalkingMultispan.left (i, j))))

Tactic:
rw [limit.w_assoc]

Result:
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i j : D.J
U : Opens ↑↑(D.U i)
⊢ D.diagramOverOpenπ U i ≫
      D.ιInvAppπEqMap U ≫
        D.ιInvApp U ≫
          limit.π (D.diagramOverOpen U) (op (WalkingMultispan.left (i, j))) ≫
            𝟙 ((componentwiseDiagram D.diagram.multispan (⋯.functor.obj U)).obj (op (WalkingMultispan.left (i, j)))) =
    limit.π (D.diagramOverOpen U) (op (WalkingMultispan.left (i, j))) ≫
      𝟙 ((componentwiseDiagram D.diagram.multispan (⋯.functor.obj U)).obj (op (WalkingMultispan.left (i, j))))

Proof state:
case inst
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i j : D.J
U : Opens ↑↑(D.U i)
⊢ Mono
    ((D.f j i).c.app
        (op
          ((Opens.map
                (colimit.ι D.diagram.multispan
                    (unop (op (WalkingMultispan.right ((MultispanShape.prod D.J).snd (i, j)))))).base).obj
            (⋯.functor.obj U))) ≫
      (D.t i j).c.app
        (op
          ((Opens.map (D.f j i).base).obj
            (unop
              (op
                ((Opens.map
                      (colimit.ι D.diagram.multispan
                          (unop (op (WalkingMultispan.right ((MultispanShape.prod D.J).snd (i, j)))))).base).obj
                  (⋯.functor.obj U)))))))

Tactic:
apply (config := { allowSynthFailures := true }) mono_comp

Result:
case inst
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i j : D.J
U : Opens ↑↑(D.U i)
⊢ Mono
    ((D.f j i).c.app
      (op
        ((Opens.map
              (colimit.ι D.diagram.multispan
                  (unop (op (WalkingMultispan.right ((MultispanShape.prod D.J).snd (i, j)))))).base).obj
          (⋯.functor.obj U))))

case inst
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i j : D.J
U : Opens ↑↑(D.U i)
⊢ Mono
    ((D.t i j).c.app
      (op
        ((Opens.map (D.f j i).base).obj
          (unop
            (op
              ((Opens.map
                    (colimit.ι D.diagram.multispan
                        (unop (op (WalkingMultispan.right ((MultispanShape.prod D.J).snd (i, j)))))).base).obj
                (⋯.functor.obj U)))))))

Proof state:
case inst
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i j : D.J
U : Opens ↑↑(D.U i)
⊢ Mono
    ((D.diagram.multispan.map (Quiver.Hom.op (WalkingMultispan.Hom.snd (i, j))).unop).c.app
      (op
        ((Opens.map
              (colimit.ι D.diagram.multispan
                  (unop (op (WalkingMultispan.right ((MultispanShape.prod D.J).snd (i, j)))))).base).obj
          (⋯.functor.obj U))))

Tactic:
change Mono ((_ ≫ D.f j i).c.app _)

Result:
case inst
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i j : D.J
U : Opens ↑↑(D.U i)
⊢ Mono
    ((D.t i j ≫ D.f j i).c.app
      (op
        ((Opens.map
              (colimit.ι D.diagram.multispan
                  (unop (op (WalkingMultispan.right ((MultispanShape.prod D.J).snd (i, j)))))).base).obj
          (⋯.functor.obj U))))

Proof state:
case inst
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i j : D.J
U : Opens ↑↑(D.U i)
⊢ Mono
    ((D.f j i).c.app
      (op ((opensFunctor (D.f j i)).obj ((Opens.map (D.t j i).base).obj ((Opens.map (D.f i j).base).obj U)))))

Tactic:
infer_instance

Result:
no goals

Proof state:
case inst
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i j : D.J
U : Opens ↑↑(D.U i)
this : IsIso (D.t i j).c
⊢ Mono
    ((D.t i j).c.app
      (op
        ((Opens.map (D.f j i).base).obj
          (unop
            (op
              ((Opens.map
                    (colimit.ι D.diagram.multispan
                        (unop (op (WalkingMultispan.right ((MultispanShape.prod D.J).snd (i, j)))))).base).obj
                (⋯.functor.obj U)))))))

Tactic:
infer_instance

Result:
no goals