-- 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
pf : ∀ (i_1 : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)), IsOpenImmersion (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1)
pf_1 :
  ∀ (i_1 : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)),
    Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1) ≤
      ⨆ (i_2 : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)), Hom.opensRange (F.map i_2.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1)
h :
  ∃ (i_1 : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)) (y :
    ↥(↑(Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1)) : Scheme)),
    ((F.obj ↓i).homOfLE ⋯) y =
      Subtype.mk (p := fun (x : ↥(F.obj ↓i)) ↦
        Membership.mem (γ := TopologicalSpace.Opens ↥(F.obj ↓i))
          (⨆ (i_2 : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)),
            Hom.opensRange (F.map i_2.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1))
          x)
        k hk
pf_2 :
  IsOpenImmersion
    (F.map
      h.choose (p := fun (i_1 : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)) ↦
              ∃ (y : ↥(↑(Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1)) : Scheme)),
                ((F.obj ↓i).homOfLE ⋯) y =
                  Subtype.mk (p := fun (x : ↥(F.obj ↓i)) ↦
                    Membership.mem (γ := TopologicalSpace.Opens ↥(F.obj ↓i))
                      (⨆ (i_2 : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)),
                        Hom.opensRange (F.map i_2.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1))
                      x)
                    k hk).snd
          (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1)
pf_3 :
  ∀
    (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)),
    ∃ (a : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)) (y :
      ↥(↑(Hom.opensRange (F.map a.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1)) : Scheme)),
      ((F.obj ↓i).homOfLE ⋯) y = x
pf_4 :
  ∀
    (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)),
    IsOpenImmersion
      (F.map
        ⋯.choose (p := fun (i_1 : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)) ↦
                ∃ (y : ↥(↑(Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1)) : Scheme)),
                  ((F.obj ↓i).homOfLE ⋯) y = x).snd
            (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1)
pf_5 :
  ∀
    (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)),
    Hom.opensRange
        (F.map
          ⋯.choose (p := fun (i_1 : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)) ↦
                  ∃ (y : ↥(↑(Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1)) : Scheme)),
                    ((F.obj ↓i).homOfLE ⋯) y = x).snd
              (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1) ≤
      ⨆ (i_1 : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)), Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1)
pf_6 :
  Membership.mem (γ :=
    Set
      (Presieve
        (↑(⨆ (i_1 : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)),
              Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1)) :
          Scheme)))
    ((precoverage IsOpenImmersion).coverings
      (↑(⨆ (i_1 : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)),
            Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1)) :
        Scheme))
    (PreZeroHypercover.presieve₀
      {
        I₀ :=
          ↥(↑(⨆ (i_1 : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)),
                  Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1)) :
              Scheme),
        X :=
          fun
            (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)) ↦
          (↑(Hom.opensRange
                (F.map
                  ⋯.choose (p := fun (i_1 : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)) ↦
                          ∃ (y :
                            ↥(↑(Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1)) : Scheme)),
                            ((F.obj ↓i).homOfLE ⋯) y = x).snd
                      (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1)) :
            Scheme),
        f :=
          fun
            (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)) ↦
          (F.obj ↓i).homOfLE ⋯ })
pf_7 :
  Hom.opensRange
      (F.map
        h.choose (p := fun (i_1 : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)) ↦
                ∃ (y : ↥(↑(Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1)) : Scheme)),
                  ((F.obj ↓i).homOfLE ⋯) y =
                    Subtype.mk (p := fun (x : ↥(F.obj ↓i)) ↦
                      Membership.mem (γ := TopologicalSpace.Opens ↥(F.obj ↓i))
                        (⨆ (i_2 : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)),
                          Hom.opensRange (F.map i_2.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1))
                        x)
                      k hk).snd
            (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1) ≤
    ⨆ (i_1 : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)), Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1)
rw :
  Hom.toLRSHom
        (F.map
          h.choose (p := fun (i_1 : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)) ↦
                  ∃ (y : ↥(↑(Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1)) : Scheme)),
                    ((F.obj ↓i).homOfLE ⋯) y =
                      Subtype.mk (p := fun (x : ↥(F.obj ↓i)) ↦
                        Membership.mem (γ := TopologicalSpace.Opens ↥(F.obj ↓i))
                          (⨆ (i_2 : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)),
                            Hom.opensRange (F.map i_2.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1))
                          x)
                        k hk).snd
              (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1) ≫
      s.ι.app ↓i =
    Hom.toLRSHom
        (F.map
          h.choose (p := fun (i_1 : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)) ↦
                  ∃ (y : ↥(↑(Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1)) : Scheme)),
                    ((F.obj ↓i).homOfLE ⋯) y =
                      Subtype.mk (p := fun (x : ↥(F.obj ↓i)) ↦
                        Membership.mem (γ := TopologicalSpace.Opens ↥(F.obj ↓i))
                          (⨆ (i_2 : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)),
                            Hom.opensRange (F.map i_2.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1))
                          x)
                        k hk).snd
              (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).2) ≫
      s.ι.app ↓j
⊢ Hom.toLRSHom
        (F.map
          h.choose (p := fun (i_1 : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)) ↦
                  ∃ (y : ↥(↑(Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1)) : Scheme)),
                    ((F.obj ↓i).homOfLE ⋯) y =
                      Subtype.mk (p := fun (x : ↥(F.obj ↓i)) ↦
                        Membership.mem (γ := TopologicalSpace.Opens ↥(F.obj ↓i))
                          (⨆ (i_2 : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)),
                            Hom.opensRange (F.map i_2.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1))
                          x)
                        k hk).snd
              (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1) ≫
      s.ι.app ↓i =
    Hom.toLRSHom
        (Iso.hom
            (Hom.isoOpensRange
              (F.map
                h.choose (p := fun (i_1 : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)) ↦
                        ∃ (y :
                          ↥(↑(Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1)) : Scheme)),
                          ((F.obj ↓i).homOfLE ⋯) y =
                            Subtype.mk (p := fun (x : ↥(F.obj ↓i)) ↦
                              Membership.mem (γ := TopologicalSpace.Opens ↥(F.obj ↓i))
                                (⨆ (i_2 : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)),
                                  Hom.opensRange (F.map i_2.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1))
                                x)
                              k hk).snd
                    (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1)) ≫
          (F.obj ↓i).homOfLE pf_7 ≫ tAux F (↓i) ↓j) ≫
      s.ι.app ↓j

Tactic:
rw [homOfLE_tAux F ↓i ↓j h.choose.2.1 h.choose.2.2, Iso.hom_inv_id_assoc]

Premises used: AlgebraicGeometry.Scheme.IsLocallyDirected.homOfLE_tAux, Prod.fst, CategoryTheory.Iso.hom_inv_id_assoc, Exists.choose, Equiv.symm, equivShrink, Sigma.snd, Prod.snd, DFunLike.coe