awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I : X.IdealSheafData
U V : (↑X.affineOpens : Type u)
h : U ≤ V
x : ↥X
hxU : x ∈ (↑U : X.Opens)
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
this :
  Eq (α := Ideal (↑(X.presheaf.stalk x) : Type u))
    (Ideal.map (R := (↑(X.presheaf.obj (Opposite.op (X.basicOpen g))) : Type u)) (F :=
      (↑(X.presheaf.obj (Opposite.op (X.basicOpen g))) : Type u) →+* (↑(X.presheaf.stalk x) : Type u))
      (CommRingCat.Hom.hom (X.presheaf.germ (X.basicOpen g) x ⋯))
      (Ideal.map (F := (↑Γ(X, (↑U : X.Opens)) : Type u) →+* (↑Γ(X, (↑(X.affineBasicOpen g) : X.Opens)) : Type u))
        (CommRingCat.Hom.hom (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯)))) (I.ideal U)))
    (Ideal.map (R := (↑(X.presheaf.obj (Opposite.op (X.basicOpen g))) : Type u)) (F :=
      (↑(X.presheaf.obj (Opposite.op (X.basicOpen g))) : Type u) →+* (↑(X.presheaf.stalk x) : Type u))
      (CommRingCat.Hom.hom (X.presheaf.germ (X.basicOpen g) x ⋯))
      (Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) (I.ideal V)))
simp :
  ∀
    (this :
      Eq (α := Ideal (↑(X.presheaf.stalk x) : Type u))
        (Ideal.map (F := (↑Γ(X, (↑U : X.Opens)) : Type u) →+* (↑(X.presheaf.stalk x) : Type u))
          (CommRingCat.Hom.hom (X.presheaf.germ (↑U : X.Opens) x ⋯)) (I.ideal U))
        (Ideal.map (F := (↑Γ(X, (↑V : X.Opens)) : Type u) →+* (↑(X.presheaf.stalk x) : Type u))
          (CommRingCat.Hom.hom (X.presheaf.germ (↑V : X.Opens) x ⋯)) (I.ideal V))),
    Eq (α := Ideal (↑(X.presheaf.stalk x) : Type u))
      (Ideal.map (F := (↑Γ(X, (↑V : X.Opens)) : Type u) →+* (↑(X.presheaf.stalk x) : Type u))
        (CommRingCat.Hom.hom (X.presheaf.map (homOfLE h).op ≫ X.presheaf.germ (↑U : X.Opens) x hxU)) (I.ideal V))
      (Ideal.map (F := (↑(X.presheaf.obj (Opposite.op (↑U : X.Opens))) : Type u) →+* (↑(X.presheaf.stalk x) : Type u))
        (CommRingCat.Hom.hom (X.presheaf.germ (↑U : X.Opens) x hxU)) (I.ideal U))
⊢ Eq (α := Ideal (↑(X.presheaf.stalk x) : Type u))
    (Ideal.map (R := (↑Γ(X, (↑U : X.Opens)) : Type u)) (F :=
      (↑(X.presheaf.obj (Opposite.op (↑U : X.Opens))) : Type u) →+* (↑(X.presheaf.stalk x) : Type u))
      (CommRingCat.Hom.hom (X.presheaf.germ (↑U : X.Opens) x hxU))
      (Ideal.map (F := (↑Γ(X, (↑V : X.Opens)) : Type u) →+* (↑Γ(X, (↑U : X.Opens)) : Type u))
        (CommRingCat.Hom.hom (X.presheaf.map (homOfLE h).op)) (I.ideal V)))
    (Ideal.map (F := (↑(X.presheaf.obj (Opposite.op (↑U : X.Opens))) : Type u) →+* (↑(X.presheaf.stalk x) : Type u))
      (CommRingCat.Hom.hom (X.presheaf.germ (↑U : X.Opens) x hxU)) (I.ideal U))

Tactic:
simp only [Ideal.map_map, ← CommRingCat.hom_comp, affineBasicOpen_coe, X.presheaf.germ_res]
    at this ⊢

