-- 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 (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)
h :
  Eq (α :=
    (D.V (i, k)).presheaf.obj (op (Functor.obj (opensFunctor (pullback.snd (D.f i j) (D.f i k))) U)) ⟶
      (D.V (k, i)).presheaf.obj
        (op
          (Functor.obj (C := Opens (↑(↑(pullback (D.f k i) (D.f k j)) : TopCat) : Type v))
            (opensFunctor (pullback.fst (D.f k i) (D.f k j))) ((Opens.map (D.t' k i j).base).1 U))))
    ((D.t k i).c.app (op (Functor.obj (opensFunctor (pullback.snd (D.f i j) (D.f i k))) U)) ≫
      (D.V (k, i)).presheaf.map (eqToHom ⋯))
    ((D.t k i).c.app (op (Functor.obj (opensFunctor (pullback.snd (D.f i j) (D.f i k))) U)) ≫
      CategoryStruct.comp (Y :=
        (D.V (k, i)).presheaf.obj
          (op
            (Functor.obj (C := Opens (↑(↑(pullback (D.f k i) (D.f k j)) : TopCat) : Type v))
              (opensFunctor (pullback.fst (D.f k i) (D.f k j)))
              (Functor.obj (Opens.map (Hom.base (pullback.fst (D.f k i) (D.f k j))))
                ((Opens.map (D.t k i).base).obj (Functor.obj (opensFunctor (pullback.snd (D.f i j) (D.f i k))) U))))))
        ((D.V (k, i)).presheaf.map
            (Quiver.Hom.op (X :=
              Set.image (α := (↑(↑(pullback (D.f k i) (D.f k j)) : 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 k i) (D.f k j)) : TopCat))
                      (Hom.base (pullback.fst (D.f k i) (D.f k j)))) :
                  (a : (↑(↑(pullback (D.f k i) (D.f k j)) : TopCat) : Type v)) → (↑(↑(D.V (k, i)) : 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 k i) (D.f k j)) : TopCat))
                        (Hom.base (pullback.fst (D.f k i) (D.f k j)))) :
                    (a : (↑(↑(pullback (D.f k i) (D.f k j)) : TopCat) : Type v)) →
                      (↑(↑(D.V (k, i)) : TopCat) : Type v)) ⁻¹'
                  ((Opens.map (D.t k i).base).obj
                      (Functor.obj (opensFunctor (pullback.snd (D.f i j) (D.f i k))) U)).carrier))
              (Y :=
              ((Opens.map (D.t k i).base).obj
                  (Functor.obj (opensFunctor (pullback.snd (D.f i j) (D.f i k))) U)).carrier)
              (eqToHom (X :=
                Set.image (α := (↑(↑(pullback (D.f k i) (D.f k j)) : 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 k i) (D.f k j)) : TopCat))
                        (Hom.base (pullback.fst (D.f k i) (D.f k j)))) :
                    (a : (↑(↑(pullback (D.f k i) (D.f k j)) : TopCat) : Type v)) → (↑(↑(D.V (k, i)) : 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 k i) (D.f k j)) : TopCat))
                          (Hom.base (pullback.fst (D.f k i) (D.f k j)))) :
                      (a : (↑(↑(pullback (D.f k i) (D.f k j)) : TopCat) : Type v)) →
                        (↑(↑(D.V (k, i)) : TopCat) : Type v)) ⁻¹'
                    ((Opens.map (D.t k i).base).obj
                        (Functor.obj (opensFunctor (pullback.snd (D.f i j) (D.f i k))) U)).carrier))
                (Y :=
                ((Opens.map (D.t k i).base).obj
                    (Functor.obj (opensFunctor (pullback.snd (D.f i j) (D.f i k))) U)).carrier)
                ⋯)) :
          (D.V (k, i)).presheaf.obj
              (op ((Opens.map (D.t k i).base).obj (Functor.obj (opensFunctor (pullback.snd (D.f i j) (D.f i k))) U))) ⟶
            (D.V (k, i)).presheaf.obj
              (op
                (Functor.obj (C := Opens (↑(↑(pullback (D.f k i) (D.f k j)) : TopCat) : Type v))
                  (opensFunctor (pullback.fst (D.f k i) (D.f k j)))
                  (Functor.obj (Opens.map (Hom.base (pullback.fst (D.f k i) (D.f k j))))
                    ((Opens.map (D.t k i).base).obj
                      (Functor.obj (opensFunctor (pullback.snd (D.f i j) (D.f i k))) U))))))
        (CategoryStruct.comp (Y :=
            (D.V (k, i)).presheaf.obj
              (op
                (Functor.obj (opensFunctor (pullback.fst (D.f k i) (D.f k j)))
                  (unop
                    (op
                      ((Opens.map (D.t' k i j).base).obj
                        (Functor.obj (Opens.map (Hom.base (pullback.snd (D.f i j) (D.f i k))))
                          (Functor.obj (opensFunctor (pullback.snd (D.f i j) (D.f i k))) U))))))))
            ((D.V (k, i)).presheaf.map
              (CategoryTheory.Functor.map (Functor.op (opensFunctor (pullback.fst (D.f k i) (D.f k j)))) (eqToHom ⋯)))
            ((D.V (k, i)).presheaf.map
              (CategoryTheory.Functor.map (Functor.op (opensFunctor (pullback.fst (D.f k i) (D.f k j))))
                (Quiver.Hom.op ((Opens.map (D.t' k i j).base).map (Quiver.Hom.unop (eqToHom ⋯)))))) :
          (D.V (k, i)).presheaf.obj
              (op
                (Functor.obj (C := Opens (↑(↑(pullback (D.f k i) (D.f k j)) : TopCat) : Type v))
                  (opensFunctor (pullback.fst (D.f k i) (D.f k j)))
                  (unop
                    (op
                      (Functor.obj (Opens.map (Hom.base (pullback.fst (D.f k i) (D.f k j))))
                        ((Opens.map (D.t k i).base).obj
                          (Functor.obj (opensFunctor (pullback.snd (D.f i j) (D.f i k))) U))))))) ⟶
            (D.V (k, i)).presheaf.obj
              (op
                (Functor.obj (C := Opens (↑(↑(pullback (D.f k i) (D.f k j)) : TopCat) : Type v))
                  (opensFunctor (pullback.fst (D.f k i) (D.f k j))) ((Opens.map (D.t' k i j).base).1 U)))))
h₁ :
  (↑((Opens.map (D.t k i).base).obj (Functor.obj (opensFunctor (pullback.snd (D.f i j) (D.f i k))) U)) :
      Set (↑(↑(D.V (k, i)) : TopCat) : Type v)) ⊆
    Set.range (ι := (↑(↑(pullback (D.f k i) (D.f k j)) : 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 k i) (D.f k j)) : TopCat)) (Hom.base (pullback.fst (D.f k i) (D.f k j)))) :
        (a : (↑(↑(pullback (D.f k i) (D.f k j)) : TopCat) : Type v)) → (↑(↑(D.V (k, i)) : TopCat) : Type v))
⊢ Eq (α :=
    (D.V (i, k)).presheaf.obj (op (Functor.obj (opensFunctor (pullback.snd (D.f i j) (D.f i k))) U)) ⟶
      (D.V (k, i)).presheaf.obj
        (op
          (Functor.obj (C := Opens (↑(↑(pullback (D.f k i) (D.f k j)) : TopCat) : Type v))
            (opensFunctor (pullback.fst (D.f k i) (D.f k j))) ((Opens.map (D.t' k i j).base).1 U))))
    ((D.t k i).c.app (op (Functor.obj (opensFunctor (pullback.snd (D.f i j) (D.f i k))) U)) ≫
      (D.V (k, i)).presheaf.map (eqToHom ⋯))
    ((D.t k i).c.app (op (Functor.obj (opensFunctor (pullback.snd (D.f i j) (D.f i k))) U)) ≫
      CategoryStruct.comp (Y :=
        (pullback (D.f k i) (D.f k j)).presheaf.obj
          (op
            (Functor.obj (Opens.map (Hom.base (pullback.fst (D.f k i) (D.f k j))))
              ((Opens.map (D.t k i).base).obj (Functor.obj (opensFunctor (pullback.snd (D.f i j) (D.f i k))) U)))))
        (NatTrans.app (Hom.c (pullback.fst (D.f k i) (D.f k j)))
          (op ((Opens.map (D.t k i).base).obj (Functor.obj (opensFunctor (pullback.snd (D.f i j) (D.f i k))) U))))
        (CategoryStruct.comp (Y :=
          (pullback (D.f k i) (D.f k j)).presheaf.obj
            (op
              ((Opens.map (D.t' k i j).base).obj
                (Functor.obj (Opens.map (Hom.base (pullback.snd (D.f i j) (D.f i k))))
                  (Functor.obj (opensFunctor (pullback.snd (D.f i j) (D.f i k))) U)))))
          ((pullback (D.f k i) (D.f k j)).presheaf.map (eqToHom ⋯) :
            (pullback (D.f k i) (D.f k j)).presheaf.obj
                (op
                  (Functor.obj (Opens.map (Hom.base (pullback.fst (D.f k i) (D.f k j))))
                    ((Opens.map (D.t k i).base).obj
                      (Functor.obj (opensFunctor (pullback.snd (D.f i j) (D.f i k))) U)))) ⟶
              (pullback (D.f k i) (D.f k j)).presheaf.obj
                (op
                  ((Opens.map (D.t' k i j).base).obj
                    (Functor.obj (Opens.map (Hom.base (pullback.snd (D.f i j) (D.f i k))))
                      (Functor.obj (opensFunctor (pullback.snd (D.f i j) (D.f i k))) U)))))
          ((pullback (D.f k i) (D.f k j)).presheaf.map
                (Quiver.Hom.op ((Opens.map (D.t' k i j).base).map (Quiver.Hom.unop (eqToHom ⋯)))) ≫
              invApp (pullback.fst (D.f k i) (D.f k j)) ((Opens.map (D.t' k i j).base).1 U) :
            (pullback (D.f k i) (D.f k j)).presheaf.obj
                (op
                  ((Opens.map (D.t' k i j).base).obj
                    (Functor.obj (Opens.map (Hom.base (pullback.snd (D.f i j) (D.f i k))))
                      (Functor.obj (opensFunctor (pullback.snd (D.f i j) (D.f i k))) U)))) ⟶
              (D.V (k, i)).presheaf.obj
                (op
                  (Functor.obj (C := Opens (↑(↑(pullback (D.f k i) (D.f k j)) : TopCat) : Type v))
                    (opensFunctor (pullback.fst (D.f k i) (D.f k j))) ((Opens.map (D.t' k i j).base).1 U))))))

Tactic:
rw [IsOpenImmersion.inv_naturality, IsOpenImmersion.inv_naturality_assoc,
      IsOpenImmersion.app_inv_app'_assoc]

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