awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X : Scheme
I : X.IdealSheafData
V : (↑X.affineOpens : Type u)
f : (↑Γ(X, (↑V : X.Opens)) : Type u)
this_1 : Algebra ((↑Γ(X, (↑V : X.Opens)) : Type u) ⧸ I.ideal V)
  (HasQuotient.Quotient (↑Γ(X, (↑(X.affineBasicOpen f) : X.Opens)) : Type u) (B :=
    Ideal (↑Γ(X, (↑(X.affineBasicOpen f) : X.Opens)) : Type u)) (I.ideal (X.affineBasicOpen f))) :=
  RingHom.toAlgebra
    (Ideal.quotientMap (I.ideal (X.affineBasicOpen f)) (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) ⋯)
f' : (↑Γ(X, (↑V : X.Opens)) : Type u) ⧸ I.ideal V :=
  (Ideal.Quotient.mk (I.ideal V) :
      (a : (↑Γ(X, (↑V : X.Opens)) : Type u)) → (↑Γ(X, (↑V : X.Opens)) : Type u) ⧸ I.ideal V)
    f
this :
  IsLocalization.Away (R := (↑Γ(X, (↑V : X.Opens)) : Type u) ⧸ I.ideal V)
    ((Ideal.Quotient.mk (I.ideal V) :
          (a : (↑Γ(X, (↑V : X.Opens)) : Type u)) → (↑Γ(X, (↑V : X.Opens)) : Type u) ⧸ I.ideal V)
        f :
      (↑Γ(X, (↑V : X.Opens)) : Type u) ⧸ I.ideal V)
    (HasQuotient.Quotient (↑Γ(X, (↑(X.affineBasicOpen f) : X.Opens)) : Type u) (B :=
      Ideal (↑Γ(X, (↑(X.affineBasicOpen f) : X.Opens)) : Type u)) (I.ideal (X.affineBasicOpen f)))
⊢ (↑(PrimeSpectrum.basicOpen f') : Set (PrimeSpectrum ((↑Γ(X, (↑V : X.Opens)) : Type u) ⧸ I.ideal V))) =
    (↑(I.glueDataObjι V ⁻¹ᵁ (↑V : X.Opens).ι ⁻¹ᵁ X.basicOpen f) : Set ↥(I.glueDataObj V))
have h : (↑((Opens.comap
              { toFun := comap (Ideal.Quotient.mk (I.ideal V)), continuous_toFun := sorry :
                C(PrimeSpectrum ((↑Γ(X, (↑V : X.Opens)) : Type u) ⧸ I.ideal V),
                  PrimeSpectrum (↑Γ(X, (↑V : X.Opens)) : Type u)) } :
            (a : TopologicalSpace.Opens (PrimeSpectrum (↑Γ(X, (↑V : X.Opens)) : Type u))) →
              TopologicalSpace.Opens (PrimeSpectrum ((↑Γ(X, (↑V : X.Opens)) : Type u) ⧸ I.ideal V)))
          (IsAffineOpen.fromSpec sorry ⁻¹ᵁ X.basicOpen f) :
        TopologicalSpace.Opens (PrimeSpectrum ((↑Γ(X, (↑V : X.Opens)) : Type u) ⧸ I.ideal V))) :
    Set (PrimeSpectrum ((↑Γ(X, (↑V : X.Opens)) : Type u) ⧸ I.ideal V))) =
  (↑((Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal V))) ≫ IsAffineOpen.fromSpec sorry) ⁻¹ᵁ X.basicOpen f) :
    Set ↥(I.glueDataObj V))
Tactic: rw [← comap_basicOpen, ← V.2.fromSpec_preimage_basicOpen,
    ← Scheme.Hom.comp_preimage, glueDataObjι_ι]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X : Scheme
I : X.IdealSheafData
U V : (↑X.affineOpens : Type u)
h : U ≤ V
⊢ I.glueDataObjMap h ≫ I.glueDataObjι V = I.glueDataObjι U ≫ X.homOfLE h
have rw : Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U))) ≫
    Spec.map (CommRingCat.ofHom (CommRingCat.Hom.hom (X.presheaf.map (homOfLE h).op))) ≫ (IsAffineOpen.isoSpec sorry).inv =
  Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U))) ≫ (IsAffineOpen.isoSpec sorry).inv ≫ X.homOfLE h
