-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Gluing (goal)
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
⊢ 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))
have 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))
Tactic: rw [← CategoryTheory.GlueData.ι, reassoc_of% GlueData.ι_isoLocallyRingedSpace_inv,
        reassoc_of% GlueData.ι_isoLocallyRingedSpace_inv,
        ← cancel_epi (Hom.isoOpensRange (F.map _)).hom.toLRSHom]