-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
J : Type w
inst : Category.{v, w} J
F : CategoryTheory.Functor.{v, u, w, u + 1} J Scheme
inst_1 : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst_2 : (F ⋙ forget).IsLocallyDirected
inst_3 : Quiver.IsThin.{w, v} J
inst_4 : Small.{u, w} J
s : Cocone (F ⋙ forgetToLocallyRingedSpace)
i j : (glueData F).toLocallyRingedSpaceGlueData.J
x :
  (MultispanShape.prod
      (Cover.gluedCover (X :=
            (↑(⨆ (i_1 : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)),
                  Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1)) :
              Scheme))
            (Cover.ulift (P := IsOpenImmersion)
              (Opens.iSupOpenCover fun (i_1 : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)) ↦
                Hom.opensRange
                  (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1)))).toLocallyRingedSpaceGlueData.J).R
k : ↥(F.obj ↓i)
hk :
  Membership.mem (γ := TopologicalSpace.Opens ↥(F.obj ↓i))
    (⨆ (i_1 : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)), Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1))
    k
rw :
  Eq (α :=
    (F.obj
          (Sigma.fst (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j))
            (Cover.idx
              (Opens.iSupOpenCover fun (i_1 : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)) ↦
                Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1))
              (Subtype.mk (p := fun (x : ↥(F.obj ↓i)) ↦
                Membership.mem (γ := TopologicalSpace.Opens ↥(F.obj ↓i))
                  (⨆ (i_1 : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)),
                    Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1))
                  x)
                k hk)))).toLocallyRingedSpace ⟶
      s.pt)
    (Hom.toLRSHom
        (Iso.hom
          (Hom.isoOpensRange
            (F.map
              (Sigma.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j))
                    (Cover.idx
                      (Opens.iSupOpenCover fun (i_1 : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)) ↦
                        Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1))
                      (Subtype.mk (p := fun (x : ↥(F.obj ↓i)) ↦
                        Membership.mem (γ := TopologicalSpace.Opens ↥(F.obj ↓i))
                          (⨆ (i_1 : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)),
                            Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1))
                          x)
                        k hk)) :
                  Quiver.Hom.{v, w} (V := J)
                      (Sigma.fst (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j))
                          (Cover.idx
                            (Opens.iSupOpenCover fun (i_1 : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)) ↦
                              Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1))
                            (Subtype.mk (p := fun (x : ↥(F.obj ↓i)) ↦
                              Membership.mem (γ := TopologicalSpace.Opens ↥(F.obj ↓i))
                                (⨆ (i_1 : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)),
                                  Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1))
                                x)
                              k hk)) :
                        J)
                      (↓i : J) ×
                    Quiver.Hom.{v, w} (V := J)
                      (Sigma.fst (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j))
                          (Cover.idx
                            (Opens.iSupOpenCover fun (i_1 : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)) ↦
                              Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1))
                            (Subtype.mk (p := fun (x : ↥(F.obj ↓i)) ↦
                              Membership.mem (γ := TopologicalSpace.Opens ↥(F.obj ↓i))
                                (⨆ (i_1 : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)),
                                  Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1))
                                x)
                              k hk)) :
                        J)
                      (↓j : J)).1))) ≫
      Hom.toLRSHom
          ((Cover.gluedCover (X :=
                (↑(⨆ (i_1 : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)),
                      Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1)) :
                  Scheme))
                (Cover.ulift (P := IsOpenImmersion)
                  (Opens.iSupOpenCover fun (i_1 : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)) ↦
                    Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1)))).ι
            (Subtype.mk (p := fun (x : ↥(F.obj ↓i)) ↦
              Membership.mem (γ := TopologicalSpace.Opens ↥(F.obj ↓i))
                (⨆ (i_1 : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)),
                  Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1))
                x)
              k hk)) ≫
        Hom.toLRSHom
            (Cover.fromGlued
              (Cover.ulift (P := IsOpenImmersion)
                (Opens.iSupOpenCover fun (i_1 : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)) ↦
                  Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1)))) ≫
          Hom.toLRSHom (Opens.ι (V F (↓i) ↓j)) ≫ s.ι.app ↓i)
    (Hom.toLRSHom
        (Iso.hom
          (Hom.isoOpensRange
            (F.map
              (Sigma.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j))
                    (Cover.idx
                      (Opens.iSupOpenCover fun (i_1 : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)) ↦
                        Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1))
                      (Subtype.mk (p := fun (x : ↥(F.obj ↓i)) ↦
                        Membership.mem (γ := TopologicalSpace.Opens ↥(F.obj ↓i))
                          (⨆ (i_1 : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)),
                            Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1))
                          x)
                        k hk)) :
                  Quiver.Hom.{v, w} (V := J)
                      (Sigma.fst (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j))
                          (Cover.idx
                            (Opens.iSupOpenCover fun (i_1 : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)) ↦
                              Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1))
                            (Subtype.mk (p := fun (x : ↥(F.obj ↓i)) ↦
                              Membership.mem (γ := TopologicalSpace.Opens ↥(F.obj ↓i))
                                (⨆ (i_1 : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)),
                                  Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1))
                                x)
                              k hk)) :
                        J)
                      (↓i : J) ×
                    Quiver.Hom.{v, w} (V := J)
                      (Sigma.fst (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j))
                          (Cover.idx
                            (Opens.iSupOpenCover fun (i_1 : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)) ↦
                              Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1))
                            (Subtype.mk (p := fun (x : ↥(F.obj ↓i)) ↦
                              Membership.mem (γ := TopologicalSpace.Opens ↥(F.obj ↓i))
                                (⨆ (i_1 : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)),
                                  Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1))
                                x)
                              k hk)) :
                        J)
                      (↓j : J)).1))) ≫
      CategoryStruct.comp (Y :=
        (Cover.gluedCover (X :=
              (↑(⨆ (i_1 : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)),
                    Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1)) :
                Scheme))
              (Cover.ulift (P := IsOpenImmersion)
                (Opens.iSupOpenCover fun (i_1 : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)) ↦
                  Hom.opensRange
                    (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1)))).glued.toLocallyRingedSpace)
        (Hom.toLRSHom
            ((Cover.gluedCover (X :=
                  (↑(⨆ (i_1 : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)),
                        Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1)) :
                    Scheme))
                  (Cover.ulift (P := IsOpenImmersion)
                    (Opens.iSupOpenCover fun (i_1 : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)) ↦
                      Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1)))).ι
              (Subtype.mk (p := fun (x : ↥(F.obj ↓i)) ↦
                Membership.mem (γ := TopologicalSpace.Opens ↥(F.obj ↓i))
                  (⨆ (i_1 : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)),
                    Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1))
                  x)
                k hk)) :
          ((Cover.gluedCover (X :=
                    (↑(⨆ (i_1 : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)),
                          Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1)) :
                      Scheme))
                    (Cover.ulift (P := IsOpenImmersion)
                      (Opens.iSupOpenCover fun (i_1 : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)) ↦
                        Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1)))).U
                (Subtype.mk (p := fun (x : ↥(F.obj ↓i)) ↦
                  Membership.mem (γ := TopologicalSpace.Opens ↥(F.obj ↓i))
                    (⨆ (i_1 : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)),
                      Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1))
                    x)
                  k hk)).toLocallyRingedSpace ⟶
            (Cover.gluedCover (X :=
                  (↑(⨆ (i_1 : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)),
                        Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1)) :
                    Scheme))
                  (Cover.ulift (P := IsOpenImmersion)
                    (Opens.iSupOpenCover fun (i_1 : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)) ↦
                      Hom.opensRange
                        (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1)))).glued.toLocallyRingedSpace)
        (Hom.toLRSHom
              (Cover.fromGlued
                (Cover.ulift (P := IsOpenImmersion)
                  (Opens.iSupOpenCover fun (i_1 : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)) ↦
                    Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1)))) ≫
            Hom.toLRSHom (tAux F (↓i) ↓j) ≫ s.ι.app ↓j :
          (Cover.gluedCover (X :=
                  (↑(⨆ (i_1 : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)),
                        Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1)) :
                    Scheme))
                  (Cover.ulift (P := IsOpenImmersion)
                    (Opens.iSupOpenCover fun (i_1 : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)) ↦
                      Hom.opensRange
                        (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1)))).glued.toLocallyRingedSpace ⟶
            s.pt))
