-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
Goal:
C : Type u
inst : Category.{v, u} C
D : GlueData.{v, u} C
inst_1 : HasLimits.{v, u} C
i : D.J
U : Opens (↑(↑(D.U i) : TopCat) : Type v)
h :
  Eq (α :=
    (D.U i).presheaf.obj (op U) ⟶
      (D.U i).presheaf.obj
        (op
          (Functor.obj (C := Opens (↑(↑D.glued : TopCat) : Type v))
            (Opens.map (Hom.base (D.ι i)) :
              Opens (↑(↑D.glued : TopCat) : Type v) ⥤ Opens (↑(↑(D.U i) : TopCat) : Type v))
            (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)))))
    ((D.U i).presheaf.map
          (Quiver.Hom.op (X :=
            Set.image (α := (↑(↑(D.V (i, i)) : TopCat) : Type v))
              (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC :=
                    TopCat.carrier) (D.f i i).base) :
                (a : (↑(↑(D.V (i, i)) : TopCat) : Type v)) → (↑(↑(D.U i) : TopCat) : Type v))
              ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC :=
                      TopCat.carrier) (D.f i i).base) :
                  (a : (↑(↑(D.V (i, i)) : TopCat) : Type v)) → (↑(↑(D.U i) : TopCat) : Type v)) ⁻¹'
                U.carrier))
            (Y := U.carrier)
            (eqToHom (X :=
              Set.image (α := (↑(↑(D.V (i, i)) : TopCat) : Type v))
                (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC :=
                      TopCat.carrier) (D.f i i).base) :
                  (a : (↑(↑(D.V (i, i)) : TopCat) : Type v)) → (↑(↑(D.U i) : TopCat) : Type v))
                ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC :=
                        TopCat.carrier) (D.f i i).base) :
                    (a : (↑(↑(D.V (i, i)) : TopCat) : Type v)) → (↑(↑(D.U i) : TopCat) : Type v)) ⁻¹'
                  U.carrier))
              (Y := U.carrier) ⋯)) ≫
        (D.U i).presheaf.map ((opensFunctor (D.f i i)).op.map (𝟙 (op ((Opens.map (D.f i i).base).obj U)) ≫ eqToHom ⋯)) ≫
          (D.U i).presheaf.map (Quiver.Hom.op (eqToHom ⋯)) :
      (D.U i).presheaf.obj (op U) ⟶
        (D.U i).presheaf.obj
          (op
            (Functor.obj (C := Opens (↑(↑D.glued : TopCat) : Type v))
              (Opens.map (Hom.base (D.ι i)) :
                Opens (↑(↑D.glued : TopCat) : Type v) ⥤ Opens (↑(↑(D.U i) : TopCat) : Type v))
              (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)))))
    ((D.U i).presheaf.map (eqToHom ⋯) :
      (D.U i).presheaf.obj (op U) ⟶
        (D.U i).presheaf.obj
          (op
            (Functor.obj (C := Opens (↑(↑(Limits.colimit D.diagram.multispan) : TopCat) : Type v))
              (Opens.map (Hom.base (Multicoequalizer.π D.diagram i)) :
                Opens (↑(↑(Limits.colimit D.diagram.multispan) : TopCat) : Type v) ⥤
                  Opens (↑(↑(D.U i) : TopCat) : Type v))
              (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)))))
h₁ :
  (↑U : Set (↑(↑(D.U i) : TopCat) : Type v)) ⊆
    Set.range (ι := (↑(↑(D.V (i, i)) : TopCat) : Type v))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC := TopCat.carrier)
            (D.f i i).base) :
        (a : (↑(↑(D.V (i, i)) : TopCat) : Type v)) → (↑(↑(D.U i) : TopCat) : Type v))
⊢ Eq (α :=
    (D.U i).presheaf.obj (op U) ⟶
      (D.U i).presheaf.obj
        (op
          (Functor.obj (C := Opens (↑(↑D.glued : TopCat) : Type v))
            (Opens.map (Hom.base (D.ι i)) :
              Opens (↑(↑D.glued : TopCat) : Type v) ⥤ Opens (↑(↑(D.U i) : TopCat) : Type v))
            (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)))))
    ((D.f i i).c.app (op U) ≫
        (D.V (i, i)).presheaf.map (𝟙 (op ((Opens.map (D.f i i).base).obj U)) ≫ eqToHom ⋯) ≫
          invApp (D.f i i) ((Opens.map (D.t i i).base).1 ((Opens.map (D.f i i).base).obj U)) ≫
            (D.U i).presheaf.map (Quiver.Hom.op (eqToHom ⋯)) :
      (D.U i).presheaf.obj (op U) ⟶
        (D.U i).presheaf.obj
          (op
            (Functor.obj (C := Opens (↑(↑D.glued : TopCat) : Type v))
              (Opens.map (Hom.base (D.ι i)) :
                Opens (↑(↑D.glued : TopCat) : Type v) ⥤ Opens (↑(↑(D.U i) : TopCat) : Type v))
              (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)))))
    ((D.U i).presheaf.map (eqToHom ⋯) :
      (D.U i).presheaf.obj (op U) ⟶
        (D.U i).presheaf.obj
          (op
            (Functor.obj (C := Opens (↑(↑(Limits.colimit D.diagram.multispan) : TopCat) : Type v))
              (Opens.map (Hom.base (Multicoequalizer.π D.diagram i)) :
                Opens (↑(↑(Limits.colimit D.diagram.multispan) : TopCat) : Type v) ⥤
                  Opens (↑(↑(D.U i) : TopCat) : Type v))
              (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)))))

Tactic:
erw [IsOpenImmersion.inv_naturality_assoc, IsOpenImmersion.app_inv_app'_assoc]

Premises used: AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.inv_naturality_assoc, AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.app_inv_app'_assoc