Tactic: rw [glueDataObjMap, glueDataObjι, ← Spec.map_comp_assoc, ← CommRingCat.ofHom_comp,
    Ideal.quotientMap_comp_mk, CommRingCat.ofHom_comp, Spec.map_comp_assoc, glueDataObjι,
    Category.assoc]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X : Scheme
I : X.IdealSheafData
U V : (↑X.affineOpens : Type u)
h : U ≤ V
⊢ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U))) ≫
      Spec.map (CommRingCat.ofHom (CommRingCat.Hom.hom (X.presheaf.map (homOfLE h).op))) ≫
        (IsAffineOpen.isoSpec ⋯).inv =
    Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U))) ≫ (IsAffineOpen.isoSpec ⋯).inv ≫ X.homOfLE h
have e_a : Spec.map (CommRingCat.ofHom (CommRingCat.Hom.hom (X.presheaf.map (homOfLE h).op))) ≫ (IsAffineOpen.isoSpec sorry).inv =
  (IsAffineOpen.isoSpec sorry).inv ≫ X.homOfLE h
Tactic: congr 1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X : Scheme
I : X.IdealSheafData
U V : (↑X.affineOpens : Type u)
h : U ≤ V
⊢ Spec.map (CommRingCat.ofHom (CommRingCat.Hom.hom (X.presheaf.map (homOfLE h).op))) ≫ (IsAffineOpen.isoSpec ⋯).inv =
    (IsAffineOpen.isoSpec ⋯).inv ≫ X.homOfLE h
have e_a : (↑U : X.Opens).toSpecΓ ≫ Spec.map (X.presheaf.map (homOfLE h).op) ≫ (IsAffineOpen.isoSpec sorry).inv = X.homOfLE h
Tactic: rw [Iso.eq_inv_comp, IsAffineOpen.isoSpec_hom, CommRingCat.ofHom_hom]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X : Scheme
I : X.IdealSheafData
U V : (↑X.affineOpens : Type u)
h : U ≤ V
⊢ (↑U : X.Opens).toSpecΓ ≫ Spec.map (X.presheaf.map (homOfLE h).op) ≫ (IsAffineOpen.isoSpec ⋯).inv = X.homOfLE h
have e_a : X.homOfLE h ≫ (↑V : X.Opens).toSpecΓ ≫ (IsAffineOpen.isoSpec sorry).inv = X.homOfLE h
Tactic: erw [Scheme.Opens.toSpecΓ_SpecMap_presheaf_map_assoc U.1 V.1 h]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X : Scheme
I : X.IdealSheafData
U V : (↑X.affineOpens : Type u)
h : U ≤ V
⊢ X.homOfLE h ≫ (↑V : X.Opens).toSpecΓ ≫ (IsAffineOpen.isoSpec ⋯).inv = X.homOfLE h
have e_a : X.homOfLE h ≫ (IsAffineOpen.isoSpec sorry).hom ≫ (IsAffineOpen.isoSpec sorry).inv = X.homOfLE h
Tactic: rw [← IsAffineOpen.isoSpec_hom V.2, Iso.hom_inv_id, Category.comp_id]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X : Scheme
I : X.IdealSheafData
U V : (↑X.affineOpens : Type u)
h : U ≤ V
e_a : X.homOfLE h ≫ (IsAffineOpen.isoSpec ⋯).hom ≫ (IsAffineOpen.isoSpec ⋯).inv = X.homOfLE h
⊢ X.homOfLE h ≫ (↑V : X.Opens).toSpecΓ ≫ (IsAffineOpen.isoSpec ⋯).inv = X.homOfLE h
have e_a₁ : X.homOfLE h ≫ 𝟙 (↑(↑V : X.Opens) : Scheme) = X.homOfLE h
Tactic: rw [← IsAffineOpen.isoSpec_hom V.2, Iso.hom_inv_id, Category.comp_id]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X : Scheme
I : X.IdealSheafData
U V : (↑X.affineOpens : Type u)
h : U ≤ V
e_a : X.homOfLE h ≫ (IsAffineOpen.isoSpec ⋯).hom ≫ (IsAffineOpen.isoSpec ⋯).inv = X.homOfLE h
e_a₁ : X.homOfLE h ≫ 𝟙 (↑(↑V : X.Opens) : Scheme) = X.homOfLE h
⊢ X.homOfLE h ≫ (↑V : X.Opens).toSpecΓ ≫ (IsAffineOpen.isoSpec ⋯).inv = X.homOfLE h
have e_a₂ : X.homOfLE h = X.homOfLE h
Tactic: rw [← IsAffineOpen.isoSpec_hom V.2, Iso.hom_inv_id, Category.comp_id]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X : Scheme
I : X.IdealSheafData
U V : (↑X.affineOpens : Type u)
F : pullback (Y := (↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme)) (I.glueDataObjι U) (X.homOfLE ⋯) ⟶
  (↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme) :=
  pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯)
