awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
Goal:
X : Scheme
I J : X.IdealSheafData
ι : Type u_1
U : ι → (↑X.affineOpens : Type u)
hU : Eq.{u + 1} (α := X.Opens) (⨆ (i : ι), (↑(U i) : X.Opens)) ⊤
H : ∀ (i : ι), LE.le (α := Ideal (↑Γ(X, (↑(U i) : X.Opens)) : Type u)) (I.ideal (U i)) (J.ideal (U i))
V : (↑X.affineOpens : Type u)
i : (x : ↥(↑V : X.Opens)) → ι
r : (x : ↥(↑V : X.Opens)) → (↑Γ(X, (↑V : X.Opens)) : Type u)
rU : (x : ↥(↑V : X.Opens)) → (↑Γ(X, (↑(U (i x)) : X.Opens)) : Type u)
e : ∀ (x : ↥(↑V : X.Opens)), X.basicOpen (r x) = X.basicOpen (rU x)
hxr : ∀ (x : ↥(↑V : X.Opens)), (↑x : ↥X) ∈ X.basicOpen (r x)
⊢ Eq (α := Ideal (↑Γ(X, (↑V : X.Opens)) : Type u)) (Ideal.span (Set.range r)) ⊤
have rw : (↑V : X.Opens) ≤ ⨆ (f : (↑(Set.range r) : Type u)), X.basicOpen (↑f : (↑Γ(X, (↑V : X.Opens)) : Type u))
Tactic: rw [← V.2.self_le_iSup_basicOpen_iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (hypothesis)
Goal:
X : Scheme
I J : X.IdealSheafData
ι : Type u_1
U : ι → (↑X.affineOpens : Type u)
hU : Eq.{u + 1} (α := X.Opens) (⨆ (i : ι), (↑(U i) : X.Opens)) ⊤
H : ∀ (i : ι), LE.le (α := Ideal (↑Γ(X, (↑(U i) : X.Opens)) : Type u)) (I.ideal (U i)) (J.ideal (U i))
V : (↑X.affineOpens : Type u)
i : (x : ↥(↑V : X.Opens)) → ι
r : (x : ↥(↑V : X.Opens)) → (↑Γ(X, (↑V : X.Opens)) : Type u)
rU : (x : ↥(↑V : X.Opens)) → (↑Γ(X, (↑(U (i x)) : X.Opens)) : Type u)
e : ∀ (x : ↥(↑V : X.Opens)), X.basicOpen (r x) = X.basicOpen (rU x)
hxr : ∀ (x : ↥(↑V : X.Opens)), (↑x : ↥X) ∈ X.basicOpen (r x)
⊢ I.ideal V ≤ J.ideal V
have this : Eq (α := Ideal (↑Γ(X, (↑V : X.Opens)) : Type u)) (Ideal.span (Set.range r)) ⊤
Tactic: have : Ideal.span (Set.range r) = ⊤ := by
    rw [← V.2.self_le_iSup_basicOpen_iff]
    exact fun x hxV ↦ TopologicalSpace.Opens.mem_iSup.mpr ⟨⟨_, _, rfl⟩, hxr ⟨x, hxV⟩⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (hypothesis)
Goal:
X : Scheme
I J : X.IdealSheafData
ι : Type u_1
U : ι → (↑X.affineOpens : Type u)
hU : Eq.{u + 1} (α := X.Opens) (⨆ (i : ι), (↑(U i) : X.Opens)) ⊤
H : ∀ (i : ι), LE.le (α := Ideal (↑Γ(X, (↑(U i) : X.Opens)) : Type u)) (I.ideal (U i)) (J.ideal (U i))
V : (↑X.affineOpens : Type u)
i : (x : ↥(↑V : X.Opens)) → ι
r : (x : ↥(↑V : X.Opens)) → (↑Γ(X, (↑V : X.Opens)) : Type u)
rU : (x : ↥(↑V : X.Opens)) → (↑Γ(X, (↑(U (i x)) : X.Opens)) : Type u)
e : ∀ (x : ↥(↑V : X.Opens)), X.basicOpen (r x) = X.basicOpen (rU x)
hxr : ∀ (x : ↥(↑V : X.Opens)), (↑x : ↥X) ∈ X.basicOpen (r x)
this : Eq (α := Ideal (↑Γ(X, (↑V : X.Opens)) : Type u)) (Ideal.span (Set.range r)) ⊤
⊢ I.ideal V ≤ J.ideal V
have inst : ∀ (f : (↑Γ(X, (↑V : X.Opens)) : Type u)), IsLocalization.Away f (↑Γ(X, X.basicOpen f) : Type u)
Tactic: have inst := V.2.isLocalization_basicOpen
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
Goal:
X : Scheme
I J : X.IdealSheafData
ι : Type u_1
U : ι → (↑X.affineOpens : Type u)
hU : Eq.{u + 1} (α := X.Opens) (⨆ (i : ι), (↑(U i) : X.Opens)) ⊤
H : ∀ (i : ι), LE.le (α := Ideal (↑Γ(X, (↑(U i) : X.Opens)) : Type u)) (I.ideal (U i)) (J.ideal (U i))
V : (↑X.affineOpens : Type u)
i : (x : ↥(↑V : X.Opens)) → ι
r : (x : ↥(↑V : X.Opens)) → (↑Γ(X, (↑V : X.Opens)) : Type u)
rU : (x : ↥(↑V : X.Opens)) → (↑Γ(X, (↑(U (i x)) : X.Opens)) : Type u)
e : ∀ (x : ↥(↑V : X.Opens)), X.basicOpen (r x) = X.basicOpen (rU x)
hxr : ∀ (x : ↥(↑V : X.Opens)), (↑x : ↥X) ∈ X.basicOpen (r x)
this : Eq (α := Ideal (↑Γ(X, (↑V : X.Opens)) : Type u)) (Ideal.span (Set.range r)) ⊤
inst : ∀ (f : (↑Γ(X, (↑V : X.Opens)) : Type u)), IsLocalization.Away f (↑Γ(X, X.basicOpen f) : Type u)
⊢ I.ideal V ≤ J.ideal V
have refine : ∀ (r_1 : (↑(Set.range r) : Type u)),
  LE.le (α :=
    Submodule (↑Γ(X, (↑V : X.Opens)) : Type u)
      ((fun (i : (↑(Set.range r) : Type u)) ↦ (↑Γ(X, X.basicOpen (↑i : (↑Γ(X, (↑V : X.Opens)) : Type u))) : Type u))
        r_1))
    (Submodule.localized₀ (Submonoid.powers (↑r_1 : (↑Γ(X, (↑V : X.Opens)) : Type u)))
      ((fun (i : (↑(Set.range r) : Type u)) ↦
          (Algebra.linearMap (↑Γ(X, (↑V : X.Opens)) : Type u)
              (↑Γ(X, X.basicOpen (↑i : (↑Γ(X, (↑V : X.Opens)) : Type u))) : Type u) :
            LinearMap (R := (↑Γ(X, (↑V : X.Opens)) : Type u)) (RingHom.id (↑Γ(X, (↑V : X.Opens)) : Type u))
              (↑Γ(X, (↑V : X.Opens)) : Type u) (↑Γ(X, X.basicOpen (↑i : (↑Γ(X, (↑V : X.Opens)) : Type u))) : Type u)))
        r_1)
      (I.ideal V))
    (Submodule.localized₀ (Submonoid.powers (↑r_1 : (↑Γ(X, (↑V : X.Opens)) : Type u)))
      ((fun (i : (↑(Set.range r) : Type u)) ↦
          (Algebra.linearMap (↑Γ(X, (↑V : X.Opens)) : Type u)
              (↑Γ(X, X.basicOpen (↑i : (↑Γ(X, (↑V : X.Opens)) : Type u))) : Type u) :
            LinearMap (R := (↑Γ(X, (↑V : X.Opens)) : Type u)) (RingHom.id (↑Γ(X, (↑V : X.Opens)) : Type u))
              (↑Γ(X, (↑V : X.Opens)) : Type u) (↑Γ(X, X.basicOpen (↑i : (↑Γ(X, (↑V : X.Opens)) : Type u))) : Type u)))
        r_1)
      (J.ideal V))
Tactic: refine Submodule.le_of_isLocalized_span _ this (fun i ↦ Γ(X, X.basicOpen i.1))
    (fun i ↦ Algebra.linearMap Γ(X, V.1) Γ(X, X.basicOpen i.1)) ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
Goal:
X : Scheme
I J : X.IdealSheafData
ι : Type u_1
U : ι → (↑X.affineOpens : Type u)
hU : Eq.{u + 1} (α := X.Opens) (⨆ (i : ι), (↑(U i) : X.Opens)) ⊤
H : ∀ (i : ι), LE.le (α := Ideal (↑Γ(X, (↑(U i) : X.Opens)) : Type u)) (I.ideal (U i)) (J.ideal (U i))
V : (↑X.affineOpens : Type u)
i : (x : ↥(↑V : X.Opens)) → ι
r : (x : ↥(↑V : X.Opens)) → (↑Γ(X, (↑V : X.Opens)) : Type u)
rU : (x : ↥(↑V : X.Opens)) → (↑Γ(X, (↑(U (i x)) : X.Opens)) : Type u)
e : ∀ (x : ↥(↑V : X.Opens)), X.basicOpen (r x) = X.basicOpen (rU x)
hxr : ∀ (x : ↥(↑V : X.Opens)), (↑x : ↥X) ∈ X.basicOpen (r x)
this : Eq (α := Ideal (↑Γ(X, (↑V : X.Opens)) : Type u)) (Ideal.span (Set.range r)) ⊤
inst : ∀ (f : (↑Γ(X, (↑V : X.Opens)) : Type u)), IsLocalization.Away f (↑Γ(X, X.basicOpen f) : Type u)
j : ↥(↑V : X.Opens)
⊢ LE.le (α :=
    Submodule (↑Γ(X, (↑V : X.Opens)) : Type u)
      ((fun (i : (↑(Set.range r) : Type u)) ↦ (↑Γ(X, X.basicOpen (↑i : (↑Γ(X, (↑V : X.Opens)) : Type u))) : Type u))
        (Subtype.mk (p := fun (x : (↑Γ(X, (↑V : X.Opens)) : Type u)) ↦ x ∈ Set.range r) (r j) ⋯)))
    (Submodule.localized₀
      (Submonoid.powers
        (↑(Subtype.mk (p := fun (x : (↑Γ(X, (↑V : X.Opens)) : Type u)) ↦ x ∈ Set.range r) (r j) ⋯) :
          (↑Γ(X, (↑V : X.Opens)) : Type u)))
      ((fun (i : (↑(Set.range r) : Type u)) ↦
          (Algebra.linearMap (↑Γ(X, (↑V : X.Opens)) : Type u)
              (↑Γ(X, X.basicOpen (↑i : (↑Γ(X, (↑V : X.Opens)) : Type u))) : Type u) :
            LinearMap (R := (↑Γ(X, (↑V : X.Opens)) : Type u)) (RingHom.id (↑Γ(X, (↑V : X.Opens)) : Type u))
              (↑Γ(X, (↑V : X.Opens)) : Type u) (↑Γ(X, X.basicOpen (↑i : (↑Γ(X, (↑V : X.Opens)) : Type u))) : Type u)))
        (Subtype.mk (p := fun (x : (↑Γ(X, (↑V : X.Opens)) : Type u)) ↦ x ∈ Set.range r) (r j) ⋯))
      (I.ideal V))
    (Submodule.localized₀
      (Submonoid.powers
        (↑(Subtype.mk (p := fun (x : (↑Γ(X, (↑V : X.Opens)) : Type u)) ↦ x ∈ Set.range r) (r j) ⋯) :
          (↑Γ(X, (↑V : X.Opens)) : Type u)))
      ((fun (i : (↑(Set.range r) : Type u)) ↦
          (Algebra.linearMap (↑Γ(X, (↑V : X.Opens)) : Type u)
              (↑Γ(X, X.basicOpen (↑i : (↑Γ(X, (↑V : X.Opens)) : Type u))) : Type u) :
            LinearMap (R := (↑Γ(X, (↑V : X.Opens)) : Type u)) (RingHom.id (↑Γ(X, (↑V : X.Opens)) : Type u))
              (↑Γ(X, (↑V : X.Opens)) : Type u) (↑Γ(X, X.basicOpen (↑i : (↑Γ(X, (↑V : X.Opens)) : Type u))) : Type u)))
        (Subtype.mk (p := fun (x : (↑Γ(X, (↑V : X.Opens)) : Type u)) ↦ x ∈ Set.range r) (r j) ⋯))
      (J.ideal V))
have dsimp : LE.le (α := Submodule (↑Γ(X, (↑V : X.Opens)) : Type u) (↑Γ(X, X.basicOpen (r j)) : Type u))
  (Submodule.localized₀ (Submonoid.powers (r j))
    (Algebra.linearMap (↑Γ(X, (↑V : X.Opens)) : Type u) (↑Γ(X, X.basicOpen (r j)) : Type u)) (I.ideal V))
  (Submodule.localized₀ (Submonoid.powers (r j))
    (Algebra.linearMap (↑Γ(X, (↑V : X.Opens)) : Type u) (↑Γ(X, X.basicOpen (r j)) : Type u)) (J.ideal V))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
Goal:
X : Scheme
I J : X.IdealSheafData
ι : Type u_1
U : ι → (↑X.affineOpens : Type u)
hU : Eq.{u + 1} (α := X.Opens) (⨆ (i : ι), (↑(U i) : X.Opens)) ⊤
H : ∀ (i : ι), LE.le (α := Ideal (↑Γ(X, (↑(U i) : X.Opens)) : Type u)) (I.ideal (U i)) (J.ideal (U i))
V : (↑X.affineOpens : Type u)
i : (x : ↥(↑V : X.Opens)) → ι
r : (x : ↥(↑V : X.Opens)) → (↑Γ(X, (↑V : X.Opens)) : Type u)
rU : (x : ↥(↑V : X.Opens)) → (↑Γ(X, (↑(U (i x)) : X.Opens)) : Type u)
e : ∀ (x : ↥(↑V : X.Opens)), X.basicOpen (r x) = X.basicOpen (rU x)
hxr : ∀ (x : ↥(↑V : X.Opens)), (↑x : ↥X) ∈ X.basicOpen (r x)
this : Eq (α := Ideal (↑Γ(X, (↑V : X.Opens)) : Type u)) (Ideal.span (Set.range r)) ⊤
inst : ∀ (f : (↑Γ(X, (↑V : X.Opens)) : Type u)), IsLocalization.Away f (↑Γ(X, X.basicOpen f) : Type u)
j : ↥(↑V : X.Opens)
⊢ LE.le (α := Submodule (↑Γ(X, (↑V : X.Opens)) : Type u) (↑Γ(X, X.basicOpen (r j)) : Type u))
    (Submodule.localized₀ (Submonoid.powers (r j))
      (Algebra.linearMap (↑Γ(X, (↑V : X.Opens)) : Type u) (↑Γ(X, X.basicOpen (r j)) : Type u)) (I.ideal V))
    (Submodule.localized₀ (Submonoid.powers (r j))
      (Algebra.linearMap (↑Γ(X, (↑V : X.Opens)) : Type u) (↑Γ(X, X.basicOpen (r j)) : Type u)) (J.ideal V))
have simp : LE.le (α := Submodule (↑Γ(X, (↑V : X.Opens)) : Type u) (↑Γ(X, X.basicOpen (r j)) : Type u))
  (Submodule.restrictScalars (↑Γ(X, (↑V : X.Opens)) : Type u)
    (Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE sorry).op)) (I.ideal V)))
  (Submodule.restrictScalars (↑Γ(X, (↑V : X.Opens)) : Type u)
    (Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE sorry).op)) (J.ideal V)))
