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

Tactic:
generalize_proofs _ _ h