⊢ I.glueDataObjPullback U V ⟶ I.glueDataObjPullback V U
have refine_1 : I.ideal V ≤
  RingHom.ker
    (CommRingCat.Hom.hom
      (Iso.inv (ΓSpecIso Γ(X, (↑V : X.Opens))) ≫ Hom.appTop (F ≫ X.homOfLE sorry ≫ (IsAffineOpen.isoSpec sorry).hom)))
Tactic: refine pullback.lift ((F ≫ X.homOfLE inf_le_right ≫
    V.2.isoSpec.hom).liftQuotient _ ?_) (F ≫ X.homOfLE (by simp)) ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X : Scheme
I : X.IdealSheafData
U V : (↑X.affineOpens : Type u)
F : pullback (Y := (↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme)) (I.glueDataObjι U) (X.homOfLE ⋯) ⟶
  (↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme) :=
  pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯)
refine_1 :
  I.ideal V ≤
    RingHom.ker
      (CommRingCat.Hom.hom
        (Iso.inv (ΓSpecIso Γ(X, (↑V : X.Opens))) ≫ Hom.appTop (F ≫ X.homOfLE ⋯ ≫ (IsAffineOpen.isoSpec ⋯).hom)))
⊢ I.glueDataObjPullback U V ⟶ I.glueDataObjPullback V U
have refine_2 : Hom.liftQuotient (F ≫ X.homOfLE sorry ≫ (IsAffineOpen.isoSpec sorry).hom) (I.ideal V) sorry ≫ I.glueDataObjι V =
  (F ≫ X.homOfLE sorry) ≫ X.homOfLE sorry
Tactic: refine pullback.lift ((F ≫ X.homOfLE inf_le_right ≫
    V.2.isoSpec.hom).liftQuotient _ ?_) (F ≫ X.homOfLE (by simp)) ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X : Scheme
I : X.IdealSheafData
U V : (↑X.affineOpens : Type u)
F : pullback (Y := (↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme)) (I.glueDataObjι U) (X.homOfLE ⋯) ⟶
  (↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme) :=
  pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯)
x : (↑Γ(X, (↑V : X.Opens)) : Type u)
hx : x ∈ I.ideal V
⊢ Membership.mem (γ := Submodule (↑Γ(X, (↑V : X.Opens)) : Type u) (↑Γ(X, (↑V : X.Opens)) : Type u))
    (RingHom.ker
      (CommRingCat.Hom.hom
        (Iso.inv (ΓSpecIso Γ(X, (↑V : X.Opens))) ≫ Hom.appTop (F ≫ X.homOfLE ⋯ ≫ (IsAffineOpen.isoSpec ⋯).hom))))
    x