Tactic: simp +instances only [← Submodule.restrictScalars_localized' Γ(X, X.basicOpen (r j)),
    Ideal.localized'_eq_map, RingHom.algebraMap_toAlgebra]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
Goal:
X : Scheme
I J : X.IdealSheafData
ι : Type u_1
U : ι → (↑X.affineOpens : Type u)
hU : Eq.{u + 1} (α := X.Opens) (⨆ (i : ι), (↑(U i) : X.Opens)) ⊤
H : ∀ (i : ι), LE.le (α := Ideal (↑Γ(X, (↑(U i) : X.Opens)) : Type u)) (I.ideal (U i)) (J.ideal (U i))
V : (↑X.affineOpens : Type u)
i : (x : ↥(↑V : X.Opens)) → ι
r : (x : ↥(↑V : X.Opens)) → (↑Γ(X, (↑V : X.Opens)) : Type u)
rU : (x : ↥(↑V : X.Opens)) → (↑Γ(X, (↑(U (i x)) : X.Opens)) : Type u)
e : ∀ (x : ↥(↑V : X.Opens)), X.basicOpen (r x) = X.basicOpen (rU x)
hxr : ∀ (x : ↥(↑V : X.Opens)), (↑x : ↥X) ∈ X.basicOpen (r x)
this : Eq (α := Ideal (↑Γ(X, (↑V : X.Opens)) : Type u)) (Ideal.span (Set.range r)) ⊤
inst : ∀ (f : (↑Γ(X, (↑V : X.Opens)) : Type u)), IsLocalization.Away f (↑Γ(X, X.basicOpen f) : Type u)
j : ↥(↑V : X.Opens)
⊢ LE.le (α := Submodule (↑Γ(X, (↑V : X.Opens)) : Type u) (↑Γ(X, X.basicOpen (r j)) : Type u))
    (Submodule.restrictScalars (↑Γ(X, (↑V : X.Opens)) : Type u)
      (Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) (I.ideal V)))
    (Submodule.restrictScalars (↑Γ(X, (↑V : X.Opens)) : Type u)
      (Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) (J.ideal V)))
