awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I J : X.IdealSheafData
U : (↑X.affineOpens : Type u)
f : (↑Γ(X, (↑U : X.Opens)) : Type u)
this :
  CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op) =
    algebraMap (↑Γ(X, (↑U : X.Opens)) : Type u) (↑Γ(X, X.basicOpen f) : Type u)
inst : IsLocalization.Away f (↑Γ(X, X.basicOpen f) : Type u)
h :
  ∀ (x : (↑Γ(X, X.basicOpen f) : Type u)),
    Membership.mem (γ := Ideal (↑Γ(X, X.basicOpen f) : Type u))
        (Ideal.map (F := (↑Γ(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)) (I.ideal U ⊓ J.ideal U))
        x ↔
      Membership.mem (γ := Ideal (↑Γ(X, X.basicOpen f) : Type u))
        (Ideal.map (F := (↑Γ(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)) (I.ideal U) ⊓
          Ideal.map (F := (↑Γ(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)) (J.ideal U))
        x
⊢ Eq (α := Ideal (↑Γ(X, X.basicOpen f) : Type u))
    (Ideal.map (F := (↑Γ(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)) (I.ideal U ⊓ J.ideal U))
    (Ideal.map (F := (↑Γ(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)) (I.ideal U) ⊓
      Ideal.map (F := (↑Γ(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)) (J.ideal U))

Tactic:
ext x
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I J : X.IdealSheafData
U : (↑X.affineOpens : Type u)
f : (↑Γ(X, (↑U : X.Opens)) : Type u)
this :
  CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op) =
    algebraMap (↑Γ(X, (↑U : X.Opens)) : Type u) (↑Γ(X, X.basicOpen f) : Type u)
inst : IsLocalization.Away f (↑Γ(X, X.basicOpen f) : Type u)
x : (↑Γ(X, X.basicOpen f) : Type u)
h :
  ∀ (x : (↑Γ(X, (↑U : X.Opens)) : Type u)) (s : ↥(Submonoid.powers f)),
    Membership.mem (γ := Ideal (↑Γ(X, X.basicOpen f) : Type u))
        (Ideal.map (F := (↑Γ(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)) (I.ideal U ⊓ J.ideal U))
        (IsLocalization.mk' (↑Γ(X, X.basicOpen f) : Type u) x s) ↔
      Membership.mem (γ := Ideal (↑Γ(X, X.basicOpen f) : Type u))
        (Ideal.map (F := (↑Γ(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)) (I.ideal U) ⊓
          Ideal.map (F := (↑Γ(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)) (J.ideal U))
        (IsLocalization.mk' (↑Γ(X, X.basicOpen f) : Type u) x s)
⊢ Membership.mem (γ := Ideal (↑Γ(X, X.basicOpen f) : Type u))
      (Ideal.map (F := (↑Γ(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)) (I.ideal U ⊓ J.ideal U))
      x ↔
    Membership.mem (γ := Ideal (↑Γ(X, X.basicOpen f) : Type u))
      (Ideal.map (F := (↑Γ(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)) (I.ideal U) ⊓
        Ideal.map (F := (↑Γ(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)) (J.ideal U))
      x

Tactic:
obtain ⟨x, s, rfl⟩ := IsLocalization.exists_mk'_eq (.powers f) x

Premises used: Submonoid.powers, rfl, IsLocalization.exists_mk'_eq
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I J : X.IdealSheafData
U : (↑X.affineOpens : Type u)
f : (↑Γ(X, (↑U : X.Opens)) : Type u)
this :
  CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op) =
    algebraMap (↑Γ(X, (↑U : X.Opens)) : Type u) (↑Γ(X, X.basicOpen f) : Type u)
inst : IsLocalization.Away f (↑Γ(X, X.basicOpen f) : Type u)
x : (↑Γ(X, (↑U : X.Opens)) : Type u)
s : ↥(Submonoid.powers f)
h :
  (∃ (a : ℕ), f ^ a * x ∈ I.ideal U ∧ f ^ a * x ∈ J.ideal U) ↔
    (∃ (a : ℕ), f ^ a * x ∈ I.ideal U) ∧ ∃ (a : ℕ), f ^ a * x ∈ J.ideal U
⊢ Membership.mem (γ := Ideal (↑Γ(X, X.basicOpen f) : Type u))
      (Ideal.map (F := (↑Γ(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)) (I.ideal U ⊓ J.ideal U))
      (IsLocalization.mk' (↑Γ(X, X.basicOpen f) : Type u) x s) ↔
    Membership.mem (γ := Ideal (↑Γ(X, X.basicOpen f) : Type u))
      (Ideal.map (F := (↑Γ(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)) (I.ideal U) ⊓
        Ideal.map (F := (↑Γ(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)) (J.ideal U))
      (IsLocalization.mk' (↑Γ(X, X.basicOpen f) : Type u) x s)

Tactic:
simp only [IsLocalization.mk'_mem_map_algebraMap_iff, Submonoid.mem_powers_iff, Ideal.mem_inf,
        exists_exists_eq_and]

Premises used: IsLocalization.mk'_mem_map_algebraMap_iff, exists_exists_eq_and, Ideal.mem_inf, Submonoid.mem_powers_iff
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I J : X.IdealSheafData
U : (↑X.affineOpens : Type u)
f : (↑Γ(X, (↑U : X.Opens)) : Type u)
this :
  CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op) =
    algebraMap (↑Γ(X, (↑U : X.Opens)) : Type u) (↑Γ(X, X.basicOpen f) : Type u)
inst : IsLocalization.Away f (↑Γ(X, X.basicOpen f) : Type u)
x : (↑Γ(X, (↑U : X.Opens)) : Type u)
s : ↥(Submonoid.powers f)
⊢ (∃ (a : ℕ), f ^ a * x ∈ I.ideal U ∧ f ^ a * x ∈ J.ideal U) ↔
    (∃ (a : ℕ), f ^ a * x ∈ I.ideal U) ∧ ∃ (a : ℕ), f ^ a * x ∈ J.ideal U

Tactic:
⟨fun ⟨n, h₁, h₂⟩ ↦ ⟨⟨n, h₁⟩, ⟨n, h₂⟩⟩, ?_⟩

Premises used: HMul.hMul, Membership.mem, Exists, _private.0.AlgebraicGeometry.Scheme.IdealSheafData.instSemilatticeInf.match_4, And, HPow.hPow, And.intro, Iff.intro, Exists.intro, AlgebraicGeometry.Scheme.IdealSheafData.ideal
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I J : X.IdealSheafData
U : (↑X.affineOpens : Type u)
f : (↑Γ(X, (↑U : X.Opens)) : Type u)
this :
  CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op) =
    algebraMap (↑Γ(X, (↑U : X.Opens)) : Type u) (↑Γ(X, X.basicOpen f) : Type u)
inst : IsLocalization.Away f (↑Γ(X, X.basicOpen f) : Type u)
x : (↑Γ(X, (↑U : X.Opens)) : Type u)
s : ↥(Submonoid.powers f)
h :
  ((∃ (a : ℕ), f ^ a * x ∈ I.ideal U) ∧ ∃ (a : ℕ), f ^ a * x ∈ J.ideal U) →
    ∃ (a : ℕ), f ^ a * x ∈ I.ideal U ∧ f ^ a * x ∈ J.ideal U
⊢ (∃ (a : ℕ), f ^ a * x ∈ I.ideal U ∧ f ^ a * x ∈ J.ideal U) ↔
    (∃ (a : ℕ), f ^ a * x ∈ I.ideal U) ∧ ∃ (a : ℕ), f ^ a * x ∈ J.ideal U

Tactic:
refine ⟨fun ⟨n, h₁, h₂⟩ ↦ ⟨⟨n, h₁⟩, ⟨n, h₂⟩⟩, ?_⟩
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I J : X.IdealSheafData
U : (↑X.affineOpens : Type u)
f : (↑Γ(X, (↑U : X.Opens)) : Type u)
this :
  CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op) =
    algebraMap (↑Γ(X, (↑U : X.Opens)) : Type u) (↑Γ(X, X.basicOpen f) : Type u)
inst : IsLocalization.Away f (↑Γ(X, X.basicOpen f) : Type u)
x : (↑Γ(X, (↑U : X.Opens)) : Type u)
s : ↥(Submonoid.powers f)
n₁ : ℕ
h₁ : f ^ n₁ * x ∈ I.ideal U
n₂ : ℕ
h₂ : f ^ n₂ * x ∈ J.ideal U
⊢ ∃ (a : ℕ), f ^ a * x ∈ I.ideal U ∧ f ^ a * x ∈ J.ideal U

Tactic:
⟨n₁ + n₂, ?_, ?_⟩

Premises used: HAdd.hAdd, And.intro, Exists.intro
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I J : X.IdealSheafData
U : (↑X.affineOpens : Type u)
f : (↑Γ(X, (↑U : X.Opens)) : Type u)
this :
  CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op) =
    algebraMap (↑Γ(X, (↑U : X.Opens)) : Type u) (↑Γ(X, X.basicOpen f) : Type u)
inst : IsLocalization.Away f (↑Γ(X, X.basicOpen f) : Type u)
x : (↑Γ(X, (↑U : X.Opens)) : Type u)
s : ↥(Submonoid.powers f)
n₁ : ℕ
h₁ : f ^ n₁ * x ∈ I.ideal U
n₂ : ℕ
h₂ : f ^ n₂ * x ∈ J.ideal U
h : f ^ (n₁ + n₂) * x ∈ I.ideal U
h₃ : f ^ (n₁ + n₂) * x ∈ J.ideal U
⊢ ∃ (a : ℕ), f ^ a * x ∈ I.ideal U ∧ f ^ a * x ∈ J.ideal U

Tactic:
refine ⟨n₁ + n₂, ?_, ?_⟩
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I J : X.IdealSheafData
U : (↑X.affineOpens : Type u)
f : (↑Γ(X, (↑U : X.Opens)) : Type u)
this :
  CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op) =
    algebraMap (↑Γ(X, (↑U : X.Opens)) : Type u) (↑Γ(X, X.basicOpen f) : Type u)
inst : IsLocalization.Away f (↑Γ(X, X.basicOpen f) : Type u)
x : (↑Γ(X, (↑U : X.Opens)) : Type u)
s : ↥(Submonoid.powers f)
n₁ : ℕ
h₁ : f ^ n₁ * x ∈ I.ideal U
n₂ : ℕ
h₂ : f ^ n₂ * x ∈ J.ideal U
h : f ^ n₂ * (f ^ n₁ * x) ∈ I.ideal U
⊢ f ^ (n₁ + n₂) * x ∈ I.ideal U

Tactic:
rw [add_comm, pow_add, mul_assoc]

Premises used: mul_assoc, pow_add, add_comm
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I J : X.IdealSheafData
U : (↑X.affineOpens : Type u)
f : (↑Γ(X, (↑U : X.Opens)) : Type u)
this :
  CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op) =
    algebraMap (↑Γ(X, (↑U : X.Opens)) : Type u) (↑Γ(X, X.basicOpen f) : Type u)
inst : IsLocalization.Away f (↑Γ(X, X.basicOpen f) : Type u)
x : (↑Γ(X, (↑U : X.Opens)) : Type u)
s : ↥(Submonoid.powers f)
n₁ : ℕ
h₁ : f ^ n₁ * x ∈ I.ideal U
n₂ : ℕ
h₂ : f ^ n₂ * x ∈ J.ideal U
⊢ f ^ n₂ * (f ^ n₁ * x) ∈ I.ideal U

Tactic:
Ideal.mul_mem_left _ _ h₁

Premises used: Set.Mem, Ideal.mul_mem_left
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I J : X.IdealSheafData
U : (↑X.affineOpens : Type u)
f : (↑Γ(X, (↑U : X.Opens)) : Type u)
this :
  CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op) =
    algebraMap (↑Γ(X, (↑U : X.Opens)) : Type u) (↑Γ(X, X.basicOpen f) : Type u)
inst : IsLocalization.Away f (↑Γ(X, X.basicOpen f) : Type u)
x : (↑Γ(X, (↑U : X.Opens)) : Type u)
s : ↥(Submonoid.powers f)
n₁ : ℕ
h₁ : f ^ n₁ * x ∈ I.ideal U
n₂ : ℕ
h₂ : f ^ n₂ * x ∈ J.ideal U
⊢ f ^ n₂ * (f ^ n₁ * x) ∈ I.ideal U

Tactic:
exact Ideal.mul_mem_left _ _ h₁

Premises used: Ideal.mul_mem_left
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I J : X.IdealSheafData
U : (↑X.affineOpens : Type u)
f : (↑Γ(X, (↑U : X.Opens)) : Type u)
this :
  CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op) =
    algebraMap (↑Γ(X, (↑U : X.Opens)) : Type u) (↑Γ(X, X.basicOpen f) : Type u)
inst : IsLocalization.Away f (↑Γ(X, X.basicOpen f) : Type u)
x : (↑Γ(X, (↑U : X.Opens)) : Type u)
s : ↥(Submonoid.powers f)
n₁ : ℕ
h₁ : f ^ n₁ * x ∈ I.ideal U
n₂ : ℕ
h₂ : f ^ n₂ * x ∈ J.ideal U
h : f ^ n₁ * (f ^ n₂ * x) ∈ J.ideal U
⊢ f ^ (n₁ + n₂) * x ∈ J.ideal U

Tactic:
rw [pow_add, mul_assoc]

Premises used: mul_assoc, pow_add
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I J : X.IdealSheafData
U : (↑X.affineOpens : Type u)
f : (↑Γ(X, (↑U : X.Opens)) : Type u)
this :
  CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op) =
    algebraMap (↑Γ(X, (↑U : X.Opens)) : Type u) (↑Γ(X, X.basicOpen f) : Type u)
inst : IsLocalization.Away f (↑Γ(X, X.basicOpen f) : Type u)
x : (↑Γ(X, (↑U : X.Opens)) : Type u)
s : ↥(Submonoid.powers f)
n₁ : ℕ
h₁ : f ^ n₁ * x ∈ I.ideal U
n₂ : ℕ
h₂ : f ^ n₂ * x ∈ J.ideal U
⊢ f ^ n₁ * (f ^ n₂ * x) ∈ J.ideal U

Tactic:
Ideal.mul_mem_left _ _ h₂

Premises used: Set.Mem, Ideal.mul_mem_left
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I J : X.IdealSheafData
U : (↑X.affineOpens : Type u)
f : (↑Γ(X, (↑U : X.Opens)) : Type u)
this :
  CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op) =
    algebraMap (↑Γ(X, (↑U : X.Opens)) : Type u) (↑Γ(X, X.basicOpen f) : Type u)
inst : IsLocalization.Away f (↑Γ(X, X.basicOpen f) : Type u)
x : (↑Γ(X, (↑U : X.Opens)) : Type u)
s : ↥(Submonoid.powers f)
n₁ : ℕ
h₁ : f ^ n₁ * x ∈ I.ideal U
n₂ : ℕ
h₂ : f ^ n₂ * x ∈ J.ideal U
⊢ f ^ n₁ * (f ^ n₂ * x) ∈ J.ideal U

Tactic:
exact Ideal.mul_mem_left _ _ h₂

Premises used: Ideal.mul_mem_left
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
⊢ Eq.{u + 1} (α := (U : (↑X.affineOpens : Type u)) → Ideal (↑Γ(X, (↑U : X.Opens)) : Type u)) (ideal ⊤) ⊤

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
⊢ Eq.{u + 1} (α := (U : (↑X.affineOpens : Type u)) → Ideal (↑Γ(X, (↑U : X.Opens)) : Type u)) (ideal ⊥) ⊥

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I J : X.IdealSheafData
⊢ (I ⊔ J).ideal = I.ideal ⊔ J.ideal

Tactic:
rfl

Premises used: Set.Mem, setOf, rfl
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I : Set X.IdealSheafData
⊢ (sSup I).ideal = sSup (ideal '' I)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
ι : Type u_1
I : ι → X.IdealSheafData
rw : (sSup (Set.range I)).ideal = ⨆ (i : ι), (I i).ideal
rw₁ : (sSup (Set.range I)).ideal = sSup (Set.range fun (i : ι) ↦ (I i).ideal)
rw₂ : sSup (ideal '' Set.range I) = sSup (Set.range fun (i : ι) ↦ (I i).ideal)
rw₃ : sSup (Set.range (ideal ∘ I)) = sSup (Set.range fun (i : ι) ↦ (I i).ideal)
rw₄ rw₅ :
  Eq.{u + 1} (α := (U : (↑X.affineOpens : Type u)) → Ideal (↑Γ(X, (↑U : X.Opens)) : Type u))
    (sSup (Set.range fun (x : ι) ↦ (I x).ideal)) (sSup (Set.range fun (i : ι) ↦ (I i).ideal))
⊢ (iSup I).ideal = ⨆ (i : ι), (I i).ideal

Tactic:
rw [← sSup_range, ← sSup_range, ideal_sSup, ← Set.range_comp, Function.comp_def]

Premises used: Set.range_comp, AlgebraicGeometry.Scheme.IdealSheafData.ideal_sSup, Function.comp_def, sSup_range
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I J : X.IdealSheafData
⊢ (I ⊓ J).ideal = I.ideal ⊓ J.ideal

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
ι : Type u_1
I : ι → X.IdealSheafData
s : Set ι
hs : s.Finite
⊢ Eq.{u + 1} (α := (U : (↑X.affineOpens : Type u)) → Ideal (↑Γ(X, (↑U : X.Opens)) : Type u))
    (ideal (⨅ (i : ι), ⨅ (_ : Membership.mem (γ := Set ι) ∅ i), I i))
    (⨅ (i : ι), ⨅ (_ : Membership.mem (γ := Set ι) ∅ i), (I i).ideal)

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
ι : Type u_1
I : ι → X.IdealSheafData
s : Set ι
hs : s.Finite
refine :
  ∀ {i : ι} {s : Set ι} (his : i ∉ s) (hs : s.Finite)
    (e :
      Eq.{u + 1} (α := (U : (↑X.affineOpens : Type u)) → Ideal (↑Γ(X, (↑U : X.Opens)) : Type u)) (ideal (⨅ i ∈ s, I i))
        (⨅ i ∈ s, (I i).ideal)),
    Eq.{u + 1} (α := (U : (↑X.affineOpens : Type u)) → Ideal (↑Γ(X, (↑U : X.Opens)) : Type u))
      (ideal (⨅ i_1 ∈ insert i s, I i_1)) (⨅ i_1 ∈ insert i s, (I i_1).ideal)
⊢ Eq.{u + 1} (α := (U : (↑X.affineOpens : Type u)) → Ideal (↑Γ(X, (↑U : X.Opens)) : Type u)) (ideal (⨅ i ∈ s, I i))
    (⨅ i ∈ s, (I i).ideal)

Tactic:
refine hs.induction_on _ (by simp) fun {i s} his hs e ↦ ?_
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
ι : Type u_1
I : ι → X.IdealSheafData
s_1 : Set ι
hs_1 : s_1.Finite
i : ι
s : Set ι
his : i ∉ s
hs : s.Finite
e :
  Eq.{u + 1} (α := (U : (↑X.affineOpens : Type u)) → Ideal (↑Γ(X, (↑U : X.Opens)) : Type u)) (ideal (⨅ i ∈ s, I i))
    (⨅ i ∈ s, (I i).ideal)
⊢ Eq.{u + 1} (α := (U : (↑X.affineOpens : Type u)) → Ideal (↑Γ(X, (↑U : X.Opens)) : Type u))
    (ideal (⨅ i_1 ∈ insert i s, I i_1)) (⨅ i_1 ∈ insert i s, (I i_1).ideal)

Tactic:
simp only [iInf_insert, e, ideal_inf]

Premises used: AlgebraicGeometry.Scheme.IdealSheafData.ideal_inf, iInf_insert
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
ι : Type u_1
I : ι → X.IdealSheafData
inst : Finite ι
⊢ Eq.{u + 1} (α := (U : (↑X.affineOpens : Type u)) → Ideal (↑Γ(X, (↑U : X.Opens)) : Type u)) (ideal (⨅ (i : ι), I i))
    (⨅ (i : ι), (I i).ideal)

Tactic:
simpa using ideal_biInf I Set.finite_univ

Premises used: Set.finite_univ, AlgebraicGeometry.Scheme.IdealSheafData.ideal_biInf
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I : X.IdealSheafData
U V : (↑X.affineOpens : Type u)
f : (↑Γ(X, (↑U : X.Opens)) : Type u)
hV : V = X.affineBasicOpen f
subst :
  Eq (α := Ideal (↑Γ(X, (↑(X.affineBasicOpen f) : X.Opens)) : Type u))
    (Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) (I.ideal U)) (I.ideal (X.affineBasicOpen f))
⊢ Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) (I.ideal U) = I.ideal V

Tactic:
subst hV
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I : X.IdealSheafData
U : (↑X.affineOpens : Type u)
f : (↑Γ(X, (↑U : X.Opens)) : Type u)
⊢ Eq (α := Ideal (↑Γ(X, (↑(X.affineBasicOpen f) : X.Opens)) : Type u))
    (Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) (I.ideal U)) (I.ideal (X.affineBasicOpen f))

Tactic:
I.map_ideal_basicOpen _ _

Premises used: AlgebraicGeometry.RingedSpace.basicOpen, AlgebraicGeometry.Scheme.basicOpen, AlgebraicGeometry.Scheme.IdealSheafData.map_ideal_basicOpen
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I : X.IdealSheafData
U : (↑X.affineOpens : Type u)
f : (↑Γ(X, (↑U : X.Opens)) : Type u)
⊢ Eq (α := Ideal (↑Γ(X, (↑(X.affineBasicOpen f) : X.Opens)) : Type u))
    (Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) (I.ideal U)) (I.ideal (X.affineBasicOpen f))

Tactic:
exact I.map_ideal_basicOpen _ _

Premises used: AlgebraicGeometry.Scheme.IdealSheafData.map_ideal_basicOpen
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Goal:
X : Scheme
I : X.IdealSheafData
U V : (↑X.affineOpens : Type u)
h : U ≤ V
rw :
  ∀ (x : ↥X) (h_1 : x ∈ (↑U : X.Opens)),
    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 h_1))
        (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 h_1)) (I.ideal 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) =
    I.ideal U