Premises used: CommRingCat.hom_comp, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, TopCat.Presheaf.germ_res, Ideal.map_map, AlgebraicGeometry.Scheme.affineBasicOpen_coe, AlgebraicGeometry.PresheafedSpace.presheaf, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, AlgebraicGeometry.Scheme.toLocallyRingedSpace
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I : X.IdealSheafData
U V : (↑X.affineOpens : Type u)
h : U ≤ V
x : ↥X
hxU : x ∈ (↑U : X.Opens)
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
this :
  Eq (α := Ideal (↑(X.presheaf.stalk x) : Type u))
    (Ideal.map (F := (↑Γ(X, (↑U : X.Opens)) : Type u) →+* (↑(X.presheaf.stalk x) : Type u))
      (CommRingCat.Hom.hom (X.presheaf.germ (↑U : X.Opens) x ⋯)) (I.ideal U))
    (Ideal.map (F := (↑Γ(X, (↑V : X.Opens)) : Type u) →+* (↑(X.presheaf.stalk x) : Type u))
      (CommRingCat.Hom.hom (X.presheaf.germ (↑V : X.Opens) x ⋯)) (I.ideal V))
⊢ Eq (α := Ideal (↑(X.presheaf.stalk x) : Type u))
    (Ideal.map (F := (↑Γ(X, (↑V : X.Opens)) : Type u) →+* (↑(X.presheaf.stalk x) : Type u))
      (CommRingCat.Hom.hom (X.presheaf.map (homOfLE h).op ≫ X.presheaf.germ (↑U : X.Opens) x hxU)) (I.ideal V))
    (Ideal.map (F := (↑(X.presheaf.obj (Opposite.op (↑U : X.Opens))) : Type u) →+* (↑(X.presheaf.stalk x) : Type u))
      (CommRingCat.Hom.hom (X.presheaf.germ (↑U : X.Opens) x hxU)) (I.ideal U))

Tactic:
simp only [homOfLE_leOfHom, TopCat.Presheaf.germ_res', this]

Premises used: TopCat.Presheaf.germ_res', CategoryTheory.homOfLE_leOfHom
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I : X.IdealSheafData
U V : (↑X.affineOpens : Type u)
h : Opposite.op (↑V : X.Opens) ⟶ Opposite.op (↑U : X.Opens)
⊢ Ideal.map (CommRingCat.Hom.hom (X.presheaf.map h)) (I.ideal V) = I.ideal U

Tactic:
map_ideal _ _

Premises used: Set.Mem, Quiver.Hom.op, AlgebraicGeometry.Scheme.IdealSheafData.map_ideal, CategoryTheory.homOfLE
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I : X.IdealSheafData
U V : (↑X.affineOpens : Type u)
h : U ≤ V
rw :
  Ideal.map (F := (↑Γ(X, (↑V : X.Opens)) : Type u) →+* (↑Γ(X, (↑U : X.Opens)) : Type u))
      (CommRingCat.Hom.hom (X.presheaf.map (homOfLE h).op)) (I.ideal V) ≤
    I.ideal U
rw₁ rw₂ :
  LE.le (α := Ideal (↑Γ(X, (↑U : X.Opens)) : Type u))
    (Ideal.map (F := (↑Γ(X, (↑V : X.Opens)) : Type u) →+* (↑Γ(X, (↑U : X.Opens)) : Type u))
      (CommRingCat.Hom.hom (X.presheaf.map (homOfLE h).op)) (I.ideal V))
    (Ideal.map (F := (↑Γ(X, (↑V : X.Opens)) : Type u) →+* (↑Γ(X, (↑U : X.Opens)) : Type u))
      (CommRingCat.Hom.hom (X.presheaf.map (homOfLE h).op)) (I.ideal V))
⊢ I.ideal V ≤
    Ideal.comap (F := (↑Γ(X, (↑V : X.Opens)) : Type u) →+* (↑Γ(X, (↑U : X.Opens)) : Type u))
      (CommRingCat.Hom.hom (X.presheaf.map (homOfLE h).op)) (I.ideal U)

Tactic:
rw [← Ideal.map_le_iff_le_comap, ← I.map_ideal h]

Premises used: AlgebraicGeometry.Scheme.IdealSheafData.map_ideal, Ideal.map_le_iff_le_comap
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
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)
x : ↥X
hxV : x ∈ (↑V : X.Opens)
obtain :
  ∀ (i : ι) (hi : x ∈ (↑(U i) : X.Opens)),
    ∃ (i : ι) (r : (↑Γ(X, (↑V : X.Opens)) : Type u)) (rU : (↑Γ(X, (↑(U i) : X.Opens)) : Type u)),
      X.basicOpen r = X.basicOpen rU ∧
        (↑(Subtype.mk (p := fun (x : ↥X) ↦ x ∈ (↑V : X.Opens)) x hxV) : ↥X) ∈ X.basicOpen r
