-- 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.f i i).c.app (op U) ≫
            ((D.V (i, i)).presheaf.map (𝟙 ((Opens.map (D.f i i).base).op.obj (op U))) ≫
                (D.V (i, i)).presheaf.map (eqToHom ⋯)) ≫
              invApp (D.f i i)
                  (unop
                    (op
                      ((Opens.map (D.t i i).base).toPrefunctor.1 (unop ((Opens.map (D.f i i).base).op.obj (op U)))))) ≫
                (D.U i).presheaf.map (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:
simp_rw [Category.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.f i i).c.app (op U) ≫
          (D.V (i, i)).presheaf.map (𝟙 ((Opens.map (D.f i i).base).op.obj (op U))) ≫
            (D.V (i, i)).presheaf.map (eqToHom ⋯) ≫
              invApp (D.f i i)
                  ((Opens.map (D.t i i).base).toPrefunctor.1 (unop ((Opens.map (D.f i i).base).op.obj (op U)))) ≫
                (D.U i).presheaf.map (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)))

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.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))))

Tactic:
rw [comp_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.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)))))))

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.f i j).c.app
          (op
            ((Opens.map (colimit.ι D.diagram.multispan (unop (op (WalkingMultispan.right i)))).base).obj
              (⋯.functor.obj U))) ≫
        (D.V (i, j)).presheaf.map
          ((Opens.map (D.f i j).base).op.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) ≫
            eqToHom ⋯) =
    limit.π (D.diagramOverOpen U) (op (WalkingMultispan.left (i, j)))

Tactic:
convert
  limit.w (componentwiseDiagram 𝖣.diagram.multispan _)
    (Quiver.Hom.op (WalkingMultispan.Hom.fst (i, j)))

Result:
no goals

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:
simp_rw [Category.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 ≫
          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))))

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)
⊢ Mono
    ((componentwiseDiagram D.diagram.multispan (⋯.functor.obj U)).map (Quiver.Hom.op (WalkingMultispan.Hom.snd (i, j))))

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.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))))

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 ≫
        { pt := (D.U i).presheaf.obj (op U), π := { app := fun j => D.ιInvAppπApp U (unop j), naturality := ⋯ } }.π.app
          (op (WalkingMultispan.left (i, j))) =
    limit.π (D.diagramOverOpen U) (op (WalkingMultispan.left (i, j)))

Tactic:
change _ ≫ _ ≫ (_ ≫ _) ≫ _ = _

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.f i i).c.app (op U) ≫
            (D.t i i).c.app ((Opens.map (D.f i i).base).op.obj (op U)) ≫
              invApp (D.f i i)
                  (unop
                    (op
                      ((Opens.map (D.t i i).base).toPrefunctor.1 (unop ((Opens.map (D.f i i).base).op.obj (op U)))))) ≫
                (D.U i).presheaf.map (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)))