awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
U : Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)
x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)
hx : x ∈ U
s :
  (↑(Functor.obj
        (ObjectProperty.FullSubcategory.obj (P :=
            (CategoryTheory.Presheaf.IsSheaf (grothendieckTopology (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) :
              (P : (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ ⥤ CommRingCat) → Prop))
            (Proj.structureSheaf 𝒜 : TopCat.Sheaf CommRingCat (ProjectiveSpectrum.top 𝒜)) :
          (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ ⥤ CommRingCat)
        (op U)) :
    Type u_1)
⊢ (ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
          CommRingCat.carrier) (X := Presheaf.stalk (Sheaf.presheaf (Proj.structureSheaf 𝒜)) x)
          (stalkToFiberRingHom 𝒜 x) :
        (a : (↑((Proj.structureSheaf 𝒜).presheaf.stalk x) : Type u_1)) → (↑(CommRingCat.of (at x)) : Type u_1))
      (((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
              CommRingCat.carrier) (X :=
              Functor.obj (Sheaf.presheaf (Proj.structureSheaf 𝒜) : Presheaf CommRingCat (ProjectiveSpectrum.top 𝒜))
                (op U))
              (Y := Presheaf.stalk (Sheaf.presheaf (Proj.structureSheaf 𝒜)) x)
              (Presheaf.germ (Sheaf.presheaf (Proj.structureSheaf 𝒜)) U x hx :
                Functor.obj (Sheaf.presheaf (Proj.structureSheaf 𝒜) : Presheaf CommRingCat (ProjectiveSpectrum.top 𝒜))
                    (op U) ⟶
                  Presheaf.stalk (Sheaf.presheaf (Proj.structureSheaf 𝒜)) x) :
            (↑(Functor.obj (Sheaf.presheaf (Proj.structureSheaf 𝒜) : Presheaf CommRingCat (ProjectiveSpectrum.top 𝒜))
                    (op U)) :
                Type u_1) →+*
              (↑(Presheaf.stalk (Sheaf.presheaf (Proj.structureSheaf 𝒜)) x) : Type u_1)) :
          (a : (↑((Proj.structureSheaf 𝒜).presheaf.obj (op U)) : Type u_1)) →
            (↑((Proj.structureSheaf 𝒜).presheaf.stalk x) : Type u_1))
        s) =
    (↑s :
        (x : ↥(unop (op U))) →
          (fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦ at x) (↑x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)))
      (Subtype.mk (p := fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦ x ∈ unop (op U)) x hx)

Tactic:
RingHom.ext_iff.1 (CommRingCat.hom_ext_iff.mp (germ_comp_stalkToFiberRingHom 𝒜 U x hx)) s

Premises used: Set.Mem, RingHom.ext_iff, AlgebraicGeometry.germ_comp_stalkToFiberRingHom, CommRingCat.hom_ext_iff, Iff.mp
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)
f : HomogeneousLocalization.NumDenSameDeg 𝒜 x.asHomogeneousIdeal.toIdeal.primeCompl
⊢ (↑f.den : A) ∉ x.asHomogeneousIdeal

Tactic:
f.den_mem

Premises used: Set.Mem, setOf, HomogeneousLocalization.NumDenSameDeg.den_mem, Not
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)
f : HomogeneousLocalization.NumDenSameDeg 𝒜 x.asHomogeneousIdeal.toIdeal.primeCompl
⊢ (↑f.den : A) ∉ x.asHomogeneousIdeal

Tactic:
exact f.den_mem

Premises used: HomogeneousLocalization.NumDenSameDeg.den_mem
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)
y : at x
f g : NumDenSameDeg 𝒜 x.asHomogeneousIdeal.toIdeal.primeCompl
e :
  NumDenSameDeg.embedding 𝒜 x.asHomogeneousIdeal.toIdeal.primeCompl f =
    NumDenSameDeg.embedding 𝒜 x.asHomogeneousIdeal.toIdeal.primeCompl g
⊢ ∃ (c : ↥x.asHomogeneousIdeal.toIdeal.primeCompl),
    (↑c : A) * ((↑g.den : A) * (↑f.num : A)) = (↑c : A) * ((↑f.den : A) * (↑g.num : A))