Tactic:
rw [U.2.ideal_ext_iff]

Premises used: Subtype.property, AlgebraicGeometry.IsAffineOpen.ideal_ext_iff
-- 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)
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),
    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))
⊢ 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:
obtain ⟨f, g, hfg, hxf⟩ := exists_basicOpen_le_affine_inter U.2 V.2 x ⟨hxU, h hxU⟩

Premises used: And.intro, AlgebraicGeometry.exists_basicOpen_le_affine_inter, Subtype.property
-- 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
⊢ Eq (α := Ideal (↑Γ(X, (↑(X.affineBasicOpen g) : X.Opens)) : Type u))
    (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))
    (I.ideal (X.affineBasicOpen g))

Tactic:
have := I.map_ideal_basicOpen_of_eq (V := X.affineBasicOpen g) f (Subtype.ext hfg.symm)
-- 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, (↑(X.affineBasicOpen g) : X.Opens)) : Type u))
    (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))
    (I.ideal (X.affineBasicOpen g))
⊢ Eq (α := Ideal (↑Γ(X, (↑(X.affineBasicOpen g) : X.Opens)) : Type u))
    (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 (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) (I.ideal V))

Tactic:
rw [← I.map_ideal_basicOpen] at this

Premises used: AlgebraicGeometry.Scheme.IdealSheafData.map_ideal_basicOpen
-- 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, (↑(X.affineBasicOpen g) : X.Opens)) : Type u))
    (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 (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) (I.ideal V))
⊢ 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)))

Tactic:
apply_fun Ideal.map (X.presheaf.germ (X.basicOpen g) x (hfg ▸ hxf)).hom at this

Premises used: CommRingCat.Hom.hom, Eq.rec, Ideal.map, TopCat.Presheaf.germ, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, AlgebraicGeometry.Scheme.basicOpen, AlgebraicGeometry.PresheafedSpace.presheaf, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, AlgebraicGeometry.Scheme.toLocallyRingedSpace