have refine_1 : Eq (α := (↑Γ(pullback (I.glueDataObjι U) (X.homOfLE sorry), ⊤) : Type u))
  (((CommRingCat.Hom.hom
            (Iso.inv (ΓSpecIso Γ(X, (↑V : X.Opens))) ≫
              Hom.app (IsAffineOpen.isoSpec sorry).hom ⊤ ≫
                CategoryStruct.comp (Y := Γ((↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme), ⊤))
                  (X.presheaf.map (Quiver.Hom.op (homOfLE sorry)) :
                    Γ(X, (↑V : X.Opens).ι ''ᵁ ⊤) ⟶ Γ(X, ((↑U : X.Opens) ⊓ (↑V : X.Opens)).ι ''ᵁ ⊤))
                  (Hom.app F ⊤ :
                    Γ((↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme), ⊤) ⟶
                      Γ(pullback (I.glueDataObjι U) (X.homOfLE sorry), F ⁻¹ᵁ ⊤))) :
          (↑Γ(X, (↑V : X.Opens)) : Type u) →+* (↑Γ(pullback (I.glueDataObjι U) (X.homOfLE sorry), ⊤) : Type u)) :
        (a : (↑Γ(X, (↑V : X.Opens)) : Type u)) → (↑Γ(pullback (I.glueDataObjι U) (X.homOfLE sorry), ⊤) : Type u))
      x :
    (↑Γ(pullback (I.glueDataObjι U) (X.homOfLE sorry), ⊤) : Type u))
  (0 : (↑Γ(pullback (I.glueDataObjι U) (X.homOfLE sorry), ⊤) : Type u))
Tactic: simp only [Hom.comp_app, Hom.comp_base, TopologicalSpace.Opens.map_comp_obj,
      TopologicalSpace.Opens.map_top, homOfLE_app, homOfLE_leOfHom, Category.assoc, RingHom.mem_ker]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X : Scheme
I : X.IdealSheafData
U V : (↑X.affineOpens : Type u)
F : pullback (Y := (↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme)) (I.glueDataObjι U) (X.homOfLE ⋯) ⟶
  (↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme) :=
  pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯)
x : (↑Γ(X, (↑V : X.Opens)) : Type u)
hx : x ∈ I.ideal V
⊢ ⊤ ≤ (F ≫ X.homOfLE ⋯) ⁻¹ᵁ (↑U : X.Opens).ι ⁻¹ᵁ (↑V : X.Opens)
have rw : ⊤ ≤ (F ≫ ((↑U : X.Opens) ⊓ (↑V : X.Opens)).ι) ⁻¹ᵁ (↑V : X.Opens)
Tactic: rw [← Scheme.Hom.comp_preimage, Category.assoc, X.homOfLE_ι]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X : Scheme
I : X.IdealSheafData
U V : (↑X.affineOpens : Type u)
F : pullback (Y := (↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme)) (I.glueDataObjι U) (X.homOfLE ⋯) ⟶
  (↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme) :=
  pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯)
x : (↑Γ(X, (↑V : X.Opens)) : Type u)
hx : x ∈ I.ideal V
⊢ Eq (α := (↑Γ(pullback (I.glueDataObjι U) (X.homOfLE ⋯), ⊤) : Type u))
    (((CommRingCat.Hom.hom
              (Iso.inv (ΓSpecIso Γ(X, (↑V : X.Opens))) ≫
                Hom.app (IsAffineOpen.isoSpec ⋯).hom ⊤ ≫
                  CategoryStruct.comp (Y := Γ((↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme), ⊤))
                    (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯)) :
                      Γ(X, (↑V : X.Opens).ι ''ᵁ ⊤) ⟶ Γ(X, ((↑U : X.Opens) ⊓ (↑V : X.Opens)).ι ''ᵁ ⊤))
                    (Hom.app F ⊤ :
                      Γ((↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme), ⊤) ⟶
                        Γ(pullback (I.glueDataObjι U) (X.homOfLE ⋯), F ⁻¹ᵁ ⊤))) :
            (↑Γ(X, (↑V : X.Opens)) : Type u) →+* (↑Γ(pullback (I.glueDataObjι U) (X.homOfLE ⋯), ⊤) : Type u)) :
          (a : (↑Γ(X, (↑V : X.Opens)) : Type u)) → (↑Γ(pullback (I.glueDataObjι U) (X.homOfLE ⋯), ⊤) : Type u))
        x :
      (↑Γ(pullback (I.glueDataObjι U) (X.homOfLE ⋯), ⊤) : Type u))
    (0 : (↑Γ(pullback (I.glueDataObjι U) (X.homOfLE ⋯), ⊤) : Type u))
