-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
Goal:
C : Type u
inst : Category.{v, u} C
D : GlueData.{v, u} C
i j k : D.J
U : Opens (↑(↑(D.V (i, j)) : TopCat) : Type v)
this :
  ∀ (U : (Opens (↑(↑(D.U i) : TopCat) : Type v))ᵒᵖ),
    (D.f i j).c.app U ≫
        NatTrans.app (Hom.c (pullback.fst (D.f i j) (D.f i k))) (op ((Opens.map (D.f i j).base).obj (unop U))) =
      ((D.f i k).c.app U ≫
          NatTrans.app (Hom.c (pullback.snd (D.f i j) (D.f i k))) (op ((Opens.map (D.f i k).base).obj (unop U)))) ≫
        (pullback (D.f i j) (D.f i k)).presheaf.map (eqToHom ⋯)
erw :
  Eq (α :=
    (D.U i).presheaf.obj (op ((opensFunctor (D.f i j)).obj U)) ⟶
      (Functor.obj (TopCat.Presheaf.pushforward C (D.f i k).base) (D.V (i, k)).presheaf).obj
        (op ((opensFunctor (D.f i j)).obj U)))
    ((D.f i k).c.app (op ((opensFunctor (D.f i j)).obj U)))
    ((D.f i k).c.app (op ((opensFunctor (D.f i j)).obj U)) ≫
      (D.V (i, k)).presheaf.map
        (CategoryStruct.comp (Y :=
          op
            (Functor.obj (C := Opens (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v))
              (opensFunctor (pullback.snd (D.f i j) (D.f i k)))
              (Functor.obj (Opens.map (Hom.base (pullback.snd (D.f i j) (D.f i k))))
                ((Opens.map (D.f i k).base).obj (unop (op ((opensFunctor (D.f i j)).obj U)))))))
          (Quiver.Hom.op (X :=
              Set.image (α := (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v))
                (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC :=
                      TopCat.carrier) (X := (↑(pullback (D.f i j) (D.f i k)) : TopCat))
                      (Hom.base (pullback.snd (D.f i j) (D.f i k)))) :
                  (a : (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)) → (↑(↑(D.V (i, k)) : TopCat) : Type v))
                ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC :=
                        TopCat.carrier) (X := (↑(pullback (D.f i j) (D.f i k)) : TopCat))
                        (Hom.base (pullback.snd (D.f i j) (D.f i k)))) :
                    (a : (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)) →
                      (↑(↑(D.V (i, k)) : TopCat) : Type v)) ⁻¹'
                  ((Opens.map (D.f i k).base).obj (unop (op ((opensFunctor (D.f i j)).obj U)))).carrier))
              (Y := ((Opens.map (D.f i k).base).obj (unop (op ((opensFunctor (D.f i j)).obj U)))).carrier)
              (homOfLE (x :=
                Set.image (α := (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v))
                  (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC :=
                        TopCat.carrier) (X := (↑(pullback (D.f i j) (D.f i k)) : TopCat))
                        (Hom.base (pullback.snd (D.f i j) (D.f i k)))) :
                    (a : (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)) → (↑(↑(D.V (i, k)) : TopCat) : Type v))
                  ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC :=
                          TopCat.carrier) (X := (↑(pullback (D.f i j) (D.f i k)) : TopCat))
                          (Hom.base (pullback.snd (D.f i j) (D.f i k)))) :
                      (a : (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)) →
                        (↑(↑(D.V (i, k)) : TopCat) : Type v)) ⁻¹'
                    ((Opens.map (D.f i k).base).obj (unop (op ((opensFunctor (D.f i j)).obj U)))).carrier))
                (y := ((Opens.map (D.f i k).base).obj (unop (op ((opensFunctor (D.f i j)).obj U)))).carrier) ⋯) :
            op ((Opens.map (D.f i k).base).obj (unop (op ((opensFunctor (D.f i j)).obj U)))).carrier ⟶
              op
                (Set.image (α := (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v))
                  (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC :=
                        TopCat.carrier) (X := (↑(pullback (D.f i j) (D.f i k)) : TopCat))
                        (Hom.base (pullback.snd (D.f i j) (D.f i k)))) :
                    (a : (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)) → (↑(↑(D.V (i, k)) : TopCat) : Type v))
                  ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC :=
                          TopCat.carrier) (X := (↑(pullback (D.f i j) (D.f i k)) : TopCat))
                          (Hom.base (pullback.snd (D.f i j) (D.f i k)))) :
                      (a : (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)) →
                        (↑(↑(D.V (i, k)) : TopCat) : Type v)) ⁻¹'
                    ((Opens.map (D.f i k).base).obj (unop (op ((opensFunctor (D.f i j)).obj U)))).carrier)))
          (CategoryTheory.Functor.map (Functor.op (opensFunctor (pullback.snd (D.f i j) (D.f i k))))
                (eqToHom ⋯ ≫
                  CategoryTheory.Functor.map (Functor.op (Opens.map (Hom.base (pullback.fst (D.f i j) (D.f i k)))))
                    (eqToHom ⋯)) ≫
              eqToHom ⋯ :
            op
                (Functor.obj (C := Opens (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v))
                  (opensFunctor (pullback.snd (D.f i j) (D.f i k)))
                  (unop
                    (Functor.obj (Functor.op (Opens.map (Hom.base (pullback.snd (D.f i j) (D.f i k) ≫ D.f i k))))
                      (op ((opensFunctor (D.f i j)).obj U))))) ⟶
              (Opens.map (D.f i k).base).op.obj (op ((opensFunctor (D.f i j)).obj U)))))
⊢ (D.f i k).c.app (op ((opensFunctor (D.f i j)).obj U)) =
    (D.f i j).c.app (op ((opensFunctor (D.f i j)).obj U)) ≫
      (D.V (i, j)).presheaf.map (eqToHom ⋯) ≫
        NatTrans.app (Hom.c (pullback.fst (D.f i j) (D.f i k))) (op U) ≫
          invApp (pullback.snd (D.f i j) (D.f i k))
              ((Opens.map (Hom.base (pullback.fst (D.f i j) (D.f i k))) :
                    Opens (↑(↑(D.V (i, j)) : TopCat) : Type v) ⥤
                      Opens (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)).1
                U) ≫
            (D.V (i, k)).presheaf.map (eqToHom ⋯)

Tactic:
erw [(π₁ i, j, k).c.naturality_assoc, reassoc_of% this, ← Functor.map_comp_assoc,
    IsOpenImmersion.inv_naturality_assoc, IsOpenImmersion.app_invApp_assoc, ←
    (D.V (i, k)).presheaf.map_comp, ← (D.V (i, k)).presheaf.map_comp]

Premises used: AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.inv_naturality_assoc, Prod.mk, CategoryTheory.Functor.map_comp_assoc, CategoryTheory.GlueData.V, AlgebraicGeometry.PresheafedSpace.presheaf, CategoryTheory.Functor.map_comp, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.app_invApp_assoc, AlgebraicGeometry.PresheafedSpace.GlueData.toGlueData