Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: case e_a
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
j k : D.J
this :
  D.t' j k i ≫ pullback.fst (D.f k i) (D.f k j) ≫ D.t k i ≫ D.f i k =
    (pullbackSymmetry (D.f j k) (D.f j i)).hom ≫ pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j
⊢ (D.V (j, k)).presheaf.map (eqToHom ⋯) ≫ (D.V (j, k)).presheaf.map (eqToHom ⋯) =
    (pullback.fst (D.f j k) (D.f j i)).c.app
        (op
          ((opensFunctor (pullback.snd (D.f j i) (D.f j k))).obj
            ((Opens.map (pullback.fst (D.f j i) (D.f j k)).base).obj
              ((Opens.map (D.t j i).base).obj ((Opens.map (D.f i j).base).obj U))))) ≫
      (pullback (D.f j k) (D.f j i)).presheaf.map (eqToHom ⋯) ≫
        invApp (pullback.fst (D.f j k) (D.f j i))
            (unop
              (op
                ((Opens.map (pullbackSymmetry (D.f j k) (D.f j i)).hom.base).obj
                  ((Opens.map (pullback.snd (D.f j i) (D.f j k)).base).obj
                    ((opensFunctor (pullback.snd (D.f j i) (D.f j k))).obj
                      ((Opens.map (pullback.fst (D.f j i) (D.f j k)).base).obj
                        ((Opens.map (D.t j i).base).obj ((Opens.map (D.f i j).base).obj U)))))))) ≫
          (D.V (j, k)).presheaf.map
              ((opensFunctor (pullback.fst (D.f j k) (D.f j i))).op.map
                ((Opens.map (pullbackSymmetry (D.f j k) (D.f j i)).hom.base).map (eqToHom ⋯).unop).op) ≫
            (D.V (j, k)).presheaf.map ((opensFunctor (pullback.fst (D.f j k) (D.f j i))).op.map (eqToHom ⋯)) ≫
              (D.V (j, k)).presheaf.map (eqToHom ⋯) ≫
                (D.V (j, k)).presheaf.map ((Opens.map (D.t j k).base).map (eqToHom ⋯).unop).op ≫
                  (D.V (j, k)).presheaf.map (eqToHom ⋯)

Tactic:
IsOpenImmersion.inv_naturality_assoc,

Goal state after:
case e_a
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
j k : D.J
this :
  D.t' j k i ≫ pullback.fst (D.f k i) (D.f k j) ≫ D.t k i ≫ D.f i k =
    (pullbackSymmetry (D.f j k) (D.f j i)).hom ≫ pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j
⊢ (D.V (j, k)).presheaf.map (eqToHom ⋯) ≫ (D.V (j, k)).presheaf.map (eqToHom ⋯) =
    (pullback.fst (D.f j k) (D.f j i)).c.app
        (op
          ((opensFunctor (pullback.snd (D.f j i) (D.f j k))).obj
            ((Opens.map (pullback.fst (D.f j i) (D.f j k)).base).obj
              ((Opens.map (D.t j i).base).obj ((Opens.map (D.f i j).base).obj U))))) ≫
      invApp (pullback.fst (D.f j k) (D.f j i))
          (unop
            (op
              ((Opens.map (pullback.fst (D.f j k) (D.f j i)).base).obj
                ((opensFunctor (pullback.snd (D.f j i) (D.f j k))).obj
                  ((Opens.map (pullback.fst (D.f j i) (D.f j k)).base).obj
                    ((Opens.map (D.t j i).base).obj ((Opens.map (D.f i j).base).obj U))))))) ≫
        (D.V (j, k)).presheaf.map ((opensFunctor (pullback.fst (D.f j k) (D.f j i))).op.map (eqToHom ⋯)) ≫
          (D.V (j, k)).presheaf.map
              ((opensFunctor (pullback.fst (D.f j k) (D.f j i))).op.map
                ((Opens.map (pullbackSymmetry (D.f j k) (D.f j i)).hom.base).map (eqToHom ⋯).unop).op) ≫
            (D.V (j, k)).presheaf.map ((opensFunctor (pullback.fst (D.f j k) (D.f j i))).op.map (eqToHom ⋯)) ≫
              (D.V (j, k)).presheaf.map (eqToHom ⋯) ≫
                (D.V (j, k)).presheaf.map ((Opens.map (D.t j k).base).map (eqToHom ⋯).unop).op ≫
                  (D.V (j, k)).presheaf.map (eqToHom ⋯)