awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
Goal:
X : Scheme
I : X.IdealSheafData
U V : (↑X.affineOpens : Type u)
x : ↥X
hxV : x ∈ (↑(↑V : X.Opens) : Set ↥X)
hxU : x ∈ (↑(↑U : X.Opens) : Set ↥X)
hx : ∀ f ∈ I.ideal U, x ∉ X.basicOpen f
s : (↑Γ(X, (↑V : X.Opens)) : Type u)
hfU : s ∈ I.ideal V
hxs : x ∈ X.basicOpen s
f : (↑Γ(X, (↑U : X.Opens)) : Type u)
g : (↑Γ(X, (↑V : X.Opens)) : Type u)
hfg : X.basicOpen f = X.basicOpen g
hxf : x ∈ X.basicOpen f
inst : IsLocalization.Away f (↑Γ(X, X.basicOpen f) : Type u)
this :
  Membership.mem (α := (↑Γ(X, (↑(X.affineBasicOpen f) : X.Opens)) : Type u)) (γ :=
    Submodule (↑Γ(X, (↑(X.affineBasicOpen f) : X.Opens)) : Type u) (↑Γ(X, (↑(X.affineBasicOpen f) : X.Opens)) : Type u))
    (Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) (I.ideal U))
    ((CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op) :
          (a : (↑Γ(X, (↑V : X.Opens)) : Type u)) → (↑Γ(X, (↑(X.affineBasicOpen f) : X.Opens)) : Type u))
        s :
      (↑Γ(X, (↑(X.affineBasicOpen f) : X.Opens)) : Type u))
⊢ False
have obtain : ∀ (s' : ↥(I.ideal U)) (n : ℕ)
  (hs' :
    HMul.hMul (α := (↑Γ(X, X.basicOpen f) : Type u)) (β := (↑Γ(X, X.basicOpen f) : Type u))
        ((CommRingCat.Hom.hom (X.presheaf.map (homOfLE sorry).op) :
              (a : (↑Γ(X, (↑V : X.Opens)) : Type u)) → (↑Γ(X, (↑(X.affineBasicOpen f) : X.Opens)) : Type u))
            s :
          (↑Γ(X, (↑(X.affineBasicOpen f) : X.Opens)) : Type u))
        ((algebraMap (↑Γ(X, (↑U : X.Opens)) : Type u) (↑Γ(X, X.basicOpen f) : Type u) :
              (a : (↑Γ(X, (↑U : X.Opens)) : Type u)) → (↑Γ(X, X.basicOpen f) : Type u))
            (↑(s',
                    Subtype.mk (p := fun (x : (↑Γ(X, (↑U : X.Opens)) : Type u)) ↦
                      Membership.mem (γ := Submonoid (↑Γ(X, (↑U : X.Opens)) : Type u)) (Submonoid.powers f) x)
                      ((fun (x : ℕ) ↦ f ^ x) n) sorry).2 :
              (↑Γ(X, (↑U : X.Opens)) : Type u)) :
          (↑Γ(X, X.basicOpen f) : Type u)) =
      (algebraMap (↑Γ(X, (↑U : X.Opens)) : Type u) (↑Γ(X, X.basicOpen f) : Type u) :
          (a : (↑Γ(X, (↑U : X.Opens)) : Type u)) → (↑Γ(X, X.basicOpen f) : Type u))
        (↑(s',
                Subtype.mk (p := fun (x : (↑Γ(X, (↑U : X.Opens)) : Type u)) ↦
                  Membership.mem (γ := Submonoid (↑Γ(X, (↑U : X.Opens)) : Type u)) (Submonoid.powers f) x)
                  ((fun (x : ℕ) ↦ f ^ x) n) sorry).1 :
          (↑Γ(X, (↑U : X.Opens)) : Type u))),
  False
Tactic: obtain ⟨⟨s', ⟨_, n, rfl⟩⟩, hs'⟩ :=
    (IsLocalization.mem_map_algebraMap_iff (.powers f) Γ(X, X.basicOpen f)).mp this
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
Goal:
X : Scheme
I : X.IdealSheafData
U V : (↑X.affineOpens : Type u)
x : ↥X
hxV : x ∈ (↑(↑V : X.Opens) : Set ↥X)
hxU : x ∈ (↑(↑U : X.Opens) : Set ↥X)
hx : ∀ f ∈ I.ideal U, x ∉ X.basicOpen f
s : (↑Γ(X, (↑V : X.Opens)) : Type u)
hfU : s ∈ I.ideal V
hxs : x ∈ X.basicOpen s
f : (↑Γ(X, (↑U : X.Opens)) : Type u)
g : (↑Γ(X, (↑V : X.Opens)) : Type u)
hfg : X.basicOpen f = X.basicOpen g
hxf : x ∈ X.basicOpen f
inst : IsLocalization.Away f (↑Γ(X, X.basicOpen f) : Type u)
this :
  Membership.mem (α := (↑Γ(X, (↑(X.affineBasicOpen f) : X.Opens)) : Type u)) (γ :=
    Submodule (↑Γ(X, (↑(X.affineBasicOpen f) : X.Opens)) : Type u) (↑Γ(X, (↑(X.affineBasicOpen f) : X.Opens)) : Type u))
    (Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) (I.ideal U))
    ((CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op) :
          (a : (↑Γ(X, (↑V : X.Opens)) : Type u)) → (↑Γ(X, (↑(X.affineBasicOpen f) : X.Opens)) : Type u))
        s :
      (↑Γ(X, (↑(X.affineBasicOpen f) : X.Opens)) : Type u))