have erw : LE.le (α := Submodule (↑Γ(X, (↑V : X.Opens)) : Type u) (↑Γ(X, X.basicOpen (r j)) : Type u))
  (Submodule.restrictScalars (↑Γ(X, (↑V : X.Opens)) : Type u) (R := (↑Γ(X, X.basicOpen (r j)) : Type u))
      (I.ideal (Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) (X.basicOpen (r j)) sorry)) :
    Submodule (↑Γ(X, (↑V : X.Opens)) : Type u) (↑Γ(X, X.basicOpen (r j)) : Type u))
  (Submodule.restrictScalars (↑Γ(X, (↑V : X.Opens)) : Type u) (R := (↑Γ(X, X.basicOpen (r j)) : Type u))
      (J.ideal (Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) (X.basicOpen (r j)) sorry)) :
    Submodule (↑Γ(X, (↑V : X.Opens)) : Type u) (↑Γ(X, X.basicOpen (r j)) : Type u))
Tactic: erw [I.map_ideal (U := ⟨_, V.2.basicOpen _⟩) (X.basicOpen_le (r j)),
    J.map_ideal (U := ⟨_, V.2.basicOpen _⟩) (X.basicOpen_le (r j))]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
Goal:
X : Scheme
I J : X.IdealSheafData
ι : Type u_1
U : ι → (↑X.affineOpens : Type u)
hU : Eq.{u + 1} (α := X.Opens) (⨆ (i : ι), (↑(U i) : X.Opens)) ⊤
H : ∀ (i : ι), LE.le (α := Ideal (↑Γ(X, (↑(U i) : X.Opens)) : Type u)) (I.ideal (U i)) (J.ideal (U i))
V : (↑X.affineOpens : Type u)
i : (x : ↥(↑V : X.Opens)) → ι
r : (x : ↥(↑V : X.Opens)) → (↑Γ(X, (↑V : X.Opens)) : Type u)
rU : (x : ↥(↑V : X.Opens)) → (↑Γ(X, (↑(U (i x)) : X.Opens)) : Type u)
e : ∀ (x : ↥(↑V : X.Opens)), X.basicOpen (r x) = X.basicOpen (rU x)
hxr : ∀ (x : ↥(↑V : X.Opens)), (↑x : ↥X) ∈ X.basicOpen (r x)
this : Eq (α := Ideal (↑Γ(X, (↑V : X.Opens)) : Type u)) (Ideal.span (Set.range r)) ⊤
inst : ∀ (f : (↑Γ(X, (↑V : X.Opens)) : Type u)), IsLocalization.Away f (↑Γ(X, X.basicOpen f) : Type u)
j : ↥(↑V : X.Opens)
⊢ LE.le (α := Submodule (↑Γ(X, (↑V : X.Opens)) : Type u) (↑Γ(X, X.basicOpen (r j)) : Type u))
    (Submodule.restrictScalars (↑Γ(X, (↑V : X.Opens)) : Type u) (R := (↑Γ(X, X.basicOpen (r j)) : Type u))
        (I.ideal (Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) (X.basicOpen (r j)) ⋯)) :
      Submodule (↑Γ(X, (↑V : X.Opens)) : Type u) (↑Γ(X, X.basicOpen (r j)) : Type u))
    (Submodule.restrictScalars (↑Γ(X, (↑V : X.Opens)) : Type u) (R := (↑Γ(X, X.basicOpen (r j)) : Type u))
        (J.ideal (Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) (X.basicOpen (r j)) ⋯)) :
      Submodule (↑Γ(X, (↑V : X.Opens)) : Type u) (↑Γ(X, X.basicOpen (r j)) : Type u))
