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