have h : Iso.inv (ΓSpecIso Γ(X, (↑V : X.Opens))) ≫
    Hom.app (IsAffineOpen.isoSpec sorry).hom ⊤ ≫
      CategoryStruct.comp (Y := Γ((↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme), ⊤))
        (X.presheaf.map (Quiver.Hom.op (homOfLE sorry)) :
          Γ(X, (↑V : X.Opens).ι ''ᵁ ⊤) ⟶ Γ(X, ((↑U : X.Opens) ⊓ (↑V : X.Opens)).ι ''ᵁ ⊤))
        (Hom.app F ⊤ :
          Γ((↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme), ⊤) ⟶ Γ(pullback (I.glueDataObjι U) (X.homOfLE sorry), F ⁻¹ᵁ ⊤)) =
  Hom.app (↑U : X.Opens).ι (↑V : X.Opens) ≫ Hom.appLE (F ≫ X.homOfLE sorry) ((↑U : X.Opens).ι ⁻¹ᵁ (↑V : X.Opens)) ⊤ sorry
Tactic: convert_to (U.1.ι.app V.1 ≫ (F ≫ X.homOfLE inf_le_left).appLE (U.1.ι ⁻¹ᵁ V.1) ⊤
      (by rw [← Scheme.Hom.comp_preimage, Category.assoc, X.homOfLE_ι]
          exact fun x _ ↦ by simpa using (F x).2.2)).hom x = 0 using 3
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X : Scheme
I : X.IdealSheafData
U V : (↑X.affineOpens : Type u)
F : pullback (Y := (↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme)) (I.glueDataObjι U) (X.homOfLE ⋯) ⟶
  (↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme) :=
  pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯)
x : (↑Γ(X, (↑V : X.Opens)) : Type u)
hx : x ∈ I.ideal V
h :
  Iso.inv (ΓSpecIso Γ(X, (↑V : X.Opens))) ≫
      Hom.app (IsAffineOpen.isoSpec ⋯).hom ⊤ ≫
        CategoryStruct.comp (Y := Γ((↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme), ⊤))
          (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯)) :
            Γ(X, (↑V : X.Opens).ι ''ᵁ ⊤) ⟶ Γ(X, ((↑U : X.Opens) ⊓ (↑V : X.Opens)).ι ''ᵁ ⊤))
          (Hom.app F ⊤ :
            Γ((↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme), ⊤) ⟶
              Γ(pullback (I.glueDataObjι U) (X.homOfLE ⋯), F ⁻¹ᵁ ⊤)) =
    Hom.app (↑U : X.Opens).ι (↑V : X.Opens) ≫ Hom.appLE (F ≫ X.homOfLE ⋯) ((↑U : X.Opens).ι ⁻¹ᵁ (↑V : X.Opens)) ⊤ ⋯
⊢ Eq (α := (↑Γ(pullback (I.glueDataObjι U) (X.homOfLE ⋯), ⊤) : Type u))
    (((CommRingCat.Hom.hom
              (Iso.inv (ΓSpecIso Γ(X, (↑V : X.Opens))) ≫
                Hom.app (IsAffineOpen.isoSpec ⋯).hom ⊤ ≫
                  CategoryStruct.comp (Y := Γ((↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme), ⊤))
                    (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯)) :
                      Γ(X, (↑V : X.Opens).ι ''ᵁ ⊤) ⟶ Γ(X, ((↑U : X.Opens) ⊓ (↑V : X.Opens)).ι ''ᵁ ⊤))
                    (Hom.app F ⊤ :
                      Γ((↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme), ⊤) ⟶
                        Γ(pullback (I.glueDataObjι U) (X.homOfLE ⋯), F ⁻¹ᵁ ⊤))) :
            (↑Γ(X, (↑V : X.Opens)) : Type u) →+* (↑Γ(pullback (I.glueDataObjι U) (X.homOfLE ⋯), ⊤) : Type u)) :
          (a : (↑Γ(X, (↑V : X.Opens)) : Type u)) → (↑Γ(pullback (I.glueDataObjι U) (X.homOfLE ⋯), ⊤) : Type u))
        x :
      (↑Γ(pullback (I.glueDataObjι U) (X.homOfLE ⋯), ⊤) : Type u))
    (0 : (↑Γ(pullback (I.glueDataObjι U) (X.homOfLE ⋯), ⊤) : Type u))