s' : ↥(I.ideal U)
n : ℕ
hs' :
  (x ∈
      X.basicOpen
        (HMul.hMul (α := (↑Γ(X, X.basicOpen f) : Type u)) (β := (↑Γ(X, X.basicOpen f) : Type u))
          ((CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op) :
                (a : (↑Γ(X, (↑V : X.Opens)) : Type u)) → (↑Γ(X, (↑(X.affineBasicOpen f) : X.Opens)) : Type u))
              s :
            (↑Γ(X, (↑(X.affineBasicOpen f) : X.Opens)) : Type u))
          ((algebraMap (↑Γ(X, (↑U : X.Opens)) : Type u) (↑Γ(X, X.basicOpen f) : Type u) :
                (a : (↑Γ(X, (↑U : X.Opens)) : Type u)) → (↑Γ(X, X.basicOpen f) : Type u))
              (↑(s',
                      Subtype.mk (p := fun (x : (↑Γ(X, (↑U : X.Opens)) : Type u)) ↦
                        Membership.mem (γ := Submonoid (↑Γ(X, (↑U : X.Opens)) : Type u)) (Submonoid.powers f) x)
                        ((fun (x : ℕ) ↦ f ^ x) n) ⋯).2 :
                (↑Γ(X, (↑U : X.Opens)) : Type u)) :
            (↑Γ(X, X.basicOpen f) : Type u)))) =
    (x ∈
      X.basicOpen (U := X.basicOpen f)
        ((algebraMap (↑Γ(X, (↑U : X.Opens)) : Type u) (↑Γ(X, X.basicOpen f) : Type u) :
            (a : (↑Γ(X, (↑U : X.Opens)) : Type u)) → (↑Γ(X, X.basicOpen f) : Type u))
          (↑(s',
                  Subtype.mk (p := fun (x : (↑Γ(X, (↑U : X.Opens)) : Type u)) ↦
                    Membership.mem (γ := Submonoid (↑Γ(X, (↑U : X.Opens)) : Type u)) (Submonoid.powers f) x)
                    ((fun (x : ℕ) ↦ f ^ x) n) ⋯).1 :
            (↑Γ(X, (↑U : X.Opens)) : Type u))))