have rw! : LE.le (α := Submodule (↑Γ(X, (↑V : X.Opens)) : Type u) (↑Γ(X, X.basicOpen (rU j)) : Type u))
  (Submodule.restrictScalars (↑Γ(X, (↑V : X.Opens)) : Type u) (R := (↑Γ(X, X.basicOpen (rU j)) : Type u))
      (I.ideal (Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) (X.basicOpen (rU j)) sorry)) :
    Submodule (↑Γ(X, (↑V : X.Opens)) : Type u) (↑Γ(X, X.basicOpen (rU j)) : Type u))
  (Submodule.restrictScalars (↑Γ(X, (↑V : X.Opens)) : Type u) (R := (↑Γ(X, X.basicOpen (rU j)) : Type u))
      (J.ideal (Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) (X.basicOpen (rU j)) sorry)) :
    Submodule (↑Γ(X, (↑V : X.Opens)) : Type u) (↑Γ(X, X.basicOpen (rU j)) : Type u))
Tactic: rw! [e]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
Goal:
X : Scheme
I J : X.IdealSheafData
ι : Type u_1
U : ι → (↑X.affineOpens : Type u)
hU : Eq.{u + 1} (α := X.Opens) (⨆ (i : ι), (↑(U i) : X.Opens)) ⊤
H : ∀ (i : ι), LE.le (α := Ideal (↑Γ(X, (↑(U i) : X.Opens)) : Type u)) (I.ideal (U i)) (J.ideal (U i))
V : (↑X.affineOpens : Type u)
i : (x : ↥(↑V : X.Opens)) → ι
r : (x : ↥(↑V : X.Opens)) → (↑Γ(X, (↑V : X.Opens)) : Type u)
rU : (x : ↥(↑V : X.Opens)) → (↑Γ(X, (↑(U (i x)) : X.Opens)) : Type u)
e : ∀ (x : ↥(↑V : X.Opens)), X.basicOpen (r x) = X.basicOpen (rU x)
hxr : ∀ (x : ↥(↑V : X.Opens)), (↑x : ↥X) ∈ X.basicOpen (r x)
this : Eq (α := Ideal (↑Γ(X, (↑V : X.Opens)) : Type u)) (Ideal.span (Set.range r)) ⊤
inst : ∀ (f : (↑Γ(X, (↑V : X.Opens)) : Type u)), IsLocalization.Away f (↑Γ(X, X.basicOpen f) : Type u)
j : ↥(↑V : X.Opens)
⊢ LE.le (α := Submodule (↑Γ(X, (↑V : X.Opens)) : Type u) (↑Γ(X, X.basicOpen (rU j)) : Type u))
    (Submodule.restrictScalars (↑Γ(X, (↑V : X.Opens)) : Type u) (R := (↑Γ(X, X.basicOpen (rU j)) : Type u))
        (I.ideal (Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) (X.basicOpen (rU j)) ⋯)) :
      Submodule (↑Γ(X, (↑V : X.Opens)) : Type u) (↑Γ(X, X.basicOpen (rU j)) : Type u))
    (Submodule.restrictScalars (↑Γ(X, (↑V : X.Opens)) : Type u) (R := (↑Γ(X, X.basicOpen (rU j)) : Type u))
        (J.ideal (Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) (X.basicOpen (rU j)) ⋯)) :
      Submodule (↑Γ(X, (↑V : X.Opens)) : Type u) (↑Γ(X, X.basicOpen (rU j)) : Type u))
