-- 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
simp : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ 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:
simp +instances only [Opens.iSupOpenCover, Cover.ulift, V, ← Hom.comp_toLRSHom_assoc,
        Cover.ι_fromGlued_assoc, homOfLE_ι, Hom.isoOpensRange_hom_ι, Cover.idx]

Premises used: AlgebraicGeometry.Scheme.homOfLE_ι, AlgebraicGeometry.Scheme.Cover.ι_fromGlued_assoc, AlgebraicGeometry.Scheme.Hom.isoOpensRange_hom_ι, AlgebraicGeometry.Scheme.IsLocallyDirected.V, AlgebraicGeometry.Scheme.Hom.comp_toLRSHom_assoc, AlgebraicGeometry.Scheme.Cover.idx, AlgebraicGeometry.Scheme.Opens.iSupOpenCover, AlgebraicGeometry.Scheme.Cover.ulift