⊢ False
have refine : x ∈ X.basicOpen (↑s' : (↑Γ(X, (↑U : X.Opens)) : Type u))
Tactic: refine hx s' s'.2 ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
Goal:
X : Scheme
I : X.IdealSheafData
U : (↑X.affineOpens : Type u)
⊢ I.supportSet ∩ (↑(↑U : X.Opens) : Set ↥X) =
    X.zeroLocus (↑(I.ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u)) ∩ (↑(↑U : X.Opens) : Set ↥X)
have h : ∀ (x : ↥X),
  x ∈ I.supportSet ∩ (↑(↑U : X.Opens) : Set ↥X) ↔
    x ∈ X.zeroLocus (↑(I.ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u)) ∩ (↑(↑U : X.Opens) : Set ↥X)
Tactic: ext x
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
Goal:
X : Scheme
I : X.IdealSheafData
U : (↑X.affineOpens : Type u)
x : ↥X
⊢ x ∈ I.supportSet ∩ (↑(↑U : X.Opens) : Set ↥X) ↔
    x ∈ X.zeroLocus (↑(I.ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u)) ∩ (↑(↑U : X.Opens) : Set ↥X)
have pos : ∀ (hxU : x ∈ (↑U : X.Opens)),
  x ∈ I.supportSet ∩ (↑(↑U : X.Opens) : Set ↥X) ↔
    x ∈ X.zeroLocus (↑(I.ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u)) ∩ (↑(↑U : X.Opens) : Set ↥X)
Tactic: by_cases hxU : x ∈ U.1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
Goal:
X : Scheme
I : X.IdealSheafData
U : (↑X.affineOpens : Type u)
x : ↥X
pos :
  ∀ (hxU : x ∈ (↑U : X.Opens)),
    x ∈ I.supportSet ∩ (↑(↑U : X.Opens) : Set ↥X) ↔
      x ∈ X.zeroLocus (↑(I.ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u)) ∩ (↑(↑U : X.Opens) : Set ↥X)
⊢ x ∈ I.supportSet ∩ (↑(↑U : X.Opens) : Set ↥X) ↔
    x ∈ X.zeroLocus (↑(I.ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u)) ∩ (↑(↑U : X.Opens) : Set ↥X)
have neg : ∀ (hxU : x ∉ (↑U : X.Opens)),
  x ∈ I.supportSet ∩ (↑(↑U : X.Opens) : Set ↥X) ↔
    x ∈ X.zeroLocus (↑(I.ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u)) ∩ (↑(↑U : X.Opens) : Set ↥X)
Tactic: by_cases hxU : x ∈ U.1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
Goal:
X : Scheme
I : X.IdealSheafData
⊢ IsClosed I.supportSet
have rw : ∀ (i : (↑X.affineOpens : Type u)),
  IsClosed (X := ↥(↑i : X.Opens)) (Subtype.val (p := fun (x : ↥X) ↦ x ∈ (↑i : X.Opens)) ⁻¹' I.supportSet)
Tactic: rw [TopologicalSpace.IsOpenCover.isClosed_iff_coe_preimage (iSup_affineOpens_eq_top X)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
Goal:
X : Scheme
I : X.IdealSheafData
U : (↑X.affineOpens : Type u)
⊢ IsClosed (X := ↥(↑U : X.Opens)) (Subtype.val (p := fun (x : ↥X) ↦ x ∈ (↑U : X.Opens)) ⁻¹' I.supportSet)
have refine : Eq (α := Set ↥(↑U : X.Opens))
  (Subtype.val (p := fun (x : ↥X) ↦ x ∈ (↑U : X.Opens)) ⁻¹'
    (X.zeroLocus (↑(I.ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u)))ᶜ)
  (Subtype.val (p := fun (x : ↥X) ↦ x ∈ (↑U : X.Opens)) ⁻¹' I.supportSet)ᶜ
Tactic: refine ⟨(X.zeroLocus (U := U.1) (I.ideal U))ᶜ, (X.zeroLocus_isClosed _).isOpen_compl, ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
Goal:
X : Scheme
I : X.IdealSheafData
U : (↑X.affineOpens : Type u)
⊢ Eq (α := Set ↥(↑U : X.Opens))
    (Subtype.val (p := fun (x : ↥X) ↦ x ∈ (↑U : X.Opens)) ⁻¹'
      (X.zeroLocus (↑(I.ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u)))ᶜ)
    (Subtype.val (p := fun (x : ↥X) ↦ x ∈ (↑U : X.Opens)) ⁻¹' I.supportSet)ᶜ
have simp : Eq (α := Set ↥(↑U : X.Opens))
  (Subtype.val (p := fun (x : ↥X) ↦ x ∈ (↑U : X.Opens)) ⁻¹'
    X.zeroLocus (↑(I.ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u)))
  (Subtype.val (p := fun (x : ↥X) ↦ x ∈ (↑U : X.Opens)) ⁻¹' I.supportSet)
Tactic: simp only [Set.preimage_compl, compl_inj_iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
Goal:
X : Scheme
I : X.IdealSheafData
U : (↑X.affineOpens : Type u)
⊢ Eq (α := Set ↥(↑U : X.Opens))
    (Subtype.val (p := fun (x : ↥X) ↦ x ∈ (↑U : X.Opens)) ⁻¹'
      X.zeroLocus (↑(I.ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u)))
    (Subtype.val (p := fun (x : ↥X) ↦ x ∈ (↑U : X.Opens)) ⁻¹' I.supportSet)
have a : Set.image (α := ↥(↑U : X.Opens)) (Subtype.val (p := fun (x : ↥X) ↦ x ∈ (↑U : X.Opens)))
    (Subtype.val (p := fun (x : ↥X) ↦ x ∈ (↑U : X.Opens)) ⁻¹'
      X.zeroLocus (↑(I.ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u))) =
  Set.image (α := ↥(↑U : X.Opens)) (Subtype.val (p := fun (x : ↥X) ↦ x ∈ (↑U : X.Opens)))
    (Subtype.val (p := fun (x : ↥X) ↦ x ∈ (↑U : X.Opens)) ⁻¹' I.supportSet)
Tactic: apply Subtype.val_injective.image_injective
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
Goal:
X : Scheme
I : X.IdealSheafData
ideal : (U : (↑X.affineOpens : Type u)) → Ideal (↑Γ(X, (↑U : X.Opens)) : Type u)
map_ideal_basicOpen :
  ∀ (U : (↑X.affineOpens : Type u)) (f : (↑Γ(X, (↑U : X.Opens)) : Type u)),
    Eq (α := Ideal (↑Γ(X, X.basicOpen f) : Type u))
      (Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) (ideal U) :
        Ideal (↑Γ(X, X.basicOpen f) : Type u))
      (ideal (X.affineBasicOpen f) : Ideal (↑Γ(X, (↑(X.affineBasicOpen f) : X.Opens)) : Type u))
supportSet : Set ↥X
supportSet_inter :
  ∀ (U : (↑X.affineOpens : Type u)),
    ∀ x ∈ (↑U : X.Opens), x ∈ supportSet ↔ x ∈ X.zeroLocus (↑(ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u))
I' : X.IdealSheafData :=
  { ideal := ideal, map_ideal_basicOpen := map_ideal_basicOpen, supportSet_eq_iInter_zeroLocus := ⋯ }
⊢ supportSet = ⋂ (U : (↑X.affineOpens : Type u)), X.zeroLocus (↑(ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u))
have change : supportSet = I'.supportSet
Tactic: change supportSet = I'.supportSet
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
Goal:
X : Scheme
I : X.IdealSheafData
ideal : (U : (↑X.affineOpens : Type u)) → Ideal (↑Γ(X, (↑U : X.Opens)) : Type u)
map_ideal_basicOpen :
  ∀ (U : (↑X.affineOpens : Type u)) (f : (↑Γ(X, (↑U : X.Opens)) : Type u)),
    Eq (α := Ideal (↑Γ(X, X.basicOpen f) : Type u))
      (Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) (ideal U) :
        Ideal (↑Γ(X, X.basicOpen f) : Type u))
      (ideal (X.affineBasicOpen f) : Ideal (↑Γ(X, (↑(X.affineBasicOpen f) : X.Opens)) : Type u))
supportSet : Set ↥X
supportSet_inter :
  ∀ (U : (↑X.affineOpens : Type u)),
    ∀ x ∈ (↑U : X.Opens), x ∈ supportSet ↔ x ∈ X.zeroLocus (↑(ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u))
I' : X.IdealSheafData :=
  { ideal := ideal, map_ideal_basicOpen := map_ideal_basicOpen, supportSet_eq_iInter_zeroLocus := ⋯ }
⊢ supportSet = I'.supportSet
have h : ∀ (x : ↥X), x ∈ supportSet ↔ x ∈ I'.supportSet
Tactic: ext x
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
Goal:
X : Scheme
I : X.IdealSheafData
ideal : (U : (↑X.affineOpens : Type u)) → Ideal (↑Γ(X, (↑U : X.Opens)) : Type u)
map_ideal_basicOpen :
  ∀ (U : (↑X.affineOpens : Type u)) (f : (↑Γ(X, (↑U : X.Opens)) : Type u)),
    Eq (α := Ideal (↑Γ(X, X.basicOpen f) : Type u))
      (Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) (ideal U) :
        Ideal (↑Γ(X, X.basicOpen f) : Type u))
      (ideal (X.affineBasicOpen f) : Ideal (↑Γ(X, (↑(X.affineBasicOpen f) : X.Opens)) : Type u))
supportSet : Set ↥X
supportSet_inter :
  ∀ (U : (↑X.affineOpens : Type u)),
    ∀ x ∈ (↑U : X.Opens), x ∈ supportSet ↔ x ∈ X.zeroLocus (↑(ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u))
I' : X.IdealSheafData :=
  { ideal := ideal, map_ideal_basicOpen := map_ideal_basicOpen, supportSet_eq_iInter_zeroLocus := ⋯ }
x : ↥X
⊢ x ∈ supportSet ↔ x ∈ I'.supportSet
have h : ∀ (U : TopologicalSpace.Opens ↥X) (hU : U ∈ X.affineOpens) (hxU : x ∈ (↑U : Set ↥X)), x ∈ supportSet ↔ x ∈ I'.supportSet
Tactic: obtain ⟨_, ⟨U, hU, rfl⟩, hxU, -⟩ :=
      X.isBasis_affineOpens.exists_subset_of_mem_open (Set.mem_univ x) isOpen_univ
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
Goal:
X : Scheme
I J : X.IdealSheafData
h : I ≤ J
⊢ J.support ≤ I.support
have rw : Subset.{u} (α := Set ↥X)
  (⋂ (U : (↑X.affineOpens : Type u)), X.zeroLocus (↑(J.ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u)))
  (⋂ (U : (↑X.affineOpens : Type u)), X.zeroLocus (↑(I.ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u)))
Tactic: rw [← SetLike.coe_subset_coe, I.coe_support_eq_eq_iInter_zeroLocus,
    J.coe_support_eq_eq_iInter_zeroLocus]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
Goal:
X : Scheme
I : X.IdealSheafData
⊢ I.support = ⊥ ↔ I = ⊤
have refine : ∀ (H : I.support = ⊥) (U : (↑X.affineOpens : Type u)), ideal ⊤ U ≤ I.ideal U
Tactic: refine ⟨fun H ↦ top_le_iff.mp fun U ↦ ?_, by simp +contextual⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (hypothesis)
Goal:
X : Scheme
I : X.IdealSheafData
H : I.support = ⊥
U : (↑X.affineOpens : Type u)
⊢ ideal ⊤ U ≤ I.ideal U
have this : Set.image (α := ↥(Spec Γ(X, (↑U : X.Opens)))) (⇑(IsAffineOpen.fromSpec sorry))
    (PrimeSpectrum.zeroLocus (↑(I.ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u))) ⊆
  (↑⊥ : Set ↥X)
Tactic: have := (U.2.fromSpec_image_zeroLocus _).trans_subset
    ((zeroLocus_inter_subset_supportSet I U).trans H.le)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (hypothesis)
Goal:
X : Scheme
I : X.IdealSheafData
H : I.support = ⊥
U : (↑X.affineOpens : Type u)
this :
  Set.image (α := ↥(Spec Γ(X, (↑U : X.Opens)))) (⇑(IsAffineOpen.fromSpec ⋯))
      (PrimeSpectrum.zeroLocus (↑(I.ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u))) ⊆
    (↑⊥ : Set ↥X)
⊢ ideal ⊤ U ≤ I.ideal U
have this₁ : Eq (α := Set ↥(Spec Γ(X, (↑U : X.Opens))))
  (PrimeSpectrum.zeroLocus (↑(I.ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u))) ∅
Tactic: simp only [Set.subset_empty_iff, Set.image_eq_empty, Closeds.coe_bot] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
Goal:
X : Scheme
I_1 I_2 J K I : X.IdealSheafData
n : ℕ
U : (↑X.affineOpens : Type u)
x : ↥X
hxU : x ∈ (↑U : X.Opens)
⊢ x ∈ X.zeroLocus (↑((I.ideal ^ n) U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u)) ↔ x ∈ if n = 0 then ∅ else I.supportSet
have zero : x ∈ X.zeroLocus (↑(HPow.hPow (β := ℕ) I.ideal 0 U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u)) ↔
  x ∈ if Eq (α := ℕ) 0 0 then ∅ else I.supportSet
Tactic: induction n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
Goal:
X : Scheme
I_1 I_2 J K I : X.IdealSheafData
n : ℕ
U : (↑X.affineOpens : Type u)
x : ↥X
hxU : x ∈ (↑U : X.Opens)
zero :
  x ∈ X.zeroLocus (↑(HPow.hPow (β := ℕ) I.ideal 0 U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u)) ↔
    x ∈ if Eq (α := ℕ) 0 0 then ∅ else I.supportSet
⊢ x ∈ X.zeroLocus (↑((I.ideal ^ n) U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u)) ↔ x ∈ if n = 0 then ∅ else I.supportSet
have succ : ∀ (n : ℕ),
  (x ∈ X.zeroLocus (↑((I.ideal ^ n) U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u)) ↔
      x ∈ if n = 0 then ∅ else I.supportSet) →
    (x ∈ X.zeroLocus (↑((I.ideal ^ (n + 1)) U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u)) ↔
      x ∈ if n + 1 = 0 then ∅ else I.supportSet)
Tactic: induction n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
Goal:
X : Scheme
I : X.IdealSheafData
n : ℕ
hn : n ≠ 0
⊢ (I ^ n).support = I.support
have zero : ∀ (hn : Ne (α := ℕ) 0 0), (HPow.hPow (β := ℕ) I 0).support = I.support
Tactic: cases n
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
Goal:
X : Scheme
I : X.IdealSheafData
n : ℕ
hn : n ≠ 0
zero : ∀ (hn : Ne (α := ℕ) 0 0), (HPow.hPow (β := ℕ) I 0).support = I.support
⊢ (I ^ n).support = I.support
have succ : ∀ (n : ℕ) (hn : n + 1 ≠ 0), (I ^ (n + 1)).support = I.support
Tactic: cases n
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
Goal:
X : Scheme
I : X.IdealSheafData
⊢ ⊤ * I = I
have h : ∀ (x : (↑X.affineOpens : Type u)) (x_1 : (↑Γ(X, (↑x : X.Opens)) : Type u)), x_1 ∈ (⊤ * I).ideal x ↔ x_1 ∈ I.ideal x
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
Goal:
X : Scheme
I : X.IdealSheafData
⊢ I * ⊤ = I
have h : ∀ (x : (↑X.affineOpens : Type u)) (x_1 : (↑Γ(X, (↑x : X.Opens)) : Type u)), x_1 ∈ (I * ⊤).ideal x ↔ x_1 ∈ I.ideal x
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
Goal:
X : Scheme
I : X.IdealSheafData
⊢ ⊥ * I = ⊥
have h : ∀ (x : (↑X.affineOpens : Type u)) (x_1 : (↑Γ(X, (↑x : X.Opens)) : Type u)), x_1 ∈ (⊥ * I).ideal x ↔ x_1 ∈ ideal ⊥ x
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
Goal:
X : Scheme
I : X.IdealSheafData
⊢ I * ⊥ = ⊥
have h : ∀ (x : (↑X.affineOpens : Type u)) (x_1 : (↑Γ(X, (↑x : X.Opens)) : Type u)), x_1 ∈ (I * ⊥).ideal x ↔ x_1 ∈ ideal ⊥ x
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
Goal:
X : Scheme
I J K : X.IdealSheafData
⊢ I * (J ⊔ K) = I * J ⊔ I * K
have h : ∀ (U : (↑X.affineOpens : Type u)), (I * (J ⊔ K)).ideal U = (I * J ⊔ I * K).ideal U
Tactic: ext U : 2
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
Goal:
X : Scheme
I J K : X.IdealSheafData
⊢ (I ⊔ J) * K = I * K ⊔ J * K
have h : ∀ (U : (↑X.affineOpens : Type u)), ((I ⊔ J) * K).ideal U = (I * K ⊔ J * K).ideal U
Tactic: ext U : 2
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
Goal:
X : Scheme
I_1 I J K x : X.IdealSheafData
⊢ HPow.hPow (β := ℕ) x 0 = 1
have h : ∀ (x_1 : (↑X.affineOpens : Type u)) (x_2 : (↑Γ(X, (↑x_1 : X.Opens)) : Type u)),
  x_2 ∈ (HPow.hPow (β := ℕ) x 0).ideal x_1 ↔ x_2 ∈ ideal 1 x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
Goal:
X : Scheme
I_1 I J K : X.IdealSheafData
x : ℕ
x_1 : X.IdealSheafData
⊢ x_1 ^ (x + 1) = x_1 ^ x * x_1
have h : ∀ (x_2 : (↑X.affineOpens : Type u)) (x_3 : (↑Γ(X, (↑x_2 : X.Opens)) : Type u)),
  x_3 ∈ (x_1 ^ (x + 1)).ideal x_2 ↔ x_3 ∈ (x_1 ^ x * x_1).ideal x_2
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
Goal:
X : Scheme
I_1 : X.IdealSheafData
I : Ideal (↑Γ(X, ⊤) : Type u)
U : (↑X.affineOpens : Type u)
f : (↑Γ(X, (↑U : X.Opens)) : Type u)
⊢ 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)) ↦
          (Ideal.map (F :=
              (↑(X.presheaf.obj (Opposite.op ⊤)) : Type u) →+*
                (↑(X.presheaf.obj (Opposite.op (↑U : X.Opens))) : Type u))
              (CommRingCat.Hom.hom (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯)))) I :
            Ideal (↑Γ(X, (↑U : X.Opens)) : Type u)))
        U))
    ((fun (U : (↑X.affineOpens : Type u)) ↦
        (Ideal.map (F :=
            (↑(X.presheaf.obj (Opposite.op ⊤)) : Type u) →+* (↑(X.presheaf.obj (Opposite.op (↑U : X.Opens))) : Type u))
            (CommRingCat.Hom.hom (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯)))) I :
          Ideal (↑Γ(X, (↑U : X.Opens)) : Type u)))
      (X.affineBasicOpen f))