have refine_1 : Eq (α := (↑Γ(pullback (I.glueDataObjι U) (X.homOfLE sorry), ⊤) : Type u))
  ((CommRingCat.Hom.hom
          (Hom.app (↑U : X.Opens).ι (↑V : X.Opens) ≫
            Hom.appLE (F ≫ X.homOfLE sorry) ((↑U : X.Opens).ι ⁻¹ᵁ (↑V : X.Opens)) ⊤ sorry) :
        (a : (↑Γ(X, (↑V : X.Opens)) : Type u)) → (↑Γ(pullback (I.glueDataObjι U) (X.homOfLE sorry), ⊤) : Type u))
      x :
    (↑Γ(pullback (I.glueDataObjι U) (X.homOfLE sorry), ⊤) : Type u))
  (0 : (↑Γ(pullback (I.glueDataObjι U) (X.homOfLE sorry), ⊤) : Type u))
Tactic: convert_to (U.1.ι.app V.1 ≫ (F ≫ X.homOfLE inf_le_left).appLE (U.1.ι ⁻¹ᵁ V.1) ⊤
      (by rw [← Scheme.Hom.comp_preimage, Category.assoc, X.homOfLE_ι]
          exact fun x _ ↦ by simpa using (F x).2.2)).hom x = 0 using 3
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X : Scheme
I : X.IdealSheafData
U V : (↑X.affineOpens : Type u)
F : pullback (Y := (↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme)) (I.glueDataObjι U) (X.homOfLE ⋯) ⟶
  (↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme) :=
  pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯)
x : (↑Γ(X, (↑V : X.Opens)) : Type u)
hx : x ∈ I.ideal V
⊢ Iso.inv (ΓSpecIso Γ(X, (↑V : X.Opens))) ≫
      Hom.app (IsAffineOpen.isoSpec ⋯).hom ⊤ ≫
        CategoryStruct.comp (Y := Γ((↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme), ⊤))
          (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯)) :
            Γ(X, (↑V : X.Opens).ι ''ᵁ ⊤) ⟶ Γ(X, ((↑U : X.Opens) ⊓ (↑V : X.Opens)).ι ''ᵁ ⊤))
          (Hom.app F ⊤ :
            Γ((↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme), ⊤) ⟶
              Γ(pullback (I.glueDataObjι U) (X.homOfLE ⋯), F ⁻¹ᵁ ⊤)) =
    Hom.app (↑U : X.Opens).ι (↑V : X.Opens) ≫ Hom.appLE (F ≫ X.homOfLE ⋯) ((↑U : X.Opens).ι ⁻¹ᵁ (↑V : X.Opens)) ⊤ ⋯
have h : Eq (α := Γ(X, (↑V : X.Opens)).Hom Γ(pullback (I.glueDataObjι U) (X.homOfLE sorry), ⊤))
  (Iso.inv (ΓSpecIso Γ(X, (↑V : X.Opens))) ≫
      Hom.app (IsAffineOpen.isoSpec sorry).hom ⊤ ≫
        CategoryStruct.comp (Y := Γ((↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme), ⊤))
          (X.presheaf.map (Quiver.Hom.op (homOfLE sorry)) :
            Γ(X, (↑V : X.Opens).ι ''ᵁ ⊤) ⟶ Γ(X, ((↑U : X.Opens) ⊓ (↑V : X.Opens)).ι ''ᵁ ⊤))
          (Hom.app F ⊤ :
            Γ((↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme), ⊤) ⟶
              Γ(pullback (I.glueDataObjι U) (X.homOfLE sorry), F ⁻¹ᵁ ⊤)) :
    Γ(X, (↑V : X.Opens)) ⟶ Γ(pullback (I.glueDataObjι U) (X.homOfLE sorry), ⊤))
  (CategoryStruct.comp (Y := Γ((↑(↑U : X.Opens) : Scheme), (↑U : X.Opens).ι ⁻¹ᵁ (↑V : X.Opens)))
      (X.presheaf.map (Quiver.Hom.op (homOfLE sorry)))
      (CategoryStruct.comp (Y :=
        Γ((↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme), X.homOfLE sorry ⁻¹ᵁ (↑U : X.Opens).ι ⁻¹ᵁ (↑V : X.Opens)))
        (X.presheaf.map (Quiver.Hom.op (homOfLE sorry)))
        (Hom.appLE F (X.homOfLE sorry ⁻¹ᵁ (↑U : X.Opens).ι ⁻¹ᵁ (↑V : X.Opens)) ⊤ sorry)) :
    Γ(X, (↑V : X.Opens)) ⟶ Γ(pullback (I.glueDataObjι U) (X.homOfLE sorry), ⊤))