have rw : LE.le (α := Submodule (↑Γ(X, (↑V : X.Opens)) : Type u) (↑Γ(X, X.basicOpen (rU j)) : Type u))
  (Submodule.restrictScalars (↑Γ(X, (↑V : X.Opens)) : Type u)
    (Ideal.map (R := (↑Γ(X, (↑(U (i j)) : X.Opens)) : Type u)) (CommRingCat.Hom.hom (X.presheaf.map (homOfLE sorry).op))
      (I.ideal (U (i j)))))
  (Submodule.restrictScalars (↑Γ(X, (↑V : X.Opens)) : Type u)
    (Ideal.map (R := (↑Γ(X, (↑(U (i j)) : X.Opens)) : Type u)) (CommRingCat.Hom.hom (X.presheaf.map (homOfLE sorry).op))
      (J.ideal (U (i j)))))
Tactic: rw [← I.map_ideal (V := (U _)) (X.basicOpen_le _), ← J.map_ideal (V := (U _)) (X.basicOpen_le _)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
Goal:
X : Scheme
I : X.IdealSheafData
U : (↑X.affineOpens : Type u)
⊢ X.zeroLocus (↑(I.ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u)) ∩ (↑(↑U : X.Opens) : Set ↥X) ⊆ I.supportSet
have rw : X.zeroLocus (↑(I.ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u)) ∩ (↑(↑U : X.Opens) : Set ↥X) ⊆
  ⋂ (U : (↑X.affineOpens : Type u)), X.zeroLocus (↑(I.ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u))
Tactic: rw [I.supportSet_eq_iInter_zeroLocus]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
Goal:
X : Scheme
I : X.IdealSheafData
U : (↑X.affineOpens : Type u)
⊢ X.zeroLocus (↑(I.ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u)) ∩ (↑(↑U : X.Opens) : Set ↥X) ⊆
    ⋂ (U : (↑X.affineOpens : Type u)), X.zeroLocus (↑(I.ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u))
have refine : ∀ (V : (↑X.affineOpens : Type u)),
  X.zeroLocus (↑(I.ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u)) ∩ (↑(↑U : X.Opens) : Set ↥X) ⊆
    X.zeroLocus (↑(I.ideal V) : Set (↑Γ(X, (↑V : X.Opens)) : Type u))
Tactic: refine Set.subset_iInter fun V ↦ ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (goal)
Goal:
X : Scheme
I : X.IdealSheafData
U V : (↑X.affineOpens : Type u)
⊢ X.zeroLocus (↑(I.ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u)) ∩ (↑(↑U : X.Opens) : Set ↥X) ⊆
    X.zeroLocus (↑(I.ideal V) : Set (↑Γ(X, (↑V : X.Opens)) : Type u))
have apply : X.zeroLocus (↑(I.ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u)) ∩ (↑(↑U : X.Opens) : Set ↥X) ⊓
    (↑(↑V : X.Opens) : Set ↥X) ≤
  X.zeroLocus (↑(I.ideal V) : Set (↑Γ(X, (↑V : X.Opens)) : Type u))
Tactic: apply (X.codisjoint_zeroLocus (U := V) (I.ideal V)).symm.left_le_of_le_inf_right
-- 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)
hx : x ∈ X.zeroLocus (↑(I.ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u))
hxU : x ∈ (↑(↑U : X.Opens) : Set ↥X)
⊢ x ∈ X.zeroLocus (↑(I.ideal V) : Set (↑Γ(X, (↑V : X.Opens)) : Type u))
have simp : ∀ (hx : ∀ f ∈ I.ideal U, x ∉ X.basicOpen f), ∀ f ∈ I.ideal V, x ∉ X.basicOpen f
Tactic: simp only [Scheme.mem_zeroLocus_iff, SetLike.mem_coe] at hx ⊢
Cleared hypotheses: hx
-- 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
⊢ False
have obtain : ∀ (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), False
Tactic: obtain ⟨f, g, hfg, hxf⟩ := exists_basicOpen_le_affine_inter U.2 V.2 x ⟨hxU, hxV⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (hypothesis)
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
⊢ False
have inst : IsLocalization.Away f (↑Γ(X, X.basicOpen f) : Type u)
Tactic: have inst := U.2.isLocalization_basicOpen f
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (hypothesis)
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)
⊢ False
have 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))
  (I.ideal (X.affineBasicOpen f))
  ((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))
Tactic: have := (I.map_ideal (U := X.affineBasicOpen f) (hfg.trans_le (X.basicOpen_le g))).le
    (Ideal.mem_map_of_mem _ hfU)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Basic (hypothesis)
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))
    (I.ideal (X.affineBasicOpen f))
    ((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 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 sorry).op)) (I.ideal 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))
Tactic: rw [← I.map_ideal_basicOpen] at this
Cleared hypotheses: this