have rw : Eq (α := Ideal (↑Γ(X, X.basicOpen f) : Type u))
  (Ideal.map (F := (↑Γ(X, ⊤) : Type u) →+* (↑Γ(X, X.basicOpen f) : Type u))
    (CommRingCat.Hom.hom (X.presheaf.map (Quiver.Hom.op (homOfLE sorry) ≫ (homOfLE sorry).op))) I)
  ((fun (U : (↑X.affineOpens : Type u)) ↦
      (Ideal.map (F :=
          (↑(X.presheaf.obj (Opposite.op ⊤)) : Type u) →+* (↑(X.presheaf.obj (Opposite.op (↑U : X.Opens))) : Type u))
          (CommRingCat.Hom.hom (X.presheaf.map (Quiver.Hom.op (homOfLE sorry)))) I :
        Ideal (↑Γ(X, (↑U : X.Opens)) : Type u)))
    (X.affineBasicOpen f))
Tactic: rw [Ideal.map_map, ← CommRingCat.hom_comp, ← Functor.map_comp]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
Goal:
X : Scheme
inst : IsAffine X
I J : X.IdealSheafData
H :
  LE.le (α := Ideal (↑Γ(X, (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) ⊤ ⋯) : X.Opens)) : Type u))
    (I.ideal (Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) ⊤ ⋯))
    (J.ideal (Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) ⊤ ⋯))
