-- 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
refine :
  ∀
    (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))
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
refine Multicoequalizer.hom_ext _ _ _ fun ⟨k, hk⟩ ↦ ?_