Tactic: simp only [homOfLE_leOfHom, Opens.ι_app, Hom.comp_appLE, homOfLE_app]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X : Scheme
I : X.IdealSheafData
U V : (↑X.affineOpens : Type u)
F : pullback (Y := (↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme)) (I.glueDataObjι U) (X.homOfLE ⋯) ⟶
  (↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme) :=
  pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯)
x : (↑Γ(X, (↑V : X.Opens)) : Type u)
hx : x ∈ I.ideal V
⊢ LE.le (α := (↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme).Opens) ⊤
    (X.homOfLE ⋯ ⁻¹ᵁ (↑U : X.Opens).ι ⁻¹ᵁ (↑V : X.Opens))
have rw : ⊤ ≤ ((↑U : X.Opens) ⊓ (↑V : X.Opens)).ι ⁻¹ᵁ (↑V : X.Opens)
Tactic: rw [← Scheme.Hom.comp_preimage, X.homOfLE_ι]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (hypothesis)
Goal:
X : Scheme
I : X.IdealSheafData
U V : (↑X.affineOpens : Type u)
F : pullback (Y := (↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme)) (I.glueDataObjι U) (X.homOfLE ⋯) ⟶
  (↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme) :=
  pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯)
x : (↑Γ(X, (↑V : X.Opens)) : Type u)
hx : x ∈ I.ideal V
⊢ Eq (α := Γ(X, (↑V : X.Opens)).Hom Γ(pullback (I.glueDataObjι U) (X.homOfLE ⋯), ⊤))
    (Iso.inv (ΓSpecIso Γ(X, (↑V : X.Opens))) ≫
        Hom.app (IsAffineOpen.isoSpec ⋯).hom ⊤ ≫
          CategoryStruct.comp (Y := Γ((↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme), ⊤))
            (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯)) :
              Γ(X, (↑V : X.Opens).ι ''ᵁ ⊤) ⟶ Γ(X, ((↑U : X.Opens) ⊓ (↑V : X.Opens)).ι ''ᵁ ⊤))
            (Hom.app F ⊤ :
              Γ((↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme), ⊤) ⟶
                Γ(pullback (I.glueDataObjι U) (X.homOfLE ⋯), F ⁻¹ᵁ ⊤)) :
      Γ(X, (↑V : X.Opens)) ⟶ Γ(pullback (I.glueDataObjι U) (X.homOfLE ⋯), ⊤))
    (CategoryStruct.comp (Y := Γ((↑(↑U : X.Opens) : Scheme), (↑U : X.Opens).ι ⁻¹ᵁ (↑V : X.Opens)))
        (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯)))
        (CategoryStruct.comp (Y :=
          Γ((↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme), X.homOfLE ⋯ ⁻¹ᵁ (↑U : X.Opens).ι ⁻¹ᵁ (↑V : X.Opens)))
          (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯)))
          (Hom.appLE F (X.homOfLE ⋯ ⁻¹ᵁ (↑U : X.Opens).ι ⁻¹ᵁ (↑V : X.Opens)) ⊤ ⋯)) :
      Γ(X, (↑V : X.Opens)) ⟶ Γ(pullback (I.glueDataObjι U) (X.homOfLE ⋯), ⊤))
have H : LE.le (α := (↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme).Opens) ⊤ (X.homOfLE sorry ⁻¹ᵁ (↑U : X.Opens).ι ⁻¹ᵁ (↑V : X.Opens))
Tactic: have H : ⊤ ≤ X.homOfLE (inf_le_left (b := V.1)) ⁻¹ᵁ U.1.ι ⁻¹ᵁ V.1 := by
        rw [← Scheme.Hom.comp_preimage, X.homOfLE_ι]; exact fun x _ ↦ by simpa using x.2.2
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X : Scheme
I : X.IdealSheafData
U V : (↑X.affineOpens : Type u)
F : pullback (Y := (↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme)) (I.glueDataObjι U) (X.homOfLE ⋯) ⟶
  (↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme) :=
  pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯)
