awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
Goal:
X : Scheme
I : X.IdealSheafData
Z : Closeds ↥X
U : (↑X.affineOpens : Type u)
f : (↑Γ(X, (↑U : X.Opens)) : Type u)
F : Γ(X, (↑U : X.Opens)) ⟶ Γ(X, X.basicOpen f) := X.presheaf.map (homOfLE ⋯).op
⊢ Eq (α := Ideal (↑Γ(X, X.basicOpen f) : Type u))
    (Ideal.map (R := (↑Γ(X, (↑U : X.Opens)) : Type u)) (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op))
      ((fun (U : (↑X.affineOpens : Type u)) ↦
          (PrimeSpectrum.vanishingIdeal (⇑(IsAffineOpen.fromSpec ⋯) ⁻¹' (↑Z : Set ↥X)) :
            Ideal (↑Γ(X, (↑U : X.Opens)) : Type u)))
        U))
    ((fun (U : (↑X.affineOpens : Type u)) ↦
        (PrimeSpectrum.vanishingIdeal (⇑(IsAffineOpen.fromSpec ⋯) ⁻¹' (↑Z : Set ↥X)) :
          Ideal (↑Γ(X, (↑U : X.Opens)) : Type u)))
      (X.affineBasicOpen f))
have a : LE.le (α := Ideal (↑Γ(X, X.basicOpen f) : Type u))
  (Ideal.map (R := (↑Γ(X, (↑U : X.Opens)) : Type u)) (CommRingCat.Hom.hom (X.presheaf.map (homOfLE sorry).op))
    ((fun (U : (↑X.affineOpens : Type u)) ↦
        (PrimeSpectrum.vanishingIdeal (⇑(IsAffineOpen.fromSpec sorry) ⁻¹' (↑Z : Set ↥X)) :
          Ideal (↑Γ(X, (↑U : X.Opens)) : Type u)))
      U))
  ((fun (U : (↑X.affineOpens : Type u)) ↦
      (PrimeSpectrum.vanishingIdeal (⇑(IsAffineOpen.fromSpec sorry) ⁻¹' (↑Z : Set ↥X)) :
        Ideal (↑Γ(X, (↑U : X.Opens)) : Type u)))
    (X.affineBasicOpen f))
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
Goal:
X : Scheme
I : X.IdealSheafData
Z : Closeds ↥X
U : (↑X.affineOpens : Type u)
f : (↑Γ(X, (↑U : X.Opens)) : Type u)
F : Γ(X, (↑U : X.Opens)) ⟶ Γ(X, X.basicOpen f) := X.presheaf.map (homOfLE ⋯).op
a :
  LE.le (α := Ideal (↑Γ(X, X.basicOpen f) : Type u))
    (Ideal.map (R := (↑Γ(X, (↑U : X.Opens)) : Type u)) (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op))
      ((fun (U : (↑X.affineOpens : Type u)) ↦
          (PrimeSpectrum.vanishingIdeal (⇑(IsAffineOpen.fromSpec ⋯) ⁻¹' (↑Z : Set ↥X)) :
            Ideal (↑Γ(X, (↑U : X.Opens)) : Type u)))
        U))
    ((fun (U : (↑X.affineOpens : Type u)) ↦
        (PrimeSpectrum.vanishingIdeal (⇑(IsAffineOpen.fromSpec ⋯) ⁻¹' (↑Z : Set ↥X)) :
          Ideal (↑Γ(X, (↑U : X.Opens)) : Type u)))
      (X.affineBasicOpen f))
⊢ Eq (α := Ideal (↑Γ(X, X.basicOpen f) : Type u))
    (Ideal.map (R := (↑Γ(X, (↑U : X.Opens)) : Type u)) (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op))
      ((fun (U : (↑X.affineOpens : Type u)) ↦
          (PrimeSpectrum.vanishingIdeal (⇑(IsAffineOpen.fromSpec ⋯) ⁻¹' (↑Z : Set ↥X)) :
            Ideal (↑Γ(X, (↑U : X.Opens)) : Type u)))
        U))
    ((fun (U : (↑X.affineOpens : Type u)) ↦
        (PrimeSpectrum.vanishingIdeal (⇑(IsAffineOpen.fromSpec ⋯) ⁻¹' (↑Z : Set ↥X)) :
          Ideal (↑Γ(X, (↑U : X.Opens)) : Type u)))
      (X.affineBasicOpen f))
have a₁ : LE.le (α := Ideal (↑Γ(X, X.basicOpen f) : Type u))
  ((fun (U : (↑X.affineOpens : Type u)) ↦
      (PrimeSpectrum.vanishingIdeal (⇑(IsAffineOpen.fromSpec sorry) ⁻¹' (↑Z : Set ↥X)) :
        Ideal (↑Γ(X, (↑U : X.Opens)) : Type u)))
    (X.affineBasicOpen f))
  (Ideal.map (R := (↑Γ(X, (↑U : X.Opens)) : Type u)) (CommRingCat.Hom.hom (X.presheaf.map (homOfLE sorry).op))
    ((fun (U : (↑X.affineOpens : Type u)) ↦
        (PrimeSpectrum.vanishingIdeal (⇑(IsAffineOpen.fromSpec sorry) ⁻¹' (↑Z : Set ↥X)) :
          Ideal (↑Γ(X, (↑U : X.Opens)) : Type u)))
      U))
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
Goal:
X : Scheme
I : X.IdealSheafData
Z : Closeds ↥X
U : (↑X.affineOpens : Type u)
f : (↑Γ(X, (↑U : X.Opens)) : Type u)
F : Γ(X, (↑U : X.Opens)) ⟶ Γ(X, X.basicOpen f) := X.presheaf.map (homOfLE ⋯).op
⊢ LE.le (α := Ideal (↑Γ(X, X.basicOpen f) : Type u))
    (Ideal.map (R := (↑Γ(X, (↑U : X.Opens)) : Type u)) (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op))
      ((fun (U : (↑X.affineOpens : Type u)) ↦
          (PrimeSpectrum.vanishingIdeal (⇑(IsAffineOpen.fromSpec ⋯) ⁻¹' (↑Z : Set ↥X)) :
            Ideal (↑Γ(X, (↑U : X.Opens)) : Type u)))
        U))
    ((fun (U : (↑X.affineOpens : Type u)) ↦
        (PrimeSpectrum.vanishingIdeal (⇑(IsAffineOpen.fromSpec ⋯) ⁻¹' (↑Z : Set ↥X)) :
          Ideal (↑Γ(X, (↑U : X.Opens)) : Type u)))
      (X.affineBasicOpen f))
have a : LE.le (α := Ideal (↑Γ(X, (↑U : X.Opens)) : Type u))
  ((fun (U : (↑X.affineOpens : Type u)) ↦
      (PrimeSpectrum.vanishingIdeal (⇑(IsAffineOpen.fromSpec sorry) ⁻¹' (↑Z : Set ↥X)) :
        Ideal (↑Γ(X, (↑U : X.Opens)) : Type u)))
    U)
  (Ideal.comap (CommRingCat.Hom.hom (X.presheaf.map (homOfLE sorry).op))
    ((fun (U : (↑X.affineOpens : Type u)) ↦
        (PrimeSpectrum.vanishingIdeal (⇑(IsAffineOpen.fromSpec sorry) ⁻¹' (↑Z : Set ↥X)) :
          Ideal (↑Γ(X, (↑U : X.Opens)) : Type u)))
      (X.affineBasicOpen f)))
Tactic: rw [Ideal.map_le_iff_le_comap]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
Goal:
X : Scheme
I : X.IdealSheafData
Z : Closeds ↥X
U : (↑X.affineOpens : Type u)
f : (↑Γ(X, (↑U : X.Opens)) : Type u)
F : Γ(X, (↑U : X.Opens)) ⟶ Γ(X, X.basicOpen f) := X.presheaf.map (homOfLE ⋯).op
x : (↑Γ(X, (↑U : X.Opens)) : Type u)
hx :
  Membership.mem (γ := Submodule (↑Γ(X, (↑U : X.Opens)) : Type u) (↑Γ(X, (↑U : X.Opens)) : Type u))
    ((fun (U : (↑X.affineOpens : Type u)) ↦
        (PrimeSpectrum.vanishingIdeal (⇑(IsAffineOpen.fromSpec ⋯) ⁻¹' (↑Z : Set ↥X)) :
          Ideal (↑Γ(X, (↑U : X.Opens)) : Type u)))
      U)
    x
⊢ Membership.mem (γ := Submodule (↑Γ(X, (↑U : X.Opens)) : Type u) (↑Γ(X, (↑U : X.Opens)) : Type u))
    (Ideal.comap (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op))
      ((fun (U : (↑X.affineOpens : Type u)) ↦
          (PrimeSpectrum.vanishingIdeal (⇑(IsAffineOpen.fromSpec ⋯) ⁻¹' (↑Z : Set ↥X)) :
            Ideal (↑Γ(X, (↑U : X.Opens)) : Type u)))
        (X.affineBasicOpen f)))
    x
have a : ∀ (p : ↥(Spec Γ(X, (↑(X.affineBasicOpen f) : X.Opens)))),
  Membership.mem (α := ↥X) Z ((IsAffineOpen.fromSpec sorry) p : ↥X) →
    Membership.mem (α := (↑Γ(X, X.basicOpen f) : Type u)) p.asIdeal
      ((CommRingCat.Hom.hom F : (a : (↑Γ(X, (↑U : X.Opens)) : Type u)) → (↑Γ(X, X.basicOpen f) : Type u)) x :
        (↑Γ(X, X.basicOpen f) : Type u))
Tactic: suffices ∀ p, (X.affineBasicOpen f).2.fromSpec p ∈ Z → F.hom x ∈ p.asIdeal by
          simpa [PrimeSpectrum.mem_vanishingIdeal] using this
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
Goal:
X : Scheme
I : X.IdealSheafData
Z : Closeds ↥X
U : (↑X.affineOpens : Type u)
f : (↑Γ(X, (↑U : X.Opens)) : Type u)
F : Γ(X, (↑U : X.Opens)) ⟶ Γ(X, X.basicOpen f) := X.presheaf.map (homOfLE ⋯).op
x_1 : (↑Γ(X, (↑U : X.Opens)) : Type u)
hx :
  Membership.mem (γ := Submodule (↑Γ(X, (↑U : X.Opens)) : Type u) (↑Γ(X, (↑U : X.Opens)) : Type u))
    ((fun (U : (↑X.affineOpens : Type u)) ↦
        (PrimeSpectrum.vanishingIdeal (⇑(IsAffineOpen.fromSpec ⋯) ⁻¹' (↑Z : Set ↥X)) :
          Ideal (↑Γ(X, (↑U : X.Opens)) : Type u)))
      U)
    x_1
x : ↥(Spec Γ(X, (↑(X.affineBasicOpen f) : X.Opens)))
hxZ : Membership.mem (α := ↥X) Z ((IsAffineOpen.fromSpec ⋯) x : ↥X)
⊢ Membership.mem (α := (↑Γ(X, X.basicOpen f) : Type u)) x.asIdeal
    ((CommRingCat.Hom.hom F : (a : (↑Γ(X, (↑U : X.Opens)) : Type u)) → (↑Γ(X, X.basicOpen f) : Type u)) x_1 :
      (↑Γ(X, X.basicOpen f) : Type u))
have a : Membership.mem (α := PrimeSpectrum (↑Γ(X, (↑U : X.Opens)) : Type u)) (γ :=
  Set (PrimeSpectrum (↑Γ(X, (↑U : X.Opens)) : Type u))) (⇑(IsAffineOpen.fromSpec sorry) ⁻¹' (↑Z : Set ↥X))
  ((Spec.map (X.presheaf.map (homOfLE sorry).op)) x : ↥(Spec (X.presheaf.obj (Opposite.op (↑U : X.Opens)))))
Tactic: refine (PrimeSpectrum.mem_vanishingIdeal _ _).mp hx
          (Spec.map (X.presheaf.map (homOfLE _).op) x) ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
Goal:
X : Scheme
I : X.IdealSheafData
Z : Closeds ↥X
U : (↑X.affineOpens : Type u)
f : (↑Γ(X, (↑U : X.Opens)) : Type u)
F : Γ(X, (↑U : X.Opens)) ⟶ Γ(X, X.basicOpen f) := X.presheaf.map (homOfLE ⋯).op
x_1 : (↑Γ(X, (↑U : X.Opens)) : Type u)
hx :
  Membership.mem (γ := Submodule (↑Γ(X, (↑U : X.Opens)) : Type u) (↑Γ(X, (↑U : X.Opens)) : Type u))
    ((fun (U : (↑X.affineOpens : Type u)) ↦
        (PrimeSpectrum.vanishingIdeal (⇑(IsAffineOpen.fromSpec ⋯) ⁻¹' (↑Z : Set ↥X)) :
          Ideal (↑Γ(X, (↑U : X.Opens)) : Type u)))
      U)
    x_1
x : ↥(Spec Γ(X, (↑(X.affineBasicOpen f) : X.Opens)))
hxZ : Membership.mem (α := ↥X) Z ((IsAffineOpen.fromSpec ⋯) x : ↥X)
⊢ Membership.mem (α := PrimeSpectrum (↑Γ(X, (↑U : X.Opens)) : Type u)) (γ :=
    Set (PrimeSpectrum (↑Γ(X, (↑U : X.Opens)) : Type u))) (⇑(IsAffineOpen.fromSpec ⋯) ⁻¹' (↑Z : Set ↥X))
    ((Spec.map (X.presheaf.map (homOfLE ⋯).op)) x : ↥(Spec (X.presheaf.obj (Opposite.op (↑U : X.Opens)))))
have a : Membership.mem (α := ↥X) (↑Z : Set ↥X)
  ((IsAffineOpen.fromSpec sorry)
      ((Spec.map (X.presheaf.map (homOfLE sorry).op)) x : ↥(Spec (X.presheaf.obj (Opposite.op (↑U : X.Opens))))) :
    ↥X)
Tactic: rwa [Set.mem_preimage, ← Scheme.Hom.comp_apply,
          IsAffineOpen.map_fromSpec _ (X.affineBasicOpen f).2]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
Goal:
X : Scheme
I : X.IdealSheafData
Z : Closeds ↥X
U : (↑X.affineOpens : Type u)
f : (↑Γ(X, (↑U : X.Opens)) : Type u)
F : Γ(X, (↑U : X.Opens)) ⟶ Γ(X, X.basicOpen f) := X.presheaf.map (homOfLE ⋯).op
x_1 : (↑Γ(X, (↑U : X.Opens)) : Type u)
hx :
  Membership.mem (γ := Submodule (↑Γ(X, (↑U : X.Opens)) : Type u) (↑Γ(X, (↑U : X.Opens)) : Type u))
    ((fun (U : (↑X.affineOpens : Type u)) ↦
        (PrimeSpectrum.vanishingIdeal (⇑(IsAffineOpen.fromSpec ⋯) ⁻¹' (↑Z : Set ↥X)) :
          Ideal (↑Γ(X, (↑U : X.Opens)) : Type u)))
      U)
    x_1
x : ↥(Spec Γ(X, (↑(X.affineBasicOpen f) : X.Opens)))
hxZ : Membership.mem (α := ↥X) Z ((IsAffineOpen.fromSpec ⋯) x : ↥X)
a :
  Membership.mem (α := ↥X) (↑Z : Set ↥X)
    ((IsAffineOpen.fromSpec ⋯)
        ((Spec.map (X.presheaf.map (homOfLE ⋯).op)) x : ↥(Spec (X.presheaf.obj (Opposite.op (↑U : X.Opens))))) :
      ↥X)
⊢ Membership.mem (α := PrimeSpectrum (↑Γ(X, (↑U : X.Opens)) : Type u)) (γ :=
    Set (PrimeSpectrum (↑Γ(X, (↑U : X.Opens)) : Type u))) (⇑(IsAffineOpen.fromSpec ⋯) ⁻¹' (↑Z : Set ↥X))
    ((Spec.map (X.presheaf.map (homOfLE ⋯).op)) x : ↥(Spec (X.presheaf.obj (Opposite.op (↑U : X.Opens)))))
have a₁ : Membership.mem (α := ↥X) (↑Z : Set ↥X) ((Spec.map (X.presheaf.map (homOfLE sorry).op) ≫ IsAffineOpen.fromSpec sorry) x : ↥X)
Tactic: rwa [Set.mem_preimage, ← Scheme.Hom.comp_apply,
          IsAffineOpen.map_fromSpec _ (X.affineBasicOpen f).2]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
Goal:
X : Scheme
I : X.IdealSheafData
Z : Closeds ↥X
U : (↑X.affineOpens : Type u)
f : (↑Γ(X, (↑U : X.Opens)) : Type u)
F : Γ(X, (↑U : X.Opens)) ⟶ Γ(X, X.basicOpen f) := X.presheaf.map (homOfLE ⋯).op
x_1 : (↑Γ(X, (↑U : X.Opens)) : Type u)
hx :
  Membership.mem (γ := Submodule (↑Γ(X, (↑U : X.Opens)) : Type u) (↑Γ(X, (↑U : X.Opens)) : Type u))
    ((fun (U : (↑X.affineOpens : Type u)) ↦
        (PrimeSpectrum.vanishingIdeal (⇑(IsAffineOpen.fromSpec ⋯) ⁻¹' (↑Z : Set ↥X)) :
          Ideal (↑Γ(X, (↑U : X.Opens)) : Type u)))
      U)
    x_1
x : ↥(Spec Γ(X, (↑(X.affineBasicOpen f) : X.Opens)))
hxZ : Membership.mem (α := ↥X) Z ((IsAffineOpen.fromSpec ⋯) x : ↥X)
a :
  Membership.mem (α := ↥X) (↑Z : Set ↥X)
    ((IsAffineOpen.fromSpec ⋯)
        ((Spec.map (X.presheaf.map (homOfLE ⋯).op)) x : ↥(Spec (X.presheaf.obj (Opposite.op (↑U : X.Opens))))) :
      ↥X)
a₁ :
  Membership.mem (α := ↥X) (↑Z : Set ↥X) ((Spec.map (X.presheaf.map (homOfLE ⋯).op) ≫ IsAffineOpen.fromSpec ⋯) x : ↥X)
⊢ Membership.mem (α := PrimeSpectrum (↑Γ(X, (↑U : X.Opens)) : Type u)) (γ :=
    Set (PrimeSpectrum (↑Γ(X, (↑U : X.Opens)) : Type u))) (⇑(IsAffineOpen.fromSpec ⋯) ⁻¹' (↑Z : Set ↥X))
    ((Spec.map (X.presheaf.map (homOfLE ⋯).op)) x : ↥(Spec (X.presheaf.obj (Opposite.op (↑U : X.Opens)))))
have a₂ : Membership.mem (α := ↥X) (↑Z : Set ↥X) ((IsAffineOpen.fromSpec sorry) x : ↥X)
Tactic: rwa [Set.mem_preimage, ← Scheme.Hom.comp_apply,
          IsAffineOpen.map_fromSpec _ (X.affineBasicOpen f).2]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (hypothesis)
Goal:
X : Scheme
I : X.IdealSheafData
Z : Closeds ↥X
U : (↑X.affineOpens : Type u)
f : (↑Γ(X, (↑U : X.Opens)) : Type u)
F : Γ(X, (↑U : X.Opens)) ⟶ Γ(X, X.basicOpen f) := X.presheaf.map (homOfLE ⋯).op
this : Algebra (↑Γ(X, (↑U : X.Opens)) : Type u) (↑Γ(X, (↑(X.affineBasicOpen f) : X.Opens)) : Type u) :=
  (CommRingCat.Hom.hom F).toAlgebra
⊢ LE.le (α := Ideal (↑Γ(X, X.basicOpen f) : Type u))
    ((fun (U : (↑X.affineOpens : Type u)) ↦
        (PrimeSpectrum.vanishingIdeal (⇑(IsAffineOpen.fromSpec ⋯) ⁻¹' (↑Z : Set ↥X)) :
          Ideal (↑Γ(X, (↑U : X.Opens)) : Type u)))
      (X.affineBasicOpen f))
    (Ideal.map (R := (↑Γ(X, (↑U : X.Opens)) : Type u)) (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op))
      ((fun (U : (↑X.affineOpens : Type u)) ↦
          (PrimeSpectrum.vanishingIdeal (⇑(IsAffineOpen.fromSpec ⋯) ⁻¹' (↑Z : Set ↥X)) :
            Ideal (↑Γ(X, (↑U : X.Opens)) : Type u)))
        U))
have this₁ : IsLocalization.Away f (↑Γ(X, X.basicOpen f) : Type u)
Tactic: have : IsLocalization.Away f Γ(X, X.basicOpen f) :=
          U.2.isLocalization_of_eq_basicOpen _ _ rfl
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (hypothesis)
Goal:
X : Scheme
I : X.IdealSheafData
Z : Closeds ↥X
U : (↑X.affineOpens : Type u)
f : (↑Γ(X, (↑U : X.Opens)) : Type u)
F : Γ(X, (↑U : X.Opens)) ⟶ Γ(X, X.basicOpen f) := X.presheaf.map (homOfLE ⋯).op
this_1 : Algebra (↑Γ(X, (↑U : X.Opens)) : Type u) (↑Γ(X, (↑(X.affineBasicOpen f) : X.Opens)) : Type u) :=
  (CommRingCat.Hom.hom F).toAlgebra
this : IsLocalization.Away f (↑Γ(X, X.basicOpen f) : Type u)
x : (↑Γ(X, X.basicOpen f) : Type u)
hx :
  Membership.mem (γ := Submodule (↑Γ(X, X.basicOpen f) : Type u) (↑Γ(X, X.basicOpen f) : Type u))
    (PrimeSpectrum.vanishingIdeal (⇑(IsAffineOpen.fromSpec ⋯) ⁻¹' (↑Z : Set ↥X))) x
⊢ Membership.mem (γ := Submodule (↑Γ(X, X.basicOpen f) : Type u) (↑Γ(X, X.basicOpen f) : Type u))
    (Ideal.map (R := (↑Γ(X, (↑U : X.Opens)) : Type u)) (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op))
      (PrimeSpectrum.vanishingIdeal (⇑(IsAffineOpen.fromSpec ⋯) ⁻¹' (↑Z : Set ↥X))))
    x
have this₁ : Topology.IsOpenEmbedding (X := ↥(Spec Γ(X, X.basicOpen f))) (Y := ↥(Spec Γ(X, (↑U : X.Opens)))) ⇑(Spec.map F)
Tactic: have : Topology.IsOpenEmbedding (Spec.map F) :=
          localization_away_isOpenEmbedding Γ(X, X.basicOpen f) f
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (hypothesis)
Goal:
X : Scheme
I : X.IdealSheafData
Z : Closeds ↥X
U : (↑X.affineOpens : Type u)
f : (↑Γ(X, (↑U : X.Opens)) : Type u)
F : Γ(X, (↑U : X.Opens)) ⟶ Γ(X, X.basicOpen f) := X.presheaf.map (homOfLE ⋯).op
this_1 : Algebra (↑Γ(X, (↑U : X.Opens)) : Type u) (↑Γ(X, (↑(X.affineBasicOpen f) : X.Opens)) : Type u) :=
  (CommRingCat.Hom.hom F).toAlgebra
this_2 : IsLocalization.Away f (↑Γ(X, X.basicOpen f) : Type u)
x : (↑Γ(X, X.basicOpen f) : Type u)
hx :
  Membership.mem (γ := Submodule (↑Γ(X, X.basicOpen f) : Type u) (↑Γ(X, X.basicOpen f) : Type u))
    (PrimeSpectrum.vanishingIdeal (⇑(IsAffineOpen.fromSpec ⋯) ⁻¹' (↑Z : Set ↥X))) x
this : Topology.IsOpenEmbedding (X := ↥(Spec Γ(X, X.basicOpen f))) (Y := ↥(Spec Γ(X, (↑U : X.Opens)))) ⇑(Spec.map F)
⊢ Membership.mem (γ := Submodule (↑Γ(X, X.basicOpen f) : Type u) (↑Γ(X, X.basicOpen f) : Type u))
    (Ideal.map (R := (↑Γ(X, (↑U : X.Opens)) : Type u)) (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op))
      (PrimeSpectrum.vanishingIdeal (⇑(IsAffineOpen.fromSpec ⋯) ⁻¹' (↑Z : Set ↥X))))
    x
have hx₁ : Membership.mem (γ := Submodule (↑Γ(X, X.basicOpen f) : Type u) (↑Γ(X, X.basicOpen f) : Type u))
  (PrimeSpectrum.vanishingIdeal
    (Set.preimage (β := ↥(Spec Γ(X, (↑U : X.Opens)))) (⇑(Spec.map (X.presheaf.map (homOfLE sorry).op)))
      (⇑(IsAffineOpen.fromSpec sorry) ⁻¹' (↑Z : Set ↥X))))
  x
Tactic: rw [← U.2.map_fromSpec (X.affineBasicOpen f).2 (homOfLE (X.basicOpen_le f)).op,
          Scheme.Hom.comp_base, TopCat.coe_comp, Set.preimage_comp] at hx
Cleared hypotheses: hx, this
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
Goal:
X : Scheme
I : X.IdealSheafData
Z : Closeds ↥X
U : (↑X.affineOpens : Type u)
f : (↑Γ(X, (↑U : X.Opens)) : Type u)
F : Γ(X, (↑U : X.Opens)) ⟶ Γ(X, X.basicOpen f) := X.presheaf.map (homOfLE ⋯).op
this_1 : Algebra (↑Γ(X, (↑U : X.Opens)) : Type u) (↑Γ(X, (↑(X.affineBasicOpen f) : X.Opens)) : Type u) :=
  (CommRingCat.Hom.hom F).toAlgebra
this_2 : IsLocalization.Away f (↑Γ(X, X.basicOpen f) : Type u)
x : (↑Γ(X, X.basicOpen f) : Type u)
hx :
  Membership.mem (γ := Submodule (↑Γ(X, X.basicOpen f) : Type u) (↑Γ(X, X.basicOpen f) : Type u))
    (PrimeSpectrum.vanishingIdeal
      (Set.preimage (β := ↥(Spec Γ(X, (↑U : X.Opens)))) (⇑(Spec.map (X.presheaf.map (homOfLE ⋯).op)))
        (⇑(IsAffineOpen.fromSpec ⋯) ⁻¹' (↑Z : Set ↥X))))
    x
this : Topology.IsOpenEmbedding (X := ↥(Spec Γ(X, X.basicOpen f))) (Y := ↥(Spec Γ(X, (↑U : X.Opens)))) ⇑(Spec.map F)
⊢ Membership.mem (γ := Submodule (↑Γ(X, X.basicOpen f) : Type u) (↑Γ(X, X.basicOpen f) : Type u))
    (Ideal.map (R := (↑Γ(X, (↑U : X.Opens)) : Type u)) (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op))
      (PrimeSpectrum.vanishingIdeal (⇑(IsAffineOpen.fromSpec ⋯) ⁻¹' (↑Z : Set ↥X))))
    x
have a : ∀ (Z' : Set ↥(Spec Γ(X, (↑U : X.Opens))))
  (hx :
    Membership.mem (γ := Submodule (↑Γ(X, X.basicOpen f) : Type u) (↑Γ(X, X.basicOpen f) : Type u))
      (PrimeSpectrum.vanishingIdeal (⇑(Spec.map (X.presheaf.map (homOfLE sorry).op)) ⁻¹' Z')) x),
  Membership.mem (γ := Submodule (↑Γ(X, X.basicOpen f) : Type u) (↑Γ(X, X.basicOpen f) : Type u))
    (Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE sorry).op)) (PrimeSpectrum.vanishingIdeal Z')) x
Tactic: generalize U.2.fromSpec ⁻¹' Z = Z' at hx ⊢
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (hypothesis)
Goal:
X : Scheme
I : X.IdealSheafData
Z : Closeds ↥X
U : (↑X.affineOpens : Type u)
f : (↑Γ(X, (↑U : X.Opens)) : Type u)
F : Γ(X, (↑U : X.Opens)) ⟶ Γ(X, X.basicOpen f) := X.presheaf.map (homOfLE ⋯).op
this_1 : Algebra (↑Γ(X, (↑U : X.Opens)) : Type u) (↑Γ(X, (↑(X.affineBasicOpen f) : X.Opens)) : Type u) :=
  (CommRingCat.Hom.hom F).toAlgebra
this_2 : IsLocalization.Away f (↑Γ(X, X.basicOpen f) : Type u)
x : (↑Γ(X, X.basicOpen f) : Type u)
this : Topology.IsOpenEmbedding (X := ↥(Spec Γ(X, X.basicOpen f))) (Y := ↥(Spec Γ(X, (↑U : X.Opens)))) ⇑(Spec.map F)
Z' : Set ↥(Spec Γ(X, (↑U : X.Opens)))
hx :
  Membership.mem (γ := Submodule (↑Γ(X, X.basicOpen f) : Type u) (↑Γ(X, X.basicOpen f) : Type u))
    (PrimeSpectrum.vanishingIdeal (⇑(Spec.map (X.presheaf.map (homOfLE ⋯).op)) ⁻¹' Z')) x
⊢ Membership.mem (γ := Submodule (↑Γ(X, X.basicOpen f) : Type u) (↑Γ(X, X.basicOpen f) : Type u))
    (Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) (PrimeSpectrum.vanishingIdeal Z')) x
have hx₁ : Membership.mem (γ := Ideal (↑Γ(X, X.basicOpen f) : Type u)) (PrimeSpectrum.vanishingIdeal (⇑(Spec.map F) ⁻¹' Z')) x
Tactic: replace hx : x ∈ vanishingIdeal (Spec.map F ⁻¹' Z') := hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
Goal:
X : Scheme
I : X.IdealSheafData
Z : Closeds ↥X
U : (↑X.affineOpens : Type u)
f : (↑Γ(X, (↑U : X.Opens)) : Type u)
F : Γ(X, (↑U : X.Opens)) ⟶ Γ(X, X.basicOpen f) := X.presheaf.map (homOfLE ⋯).op
this_1 : Algebra (↑Γ(X, (↑U : X.Opens)) : Type u) (↑Γ(X, (↑(X.affineBasicOpen f) : X.Opens)) : Type u) :=
  (CommRingCat.Hom.hom F).toAlgebra
this_2 : IsLocalization.Away f (↑Γ(X, X.basicOpen f) : Type u)
x : (↑Γ(X, X.basicOpen f) : Type u)
this : Topology.IsOpenEmbedding (X := ↥(Spec Γ(X, X.basicOpen f))) (Y := ↥(Spec Γ(X, (↑U : X.Opens)))) ⇑(Spec.map F)
Z' : Set ↥(Spec Γ(X, (↑U : X.Opens)))
hx : Membership.mem (γ := Ideal (↑Γ(X, X.basicOpen f) : Type u)) (PrimeSpectrum.vanishingIdeal (⇑(Spec.map F) ⁻¹' Z')) x
⊢ Membership.mem (γ := Submodule (↑Γ(X, X.basicOpen f) : Type u) (↑Γ(X, X.basicOpen f) : Type u))
    (Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) (PrimeSpectrum.vanishingIdeal Z')) x
have a : ∀ (I : Ideal (↑Γ(X, (↑U : X.Opens)) : Type u)) (hI : I.IsRadical)
  (e : closure Z' = PrimeSpectrum.zeroLocus (↑I : Set (↑Γ(X, (↑U : X.Opens)) : Type u))),
  Membership.mem (γ := Submodule (↑Γ(X, X.basicOpen f) : Type u) (↑Γ(X, X.basicOpen f) : Type u))
    (Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE sorry).op)) (PrimeSpectrum.vanishingIdeal Z')) x
Tactic: obtain ⟨I, hI, e⟩ :=
          (isClosed_iff_zeroLocus_radical_ideal _).mp (isClosed_closure (s := Z'))
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
Goal:
X : Scheme
I_1 : X.IdealSheafData
Z : Closeds ↥X
U : (↑X.affineOpens : Type u)
f : (↑Γ(X, (↑U : X.Opens)) : Type u)
F : Γ(X, (↑U : X.Opens)) ⟶ Γ(X, X.basicOpen f) := X.presheaf.map (homOfLE ⋯).op
this_1 : Algebra (↑Γ(X, (↑U : X.Opens)) : Type u) (↑Γ(X, (↑(X.affineBasicOpen f) : X.Opens)) : Type u) :=
  (CommRingCat.Hom.hom F).toAlgebra
this_2 : IsLocalization.Away f (↑Γ(X, X.basicOpen f) : Type u)
x : (↑Γ(X, X.basicOpen f) : Type u)
this : Topology.IsOpenEmbedding (X := ↥(Spec Γ(X, X.basicOpen f))) (Y := ↥(Spec Γ(X, (↑U : X.Opens)))) ⇑(Spec.map F)
Z' : Set ↥(Spec Γ(X, (↑U : X.Opens)))
hx : Membership.mem (γ := Ideal (↑Γ(X, X.basicOpen f) : Type u)) (PrimeSpectrum.vanishingIdeal (⇑(Spec.map F) ⁻¹' Z')) x
I : Ideal (↑Γ(X, (↑U : X.Opens)) : Type u)
hI : I.IsRadical
e : closure Z' = PrimeSpectrum.zeroLocus (↑I : Set (↑Γ(X, (↑U : X.Opens)) : Type u))
⊢ Membership.mem (γ := Submodule (↑Γ(X, X.basicOpen f) : Type u) (↑Γ(X, X.basicOpen f) : Type u))
    (Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) (PrimeSpectrum.vanishingIdeal Z')) x
have a : ∀ (I : Ideal (↑Γ(X, (↑U : X.Opens)) : Type u))
  (hx :
    Membership.mem (γ := Ideal (↑Γ(X, X.basicOpen f) : Type u))
      (PrimeSpectrum.vanishingIdeal
        (Set.preimage (β := ↥(Spec Γ(X, (↑U : X.Opens)))) (⇑(Spec.map F))
          (PrimeSpectrum.zeroLocus (↑I : Set (↑Γ(X, (↑U : X.Opens)) : Type u)))))
      x)
  (hI : I.IsRadical) (e : closure Z' = PrimeSpectrum.zeroLocus (↑I : Set (↑Γ(X, (↑U : X.Opens)) : Type u))),
  Membership.mem (γ := Submodule (↑Γ(X, X.basicOpen f) : Type u) (↑Γ(X, X.basicOpen f) : Type u))
    (Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE sorry).op)) (PrimeSpectrum.vanishingIdeal Z')) x
Tactic: rw [← vanishingIdeal_closure,
          ← this.isOpenMap.preimage_closure_eq_closure_preimage this.continuous, e] at hx
Cleared hypotheses: hx, I, hI, e
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
Goal:
X : Scheme
I_1 : X.IdealSheafData
Z : Closeds ↥X
U : (↑X.affineOpens : Type u)
f : (↑Γ(X, (↑U : X.Opens)) : Type u)
F : Γ(X, (↑U : X.Opens)) ⟶ Γ(X, X.basicOpen f) := X.presheaf.map (homOfLE ⋯).op
this_1 : Algebra (↑Γ(X, (↑U : X.Opens)) : Type u) (↑Γ(X, (↑(X.affineBasicOpen f) : X.Opens)) : Type u) :=
  (CommRingCat.Hom.hom F).toAlgebra
this_2 : IsLocalization.Away f (↑Γ(X, X.basicOpen f) : Type u)
x : (↑Γ(X, X.basicOpen f) : Type u)
this : Topology.IsOpenEmbedding (X := ↥(Spec Γ(X, X.basicOpen f))) (Y := ↥(Spec Γ(X, (↑U : X.Opens)))) ⇑(Spec.map F)
Z' : Set ↥(Spec Γ(X, (↑U : X.Opens)))
I : Ideal (↑Γ(X, (↑U : X.Opens)) : Type u)
hx :
  Membership.mem (γ := Ideal (↑Γ(X, X.basicOpen f) : Type u))
    (PrimeSpectrum.vanishingIdeal
      (Set.preimage (β := ↥(Spec Γ(X, (↑U : X.Opens)))) (⇑(Spec.map F))
        (PrimeSpectrum.zeroLocus (↑I : Set (↑Γ(X, (↑U : X.Opens)) : Type u)))))
    x
hI : I.IsRadical
e : closure Z' = PrimeSpectrum.zeroLocus (↑I : Set (↑Γ(X, (↑U : X.Opens)) : Type u))
⊢ Membership.mem (γ := Submodule (↑Γ(X, X.basicOpen f) : Type u) (↑Γ(X, X.basicOpen f) : Type u))
    (Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) (PrimeSpectrum.vanishingIdeal Z')) x
have a : Membership.mem (γ := Submodule (↑Γ(X, X.basicOpen f) : Type u) (↑Γ(X, X.basicOpen f) : Type u))
  (Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE sorry).op))
    (PrimeSpectrum.vanishingIdeal (PrimeSpectrum.zeroLocus (↑I : Set (↑Γ(X, (↑U : X.Opens)) : Type u)))))
  x
Tactic: rw [← vanishingIdeal_closure, e]