U : (↑X.affineOpens : Type u)
⊢ I.ideal U ≤ J.ideal U
have rw : LE.le (α := (fun (U : (↑X.affineOpens : Type u)) ↦ Ideal.{u} (↑Γ(X, (↑U : X.Opens)) : Type u)) U)
  (Ideal.map (R := (↑Γ(X, (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) ⊤ sorry) : X.Opens)) : Type u)) (F :=
    (↑Γ(X, (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) ⊤ sorry) : X.Opens)) : Type u) →+*
      (↑Γ(X, (↑U : X.Opens)) : Type u))
    (CommRingCat.Hom.hom (X.presheaf.map (Quiver.Hom.op (homOfLE sorry))))
    (I.ideal (Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) ⊤ sorry)))
  (Ideal.map (R := (↑Γ(X, (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) ⊤ sorry) : X.Opens)) : Type u)) (F :=
    (↑Γ(X, (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) ⊤ sorry) : X.Opens)) : Type u) →+*
      (↑Γ(X, (↑U : X.Opens)) : Type u))
    (CommRingCat.Hom.hom (X.presheaf.map (Quiver.Hom.op (homOfLE sorry))))
    (J.ideal (Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) ⊤ sorry)))
Tactic: rw [← map_ideal (U := U) (V := ⟨⊤, isAffineOpen_top X⟩) I (le_top (a := U.1)),
    ← map_ideal (U := U) (V := ⟨⊤, isAffineOpen_top X⟩) J (le_top (a := U.1))]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
Goal:
X : Scheme
I J : X.IdealSheafData
⊢ (I ⊔ J).radical = (I.radical ⊔ J.radical).radical
have h : ∀ (U : (↑X.affineOpens : Type u)), (I ⊔ J).radical.ideal U = (I.radical ⊔ J.radical).radical.ideal U
Tactic: ext U : 2
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
Goal:
X : Scheme
I J : X.IdealSheafData
⊢ (I ⊓ J).radical = I.radical ⊓ J.radical
have h : ∀ (U : (↑X.affineOpens : Type u)), (I ⊓ J).radical.ideal U = (I.radical ⊓ J.radical).ideal U
Tactic: ext U : 2
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
Goal:
X : Scheme
I J : X.IdealSheafData
⊢ (I * J).radical = I.radical ⊓ J.radical
have h : ∀ (U : (↑X.affineOpens : Type u)), (I * J).radical.ideal U = (I.radical ⊓ J.radical).ideal U
Tactic: ext U : 2