x : (↑Γ(X, (↑V : X.Opens)) : Type u)
hx : x ∈ I.ideal V
H :
  LE.le (α := (↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme).Opens) ⊤
    (X.homOfLE ⋯ ⁻¹ᵁ (↑U : X.Opens).ι ⁻¹ᵁ (↑V : X.Opens))
⊢ Eq (α := Γ(X, (↑V : X.Opens)).Hom Γ(pullback (I.glueDataObjι U) (X.homOfLE ⋯), ⊤))
    (Iso.inv (ΓSpecIso Γ(X, (↑V : X.Opens))) ≫
        Hom.app (IsAffineOpen.isoSpec ⋯).hom ⊤ ≫
          CategoryStruct.comp (Y := Γ((↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme), ⊤))
            (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯)) :
              Γ(X, (↑V : X.Opens).ι ''ᵁ ⊤) ⟶ Γ(X, ((↑U : X.Opens) ⊓ (↑V : X.Opens)).ι ''ᵁ ⊤))
            (Hom.app F ⊤ :
              Γ((↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme), ⊤) ⟶
                Γ(pullback (I.glueDataObjι U) (X.homOfLE ⋯), F ⁻¹ᵁ ⊤)) :
      Γ(X, (↑V : X.Opens)) ⟶ Γ(pullback (I.glueDataObjι U) (X.homOfLE ⋯), ⊤))
    (CategoryStruct.comp (Y := Γ((↑(↑U : X.Opens) : Scheme), (↑U : X.Opens).ι ⁻¹ᵁ (↑V : X.Opens)))
        (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯)))
        (CategoryStruct.comp (Y :=
          Γ((↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme), X.homOfLE ⋯ ⁻¹ᵁ (↑U : X.Opens).ι ⁻¹ᵁ (↑V : X.Opens)))
          (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯)))
          (Hom.appLE F (X.homOfLE ⋯ ⁻¹ᵁ (↑U : X.Opens).ι ⁻¹ᵁ (↑V : X.Opens)) ⊤ ⋯)) :
      Γ(X, (↑V : X.Opens)) ⟶ Γ(pullback (I.glueDataObjι U) (X.homOfLE ⋯), ⊤))
have h : Eq (α := Γ(X, (↑V : X.Opens)).Hom Γ(pullback (I.glueDataObjι U) (X.homOfLE sorry), ⊤))
  (Iso.inv (ΓSpecIso Γ(X, (↑V : X.Opens))) ≫
      Hom.app (IsAffineOpen.isoSpec sorry).hom ⊤ ≫
        CategoryStruct.comp (Y := Γ((↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme), ⊤))
          (X.presheaf.map (Quiver.Hom.op (homOfLE sorry)) :
            Γ(X, (↑V : X.Opens).ι ''ᵁ ⊤) ⟶ Γ(X, ((↑U : X.Opens) ⊓ (↑V : X.Opens)).ι ''ᵁ ⊤))
          (Hom.app F ⊤ :
            Γ((↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme), ⊤) ⟶
              Γ(pullback (I.glueDataObjι U) (X.homOfLE sorry), F ⁻¹ᵁ ⊤)) :
    Γ(X, (↑V : X.Opens)) ⟶ Γ(pullback (I.glueDataObjι U) (X.homOfLE sorry), ⊤))
  (X.presheaf.map (Quiver.Hom.op (homOfLE sorry)) ≫
      X.presheaf.map (Quiver.Hom.op (homOfLE sorry)) ≫
        (↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme).presheaf.map (homOfLE H).op ≫ Hom.appLE F ⊤ ⊤ sorry :
    Γ(X, (↑V : X.Opens)) ⟶ Γ(pullback (I.glueDataObjι U) (X.homOfLE sorry), ⊤))
Tactic: rw [← F.map_appLE (show ⊤ ≤ F ⁻¹ᵁ ⊤ from le_rfl) (homOfLE H).op]