⊢ ∃ (i : ι) (r : (↑Γ(X, (↑V : X.Opens)) : Type u)) (rU : (↑Γ(X, (↑(U i) : X.Opens)) : Type u)),
    X.basicOpen r = X.basicOpen rU ∧ (↑(Subtype.mk (p := fun (x : ↥X) ↦ x ∈ (↑V : X.Opens)) x hxV) : ↥X) ∈ X.basicOpen r

Tactic:
obtain ⟨i, hi⟩ := TopologicalSpace.Opens.mem_iSup.mp (hU.ge (Set.mem_univ x))

Premises used: Eq.ge, TopologicalSpace.Opens.mem_iSup, Iff.mp, Set.mem_univ
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
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)
x : ↥X
hxV : x ∈ (↑V : X.Opens)
i : ι
hi : x ∈ (↑(U i) : X.Opens)
⊢ ∃ (i : ι) (r : (↑Γ(X, (↑V : X.Opens)) : Type u)) (rU : (↑Γ(X, (↑(U i) : X.Opens)) : Type u)),
    X.basicOpen r = X.basicOpen rU ∧ (↑(Subtype.mk (p := fun (x : ↥X) ↦ x ∈ (↑V : X.Opens)) x hxV) : ↥X) ∈ X.basicOpen r

Tactic:
⟨i, exists_basicOpen_le_affine_inter V.2 (U i).2 _ ⟨hxV, hi⟩⟩

Premises used: And.intro, Exists.intro, AlgebraicGeometry.exists_basicOpen_le_affine_inter, Subtype.property
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
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)
x : ↥X
hxV : x ∈ (↑V : X.Opens)
i : ι
hi : x ∈ (↑(U i) : X.Opens)
⊢ ∃ (i : ι) (r : (↑Γ(X, (↑V : X.Opens)) : Type u)) (rU : (↑Γ(X, (↑(U i) : X.Opens)) : Type u)),
    X.basicOpen r = X.basicOpen rU ∧ (↑(Subtype.mk (p := fun (x : ↥X) ↦ x ∈ (↑V : X.Opens)) x hxV) : ↥X) ∈ X.basicOpen r

Tactic:
exact ⟨i, exists_basicOpen_le_affine_inter V.2 (U i).2 _ ⟨hxV, hi⟩⟩
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
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)
⊢ ∀ (x : ↥(↑V : X.Opens)),
    ∃ (i : ι) (r : (↑Γ(X, (↑V : X.Opens)) : Type u)) (rU : (↑Γ(X, (↑(U i) : X.Opens)) : Type u)),
      X.basicOpen r = X.basicOpen rU ∧ (↑x : ↥X) ∈ X.basicOpen r

Tactic:
have : ∀ x : V.1, ∃ (i : ι) (r : Γ(X, V.1)) (rU : Γ(X, U i)),
      X.basicOpen r = X.basicOpen rU ∧ x.1 ∈ X.basicOpen r := by
    intro ⟨x, hxV⟩
    obtain ⟨i, hi⟩ := TopologicalSpace.Opens.mem_iSup.mp (hU.ge (Set.mem_univ x))
    exact ⟨i, exists_basicOpen_le_affine_inter V.2 (U i).2 _ ⟨hxV, hi⟩⟩
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
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)
this :
  ∀ (x : ↥(↑V : X.Opens)),
    ∃ (i : ι) (r : (↑Γ(X, (↑V : X.Opens)) : Type u)) (rU : (↑Γ(X, (↑(U i) : X.Opens)) : Type u)),
      X.basicOpen r = X.basicOpen rU ∧ (↑x : ↥X) ∈ X.basicOpen r