Tactic:
simp only [HomogeneousLocalization.NumDenSameDeg.embedding, Localization.mk_eq_mk',
      IsLocalization.mk'_eq_iff_eq,
      IsLocalization.eq_iff_exists x.asHomogeneousIdeal.toIdeal.primeCompl] at e

Premises used: Localization.mk_eq_mk', IsLocalization.mk'_eq_iff_eq, Ideal.primeCompl, HomogeneousIdeal.toIdeal, ProjectiveSpectrum.asHomogeneousIdeal, IsLocalization.eq_iff_exists, HomogeneousLocalization.NumDenSameDeg.embedding
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)
U : Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)
hxU : x ∈ U
s :
  ToType (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC := CommRingCat.carrier)
    (Functor.obj (Sheaf.presheaf (Proj.structureSheaf 𝒜) : Presheaf CommRingCat (ProjectiveSpectrum.top 𝒜)) (op U))
V : Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)
hxV :
  (↑(Subtype.mk (p := fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦ x ∈ unop (op U)) x hxU) :
      (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ∈
    V
i : V ⟶ unop (op U)
n : ℕ
a b : ↥(𝒜 n)
h : ∀ (x : ↥V), (↑b : A) ∉ (↑x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)).asHomogeneousIdeal
e :
  ∀ (x : ↥V),
    Eq (α := at (↑x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)))
      ((fun (x : ↥V) ↦
          (↑s :
              (x : ↥(unop (op U))) →
                (fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦ at x)
                  (↑x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)))
            ((i : (a : ↥V) → ↥(unop (op U))) x))
        x)
      (HomogeneousLocalization.mk { deg := n, num := a, den := b, den_mem := ⋯ })
⊢ ∀ (a_1 : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) (b_1 : a_1 ∈ V),
    (↑s : (x : ↥U) → at (↑x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)))
        (Subtype.mk (p := fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦ x ∈ U) a_1 ⋯) =
      HomogeneousLocalization.mk { deg := n, num := a, den := b, den_mem := ⋯ }

Tactic:
simp only [Subtype.forall, apply_mk] at e

Premises used: Subtype.forall, TopologicalSpace.Opens.apply_mk
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)
U : Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)
hxU : x ∈ U
s :
  ToType (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC := CommRingCat.carrier)
    (Functor.obj (Sheaf.presheaf (Proj.structureSheaf 𝒜) : Presheaf CommRingCat (ProjectiveSpectrum.top 𝒜)) (op U))
V : Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)
hxV :
  (↑(Subtype.mk (p := fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦ x ∈ unop (op U)) x hxU) :
      (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ∈
    V
i : V ⟶ unop (op U)
n : ℕ
a b : ↥(𝒜 n)
h : ∀ (x : ↥V), (↑b : A) ∉ (↑x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)).asHomogeneousIdeal
e :
  ∀ (a_1 : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) (b_1 : a_1 ∈ V),
    (↑s : (x : ↥U) → at (↑x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)))
        (Subtype.mk (p := fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦ x ∈ U) a_1 ⋯) =
      HomogeneousLocalization.mk { deg := n, num := a, den := b, den_mem := ⋯ }
t : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)
ht : t ∈ unop (op V)
⊢ HomogeneousLocalization.val.{0, u_1, u_2} (ι := ℕ) (σ := σ) (𝒜 := 𝒜)
      ((↑(sectionInBasicOpen 𝒜 x { deg := n, num := a, den := b, den_mem := ⋯ }) :
          (x_1 :
              ↥(unop (op (ProjectiveSpectrum.basicOpen 𝒜 (↑{ deg := n, num := a, den := b, den_mem := ⋯ }.den : A))))) →
            (fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦ at x)
              (↑x_1 : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)))
        ((Quiver.Hom.unop (Quiver.Hom.op (homOfLE ⋯)) :
            (a_1 : ↥(unop (op V))) →
              ↥(unop (op (ProjectiveSpectrum.basicOpen 𝒜 (↑{ deg := n, num := a, den := b, den_mem := ⋯ }.den : A)))))
          (Subtype.mk (p := fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦ x ∈ unop (op V)) t ht))) =
    HomogeneousLocalization.val
      ((↑s :
          (x : ↥(unop (op (unop (op U))))) →
            (fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦ at x) (↑x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)))
        ((i.op.unop : (a : ↥(unop (op V))) → ↥(unop (op (unop (op U)))))
          (Subtype.mk (p := fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦ x ∈ unop (op V)) t ht)))