⊢ Eq (α :=
    (Cover.gluedCover (X :=
                (↑(⨆ (i_1 : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)),
                      Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1)) :
                  Scheme))
                (Cover.ulift (P := IsOpenImmersion)
                  (Opens.iSupOpenCover fun (i_1 : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)) ↦
                    Hom.opensRange
                      (F.map
                        i_1.snd (β := fun (k : J) ↦
                            (k ⟶ ↓i) × (k ⟶ ↓j)).1)))).toLocallyRingedSpaceGlueData.diagram.right
        (Subtype.mk (p := fun (x : ↥(F.obj ↓i)) ↦
          Membership.mem (γ := TopologicalSpace.Opens ↥(F.obj ↓i))
            (⨆ (i_1 : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)),
              Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1))
            x)
          k hk) ⟶
      s.pt)
    (Multicoequalizer.π
        (Cover.gluedCover (X :=
              (↑(⨆ (i_1 : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)),
                    Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1)) :
                Scheme))
              (Cover.ulift (P := IsOpenImmersion)
                (Opens.iSupOpenCover fun (i_1 : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)) ↦
                  Hom.opensRange
                    (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1)))).toLocallyRingedSpaceGlueData.diagram
        (Subtype.mk (p := fun (x : ↥(F.obj ↓i)) ↦
          Membership.mem (γ := TopologicalSpace.Opens ↥(F.obj ↓i))
            (⨆ (i_1 : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)),
              Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1))
            x)
          k hk) ≫
      Iso.inv
          (Cover.gluedCover (X :=
              (↑(⨆ (i_1 : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)),
                    Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1)) :
                Scheme))
              (Cover.ulift (P := IsOpenImmersion)
                (Opens.iSupOpenCover fun (i_1 : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)) ↦
                  Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1)))).isoLocallyRingedSpace ≫
        Hom.toLRSHom
            (Cover.fromGlued
              (Cover.ulift (P := IsOpenImmersion)
                (Opens.iSupOpenCover fun (i_1 : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)) ↦
                  Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1)))) ≫
          Hom.toLRSHom (Opens.ι (V F (↓i) ↓j)) ≫ s.ι.app ↓i)
    (CategoryStruct.comp (Y :=
      multicoequalizer
        (Cover.gluedCover (X :=
              (↑(⨆ (i_1 : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)),
                    Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1)) :
                Scheme))
              (Cover.ulift (P := IsOpenImmersion)
                (Opens.iSupOpenCover fun (i_1 : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)) ↦
                  Hom.opensRange
                    (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1)))).toLocallyRingedSpaceGlueData.diagram)
      (Multicoequalizer.π
          (Cover.gluedCover (X :=
                (↑(⨆ (i_1 : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)),
                      Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1)) :
                  Scheme))
                (Cover.ulift (P := IsOpenImmersion)
                  (Opens.iSupOpenCover fun (i_1 : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)) ↦
                    Hom.opensRange
                      (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1)))).toLocallyRingedSpaceGlueData.diagram
          (Subtype.mk (p := fun (x : ↥(F.obj ↓i)) ↦
            Membership.mem (γ := TopologicalSpace.Opens ↥(F.obj ↓i))
              (⨆ (i_1 : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)),
                Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1))
              x)
            k hk) :
        (Cover.gluedCover (X :=
                    (↑(⨆ (i_1 : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)),
                          Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1)) :
                      Scheme))
                    (Cover.ulift (P := IsOpenImmersion)
                      (Opens.iSupOpenCover fun (i_1 : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)) ↦
                        Hom.opensRange
                          (F.map
                            i_1.snd (β := fun (k : J) ↦
                                (k ⟶ ↓i) × (k ⟶ ↓j)).1)))).toLocallyRingedSpaceGlueData.diagram.right
            (Subtype.mk (p := fun (x : ↥(F.obj ↓i)) ↦
              Membership.mem (γ := TopologicalSpace.Opens ↥(F.obj ↓i))
                (⨆ (i_1 : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)),
                  Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1))
                x)
              k hk) ⟶
          multicoequalizer
            (Cover.gluedCover (X :=
                  (↑(⨆ (i_1 : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)),
                        Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1)) :
                    Scheme))
                  (Cover.ulift (P := IsOpenImmersion)
                    (Opens.iSupOpenCover fun (i_1 : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)) ↦
                      Hom.opensRange
                        (F.map
                          i_1.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1)))).toLocallyRingedSpaceGlueData.diagram)
      (Iso.inv
            (Cover.gluedCover (X :=
                (↑(⨆ (i_1 : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)),
                      Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1)) :
                  Scheme))
                (Cover.ulift (P := IsOpenImmersion)
                  (Opens.iSupOpenCover fun (i_1 : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)) ↦
                    Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1)))).isoLocallyRingedSpace ≫
          Hom.toLRSHom
              (Cover.fromGlued
                (Cover.ulift (P := IsOpenImmersion)
                  (Opens.iSupOpenCover fun (i_1 : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)) ↦
                    Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1)))) ≫
            Hom.toLRSHom (tAux F (↓i) ↓j) ≫ s.ι.app ↓j :
        (Cover.gluedCover (X :=
                (↑(⨆ (i_1 : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)),
                      Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1)) :
                  Scheme))
                (Cover.ulift (P := IsOpenImmersion)
                  (Opens.iSupOpenCover fun (i_1 : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)) ↦
                    Hom.opensRange
                      (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1)))).toLocallyRingedSpaceGlueData.glued ⟶
          s.pt))

Tactic:
rw [← CategoryTheory.GlueData.ι, reassoc_of% GlueData.ι_isoLocallyRingedSpace_inv,
        reassoc_of% GlueData.ι_isoLocallyRingedSpace_inv,
        ← cancel_epi (Hom.isoOpensRange (F.map _)).hom.toLRSHom]

Premises used: AlgebraicGeometry.Scheme.Hom.toLRSHom, AlgebraicGeometry.Scheme.Hom.isoOpensRange, CategoryTheory.Functor.map, CategoryTheory.GlueData.ι, AlgebraicGeometry.Scheme.GlueData.ι_isoLocallyRingedSpace_inv, CategoryTheory.cancel_epi, CategoryTheory.Iso.hom