choose :
  ∀ (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
⊢ I.ideal V ≤ J.ideal V

Tactic:
choose i r rU e hxr using this
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
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)
rw : (↑V : X.Opens) ≤ ⨆ (f : (↑(Set.range r) : Type u)), X.basicOpen (↑f : (↑Γ(X, (↑V : X.Opens)) : Type u))
⊢ Eq (α := Ideal (↑Γ(X, (↑V : X.Opens)) : Type u)) (Ideal.span (Set.range r)) ⊤

Tactic:
rw [← V.2.self_le_iSup_basicOpen_iff]

Premises used: AlgebraicGeometry.IsAffineOpen.self_le_iSup_basicOpen_iff, Subtype.property
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
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)
⊢ (↑V : X.Opens) ≤ ⨆ (f : (↑(Set.range r) : Type u)), X.basicOpen (↑f : (↑Γ(X, (↑V : X.Opens)) : Type u))

Tactic:
fun x hxV ↦ TopologicalSpace.Opens.mem_iSup.mpr ⟨⟨_, _, rfl⟩, hxr ⟨x, hxV⟩⟩

Premises used: Iff.mpr, Set.Mem, TopologicalSpace.Opens.mem_iSup, Subtype.mk, Exists.intro, rfl
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
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)
⊢ (↑V : X.Opens) ≤ ⨆ (f : (↑(Set.range r) : Type u)), X.basicOpen (↑f : (↑Γ(X, (↑V : X.Opens)) : Type u))

Tactic:
exact fun x hxV ↦ TopologicalSpace.Opens.mem_iSup.mpr ⟨⟨_, _, rfl⟩, hxr ⟨x, hxV⟩⟩

Premises used: Iff.mpr, TopologicalSpace.Opens.mem_iSup, Exists.intro
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
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)) ⊤

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⟩⟩
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
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)) ⊤
⊢ ∀ (f : (↑Γ(X, (↑V : X.Opens)) : Type u)), IsLocalization.Away f (↑Γ(X, X.basicOpen f) : Type u)

Tactic:
have inst := V.2.isLocalization_basicOpen
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
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

Tactic:
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)) ?_

Premises used: CommRingCat.carrier, Set.Mem, Algebra.linearMap, Submodule.le_of_isLocalized_span, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, Opposite.op, AlgebraicGeometry.Scheme.basicOpen, AlgebraicGeometry.PresheafedSpace.presheaf, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, Subtype.val, CategoryTheory.Functor.obj, AlgebraicGeometry.Scheme.toLocallyRingedSpace
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
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)
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))
⊢ I.ideal V ≤ 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)) ?_

Premises used: CommRingCat.carrier, Algebra.linearMap, Submodule.le_of_isLocalized_span, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, Opposite.op, AlgebraicGeometry.Scheme.basicOpen, AlgebraicGeometry.PresheafedSpace.presheaf, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, Subtype.val, CategoryTheory.Functor.obj, AlgebraicGeometry.Scheme.toLocallyRingedSpace
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
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)
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))
⊢ 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))

Tactic:
dsimp
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
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)
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 ⋯).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)))
⊢ 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:
simp +instances only [← Submodule.restrictScalars_localized' Γ(X, X.basicOpen (r j)),
    Ideal.localized'_eq_map, RingHom.algebraMap_toAlgebra]

Premises used: CommRingCat.carrier, Ideal.localized'_eq_map, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, Opposite.op, AlgebraicGeometry.Scheme.basicOpen, AlgebraicGeometry.PresheafedSpace.presheaf, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, RingHom.algebraMap_toAlgebra, Submodule.restrictScalars_localized', CategoryTheory.Functor.obj, AlgebraicGeometry.Scheme.toLocallyRingedSpace