Tactic:
simp [sectionInBasicOpen, HomogeneousLocalization.val_mk, Localization.mk_eq_mk', e t ht]

Premises used: Localization.mk_eq_mk', HomogeneousLocalization.val_mk, AlgebraicGeometry.sectionInBasicOpen
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)
z : at x
obtain :
  ∀ (z : HomogeneousLocalization.NumDenSameDeg 𝒜 x.asHomogeneousIdeal.toIdeal.primeCompl),
    Eq (α := (↑(CommRingCat.of (at x)) : Type u_1))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
              CommRingCat.carrier) (X := Presheaf.stalk (Sheaf.presheaf (Proj.structureSheaf 𝒜)) x)
              (stalkToFiberRingHom 𝒜 x) :
            (a : (↑((Proj.structureSheaf 𝒜).presheaf.stalk x) : Type u_1)) → (↑(CommRingCat.of (at x)) : Type u_1))
          (homogeneousLocalizationToStalk 𝒜 x (Quotient.mk'' z)) :
        (↑(CommRingCat.of (at x)) : Type u_1))
      (Quotient.mk'' z :
        _root_.Quotient (α := HomogeneousLocalization.NumDenSameDeg 𝒜 x.asHomogeneousIdeal.toIdeal.primeCompl)
          (Setoid.ker (HomogeneousLocalization.NumDenSameDeg.embedding 𝒜 x.asHomogeneousIdeal.toIdeal.primeCompl)))
⊢ (ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
          CommRingCat.carrier) (X := Presheaf.stalk (Sheaf.presheaf (Proj.structureSheaf 𝒜)) x)
          (stalkToFiberRingHom 𝒜 x) :
        (a : (↑((Proj.structureSheaf 𝒜).presheaf.stalk x) : Type u_1)) → (↑(CommRingCat.of (at x)) : Type u_1))
      (homogeneousLocalizationToStalk 𝒜 x z) =
    z

Tactic:
obtain ⟨z, rfl⟩ := Quotient.mk''_surjective z

Premises used: Quotient.mk''_surjective, rfl
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
U : Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)
x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)
hx : x ∈ U
s :
  (↑(Functor.obj
        (ObjectProperty.FullSubcategory.obj (P :=
            (CategoryTheory.Presheaf.IsSheaf (grothendieckTopology (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) :
              (P : (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ ⥤ CommRingCat) → Prop))
            (Proj.structureSheaf 𝒜 : TopCat.Sheaf CommRingCat (ProjectiveSpectrum.top 𝒜)) :
          (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ ⥤ CommRingCat)
        (op U)) :
    Type u_1)
⊢ (stalkIso' 𝒜 x : (a : (↑((Proj.structureSheaf 𝒜).presheaf.stalk x) : Type u_1)) → at x)
      (((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
              CommRingCat.carrier) (X :=
              Functor.obj (Sheaf.presheaf (Proj.structureSheaf 𝒜) : Presheaf CommRingCat (ProjectiveSpectrum.top 𝒜))
                (op U))
              (Y := Presheaf.stalk (Sheaf.presheaf (Proj.structureSheaf 𝒜)) x)
              (Presheaf.germ (Sheaf.presheaf (Proj.structureSheaf 𝒜)) U x hx :
                Functor.obj (Sheaf.presheaf (Proj.structureSheaf 𝒜) : Presheaf CommRingCat (ProjectiveSpectrum.top 𝒜))
                    (op U) ⟶
                  Presheaf.stalk (Sheaf.presheaf (Proj.structureSheaf 𝒜)) x) :
            (↑(Functor.obj (Sheaf.presheaf (Proj.structureSheaf 𝒜) : Presheaf CommRingCat (ProjectiveSpectrum.top 𝒜))
                    (op U)) :
                Type u_1) →+*
              (↑(Presheaf.stalk (Sheaf.presheaf (Proj.structureSheaf 𝒜)) x) : Type u_1)) :
          (a : (↑((Proj.structureSheaf 𝒜).presheaf.obj (op U)) : Type u_1)) →
            (↑((Proj.structureSheaf 𝒜).presheaf.stalk x) : Type u_1))
        s) =
    (↑s :
        (x : ↥(unop (op U))) →
          (fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦ at x) (↑x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)))
      (Subtype.mk (p := fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦ x ∈ unop (op U)) x hx)

Tactic:
stalkToFiberRingHom_germ 𝒜 U x hx s

Premises used: HomogeneousLocalization, Quotient, AlgebraicGeometry.stalkToFiberRingHom_germ
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)
f : HomogeneousLocalization.NumDenSameDeg 𝒜 x.asHomogeneousIdeal.toIdeal.primeCompl
⊢ Eq (α := (↑(Presheaf.stalk (Sheaf.presheaf (Proj.structureSheaf 𝒜)) x) : Type u_1))
    ((RingEquiv.symm (stalkIso' 𝒜 x) : (a : at x) → (↑((Proj.structureSheaf 𝒜).presheaf.stalk x) : Type u_1))
        (HomogeneousLocalization.mk f) :
      (↑(Presheaf.stalk (Sheaf.presheaf (Proj.structureSheaf 𝒜)) x) : Type u_1))
    (((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
              CommRingCat.carrier) (X :=
              Functor.obj (C := (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ)
                (Sheaf.presheaf (Proj.structureSheaf 𝒜) : Presheaf CommRingCat (ProjectiveSpectrum.top 𝒜))
                (op (ProjectiveSpectrum.basicOpen 𝒜 (↑f.den : A)) : (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ))
              (Y := Presheaf.stalk (Sheaf.presheaf (Proj.structureSheaf 𝒜)) x)
              (Presheaf.germ (Sheaf.presheaf (Proj.structureSheaf 𝒜)) (ProjectiveSpectrum.basicOpen 𝒜 (↑f.den : A)) x
                  ⋯ :
                Functor.obj (C := (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ)
                    (Sheaf.presheaf (Proj.structureSheaf 𝒜) : Presheaf CommRingCat (ProjectiveSpectrum.top 𝒜))
                    (op (ProjectiveSpectrum.basicOpen 𝒜 (↑f.den : A)) :
                      (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ) ⟶
                  Presheaf.stalk (Sheaf.presheaf (Proj.structureSheaf 𝒜)) x) :
            (↑(Functor.obj (C := (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ)
                    (Sheaf.presheaf (Proj.structureSheaf 𝒜) : Presheaf CommRingCat (ProjectiveSpectrum.top 𝒜))
                    (op (ProjectiveSpectrum.basicOpen 𝒜 (↑f.den : A)) :
                      (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ)) :
                Type u_1) →+*
              (↑(Presheaf.stalk (Sheaf.presheaf (Proj.structureSheaf 𝒜)) x) : Type u_1)) :
          (a :
              (↑((Proj.structureSheaf 𝒜).presheaf.obj (op (ProjectiveSpectrum.basicOpen 𝒜 (↑f.den : A)))) : Type u_1)) →
            (↑((Proj.structureSheaf 𝒜).presheaf.stalk x) : Type u_1))
        (sectionInBasicOpen 𝒜 x f) :
      (↑(Presheaf.stalk (Sheaf.presheaf (Proj.structureSheaf 𝒜)) x) : Type u_1))

Tactic:
rfl

Premises used: Quotient.liftOn', AlgebraicGeometry.homogeneousLocalizationToStalk, rfl
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
x : ProjectiveSpectrum 𝒜
⊢ x.asHomogeneousIdeal.toIdeal.IsPrime

Tactic:
x.isPrime

Premises used: ProjectiveSpectrum.isPrime
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
x : ProjectiveSpectrum 𝒜
s : Set A
⊢ Membership.mem (γ := Set (ProjectiveSpectrum 𝒜)) (zeroLocus 𝒜 s) x ↔ s ⊆ (↑x.asHomogeneousIdeal : Set A)

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, ProjectiveSpectrum.zeroLocus
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
s : Set A
h :
  ∀ (x : ProjectiveSpectrum 𝒜),
    Membership.mem (γ := Set (ProjectiveSpectrum 𝒜)) (zeroLocus 𝒜 (↑(Ideal.span s) : Set A)) x ↔
      Membership.mem (γ := Set (ProjectiveSpectrum 𝒜)) (zeroLocus 𝒜 s) x
⊢ Eq (α := Set (ProjectiveSpectrum 𝒜)) (zeroLocus 𝒜 (↑(Ideal.span s) : Set A)) (zeroLocus 𝒜 s)

Tactic:
ext x
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
s : Set A
x : ProjectiveSpectrum 𝒜
⊢ Membership.mem (γ := Set (ProjectiveSpectrum 𝒜)) (zeroLocus 𝒜 (↑(Ideal.span s) : Set A)) x ↔
    Membership.mem (γ := Set (ProjectiveSpectrum 𝒜)) (zeroLocus 𝒜 s) x

Tactic:
(Submodule.gi _ _).gc s x.asHomogeneousIdeal.toIdeal

Premises used: Submodule.gi, Set.Mem, setOf, Set.Subset, HomogeneousIdeal.toIdeal, ProjectiveSpectrum.zeroLocus, ProjectiveSpectrum.asHomogeneousIdeal, GaloisInsertion.gc
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
s : Set A
x : ProjectiveSpectrum 𝒜
⊢ Membership.mem (γ := Set (ProjectiveSpectrum 𝒜)) (zeroLocus 𝒜 (↑(Ideal.span s) : Set A)) x ↔
    Membership.mem (γ := Set (ProjectiveSpectrum 𝒜)) (zeroLocus 𝒜 s) x

Tactic:
exact (Submodule.gi _ _).gc s x.asHomogeneousIdeal.toIdeal

Premises used: Submodule.gi, HomogeneousIdeal.toIdeal, ProjectiveSpectrum.asHomogeneousIdeal, GaloisInsertion.gc
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
t : Set (ProjectiveSpectrum 𝒜)
h :
  ∀ (f : A),
    f ∈ (↑(vanishingIdeal t) : Set A) ↔ Membership.mem (γ := Set A) {f : A | ∀ x ∈ t, f ∈ x.asHomogeneousIdeal} f
⊢ (↑(vanishingIdeal t) : Set A) = {f : A | ∀ x ∈ t, f ∈ x.asHomogeneousIdeal}

Tactic:
ext f
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
t : Set (ProjectiveSpectrum 𝒜)
f : A
h :
  (∀ (i : ProjectiveSpectrum 𝒜),
      Membership.mem (γ := Submodule A A)
        (HomogeneousIdeal.toIdeal.{0, u_2, u_1} (ι := ℕ) (σ := σ) (𝒜 := 𝒜) (⨅ (_ : i ∈ t), i.asHomogeneousIdeal)) f) ↔
    Membership.mem (γ := Set A) {f : A | ∀ x ∈ t, f ∈ x.asHomogeneousIdeal} f
⊢ f ∈ (↑(vanishingIdeal t) : Set A) ↔ Membership.mem (γ := Set A) {f : A | ∀ x ∈ t, f ∈ x.asHomogeneousIdeal} f

Tactic:
rw [vanishingIdeal, SetLike.mem_coe, ← HomogeneousIdeal.mem_iff, HomogeneousIdeal.toIdeal_iInf,
    Submodule.mem_iInf]

Premises used: Submodule.mem_iInf, HomogeneousIdeal.toIdeal_iInf, ProjectiveSpectrum.vanishingIdeal, SetLike.mem_coe, HomogeneousIdeal.mem_iff
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
t : Set (ProjectiveSpectrum 𝒜)
f : A
⊢ (∀ (i : ProjectiveSpectrum 𝒜),
      Membership.mem (γ := Submodule A A)
        (HomogeneousIdeal.toIdeal.{0, u_2, u_1} (ι := ℕ) (σ := σ) (𝒜 := 𝒜) (⨅ (_ : i ∈ t), i.asHomogeneousIdeal)) f) ↔
    Membership.mem (γ := Set A) {f : A | ∀ x ∈ t, f ∈ x.asHomogeneousIdeal} f

Tactic:
forall_congr' fun x => ?_

Premises used: Set.Mem, setOf, forall_congr'
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
t : Set (ProjectiveSpectrum 𝒜)
f : A
h :
  ∀ (x : ProjectiveSpectrum 𝒜),
    Membership.mem (γ := Submodule A A)
        (HomogeneousIdeal.toIdeal.{0, u_2, u_1} (ι := ℕ) (σ := σ) (𝒜 := 𝒜) (⨅ (_ : x ∈ t), x.asHomogeneousIdeal)) f ↔
      x ∈ t → f ∈ x.asHomogeneousIdeal
⊢ (∀ (i : ProjectiveSpectrum 𝒜),
      Membership.mem (γ := Submodule A A)
        (HomogeneousIdeal.toIdeal.{0, u_2, u_1} (ι := ℕ) (σ := σ) (𝒜 := 𝒜) (⨅ (_ : i ∈ t), i.asHomogeneousIdeal)) f) ↔
    Membership.mem (γ := Set A) {f : A | ∀ x ∈ t, f ∈ x.asHomogeneousIdeal} f

Tactic:
refine forall_congr' fun x => ?_

Premises used: forall_congr'
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
t : Set (ProjectiveSpectrum 𝒜)
f : A
x : ProjectiveSpectrum 𝒜
h :
  Membership.mem (γ := Submodule A A) (⨅ (_ : x ∈ t), x.asHomogeneousIdeal.toIdeal) f ↔ x ∈ t → f ∈ x.asHomogeneousIdeal
h₁ : (∀ (i : x ∈ t), f ∈ x.asHomogeneousIdeal.toIdeal) ↔ x ∈ t → f ∈ x.asHomogeneousIdeal
h₂ h₃ : (∀ (i : x ∈ t), f ∈ x.asHomogeneousIdeal) ↔ x ∈ t → f ∈ x.asHomogeneousIdeal
⊢ Membership.mem (γ := Submodule A A)
      (HomogeneousIdeal.toIdeal.{0, u_2, u_1} (ι := ℕ) (σ := σ) (𝒜 := 𝒜) (⨅ (_ : x ∈ t), x.asHomogeneousIdeal)) f ↔
    x ∈ t → f ∈ x.asHomogeneousIdeal

Tactic:
rw [HomogeneousIdeal.toIdeal_iInf, Submodule.mem_iInf, HomogeneousIdeal.mem_iff]

Premises used: Submodule.mem_iInf, HomogeneousIdeal.toIdeal_iInf, HomogeneousIdeal.mem_iff
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
t : Set (ProjectiveSpectrum 𝒜)
f : A
rw : f ∈ (↑(vanishingIdeal t) : Set A) ↔ ∀ x ∈ t, f ∈ x.asHomogeneousIdeal
rw₁ : Membership.mem (γ := Set A) {f : A | ∀ x ∈ t, f ∈ x.asHomogeneousIdeal} f ↔ ∀ x ∈ t, f ∈ x.asHomogeneousIdeal
rw₂ rw₃ : (∀ x ∈ t, f ∈ x.asHomogeneousIdeal) ↔ ∀ x ∈ t, f ∈ x.asHomogeneousIdeal
⊢ f ∈ vanishingIdeal t ↔ ∀ x ∈ t, f ∈ x.asHomogeneousIdeal

Tactic:
rw [← SetLike.mem_coe, coe_vanishingIdeal, Set.mem_setOf_eq]

Premises used: Set.mem_setOf_eq, SetLike.mem_coe, ProjectiveSpectrum.coe_vanishingIdeal
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
x : ProjectiveSpectrum 𝒜
⊢ vanishingIdeal {x} = x.asHomogeneousIdeal

Tactic:
simp [vanishingIdeal]

Premises used: ProjectiveSpectrum.vanishingIdeal
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
t : Set (ProjectiveSpectrum 𝒜)
I : Ideal A
⊢ t ⊆ zeroLocus 𝒜 (↑I : Set A) ↔ I ≤ (vanishingIdeal t).toIdeal

Tactic:
⟨fun h _ k => (mem_vanishingIdeal _ _).mpr fun _ j => (mem_zeroLocus _ _ _).mpr (h j) k, fun h =>
    fun x j =>
    (mem_zeroLocus _ _ _).mpr (le_trans h fun _ h => ((mem_vanishingIdeal _ _).mp h) x j)⟩

Premises used: Iff.mpr, ProjectiveSpectrum.mem_vanishingIdeal, ProjectiveSpectrum.mem_zeroLocus, SetLike.coe, Iff.intro, Iff.mp, le_trans
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubmonoidClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
⊢ GaloisConnection (fun (I : Ideal A) ↦ zeroLocus 𝒜 (↑I : Set A)) fun (t : (Set (ProjectiveSpectrum 𝒜))ᵒᵈ) ↦
    (vanishingIdeal t).toIdeal

Tactic:
fun I t => subset_zeroLocus_iff_le_vanishingIdeal t I

Premises used: Set.Mem, ProjectiveSpectrum.subset_zeroLocus_iff_le_vanishingIdeal, GaloisConnection