awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
a : A
i : ℕ
⊢ f ^ i ∈ 𝒜 (i * m)

Tactic:
exact SetLike.pow_mem_graded _ f_deg

Premises used: SetLike.pow_mem_graded
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
rw :
  ∀ (s : Set ↥(pbo f)),
    Membership.mem (γ := Set (Set ↥(pbo f)))
        (Set.preimage
            (Subtype.val (p := fun (x : ProjectiveSpectrum 𝒜) ↦
              Membership.mem (γ := Opens (ProjectiveSpectrum 𝒜)) (pbo f) x)) ''
          Set.range fun (r : A) ↦ (↑(pbo r) : Set (ProjectiveSpectrum 𝒜)))
        s →
      IsOpen (X := PrimeSpectrum (↑(CommRingCat.of (A⁰_ f)) : Type u_1)) (FromSpec.toFun f_deg hm ⁻¹' s)
⊢ Continuous (X := PrimeSpectrum (↑(CommRingCat.of (A⁰_ f)) : Type u_1)) (FromSpec.toFun f_deg hm)

Tactic:
rw [isTopologicalBasis_subtype (ProjectiveSpectrum.isTopologicalBasis_basic_opens 𝒜)
        (· ∈ pbo f) |>.continuous_iff]

Premises used: isTopologicalBasis_subtype, ProjectiveSpectrum.basicOpen, Membership.mem, ProjectiveSpectrum.isTopologicalBasis_basic_opens, TopologicalSpace.IsTopologicalBasis.continuous_iff
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
a : A
⊢ Eq (α := Set ↥(pbo f))
    (Subtype.val (p := fun (x : ProjectiveSpectrum 𝒜) ↦
        Membership.mem (γ := Opens (ProjectiveSpectrum 𝒜)) (pbo f) x) ⁻¹'
      (↑(pbo a) : Set (ProjectiveSpectrum 𝒜)))
    (⋃ (i : ℕ),
      Subtype.val (p := fun (x : ProjectiveSpectrum 𝒜) ↦
          Membership.mem (γ := Opens (ProjectiveSpectrum 𝒜)) (pbo f) x) ⁻¹'
        (↑(pbo (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ℕ), ↥(𝒜 i)) a : ⨁ (i : ℕ), ↥(𝒜 i)) : (a : ℕ) → ↥(𝒜 a)) i) : A)) :
          Set (ProjectiveSpectrum 𝒜)))

Tactic:
simp [ProjectiveSpectrum.basicOpen_eq_union_of_projection 𝒜 a]

Premises used: ProjectiveSpectrum.basicOpen_eq_union_of_projection
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
a : A
⊢ Eq (α := Set ↥(pbo f))
    (Subtype.val (p := fun (x : ProjectiveSpectrum 𝒜) ↦
        Membership.mem (γ := Opens (ProjectiveSpectrum 𝒜)) (pbo f) x) ⁻¹'
      (↑(pbo a) : Set (ProjectiveSpectrum 𝒜)))
    (⋃ (i : ℕ),
      Subtype.val (p := fun (x : ProjectiveSpectrum 𝒜) ↦
          Membership.mem (γ := Opens (ProjectiveSpectrum 𝒜)) (pbo f) x) ⁻¹'
        (↑(pbo (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ℕ), ↥(𝒜 i)) a : ⨁ (i : ℕ), ↥(𝒜 i)) : (a : ℕ) → ↥(𝒜 a)) i) : A)) :
          Set (ProjectiveSpectrum 𝒜)))

Tactic:
have h₁ : Subtype.val (p := (· ∈ pbo f)) ⁻¹' (pbo a) =
          ⋃ i : ℕ, Subtype.val (p := (· ∈ pbo f)) ⁻¹' (pbo (decompose 𝒜 a i)) := by
        simp [ProjectiveSpectrum.basicOpen_eq_union_of_projection 𝒜 a]
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
a : A
h₁ :
  Eq (α := Set ↥(pbo f))
    (Subtype.val (p := fun (x : ProjectiveSpectrum 𝒜) ↦
        Membership.mem (γ := Opens (ProjectiveSpectrum 𝒜)) (pbo f) x) ⁻¹'
      (↑(pbo a) : Set (ProjectiveSpectrum 𝒜)))
    (⋃ (i : ℕ),
      Subtype.val (p := fun (x : ProjectiveSpectrum 𝒜) ↦
          Membership.mem (γ := Opens (ProjectiveSpectrum 𝒜)) (pbo f) x) ⁻¹'
        (↑(pbo (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ℕ), ↥(𝒜 i)) a : ⨁ (i : ℕ), ↥(𝒜 i)) : (a : ℕ) → ↥(𝒜 a)) i) : A)) :
          Set (ProjectiveSpectrum 𝒜)))
e : (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1) ≃
  (↑(↑(Proj.restrict (U := Functor.obj (C := Opens (↑Proj.T : Type u_1)) (Opens.toTopCat Proj.T) (pbo f))
              ⋯).toPresheafedSpace :
        TopCat) :
    Type u_1) :=
  { toFun := FromSpec.toFun f_deg hm, invFun := ToSpec.toFun f, left_inv := ⋯, right_inv := ⋯ }
change :
  IsOpen (X := (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1))
    (Set.preimage (β :=
      (↑(↑(Proj.restrict (U := Functor.obj (C := Opens (↑Proj.T : Type u_1)) (Opens.toTopCat Proj.T) (pbo f))
                  ⋯).toPresheafedSpace :
            TopCat) :
        Type u_1))
      (⇑e :
        (a : (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1)) →
          (↑(↑(Proj.restrict ⋯).toPresheafedSpace : TopCat) : Type u_1))
      (Subtype.val (p := fun (x : ProjectiveSpectrum 𝒜) ↦
          Membership.mem (γ := Opens (ProjectiveSpectrum 𝒜)) (pbo f) x) ⁻¹'
        (fun (r : A) ↦ (↑(pbo r) : Set (ProjectiveSpectrum 𝒜))) a))
⊢ IsOpen (X := PrimeSpectrum (↑(CommRingCat.of (A⁰_ f)) : Type u_1))
    (FromSpec.toFun f_deg hm ⁻¹'
      Subtype.val (p := fun (x : ProjectiveSpectrum 𝒜) ↦
          Membership.mem (γ := Opens (ProjectiveSpectrum 𝒜)) (pbo f) x) ⁻¹'
        (fun (r : A) ↦ (↑(pbo r) : Set (ProjectiveSpectrum 𝒜))) a)

Tactic:
change IsOpen <| e ⁻¹' _

Premises used: IsOpen
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
a : A
h₁ :
  Eq (α := Set ↥(pbo f))
    (Subtype.val (p := fun (x : ProjectiveSpectrum 𝒜) ↦
        Membership.mem (γ := Opens (ProjectiveSpectrum 𝒜)) (pbo f) x) ⁻¹'
      (↑(pbo a) : Set (ProjectiveSpectrum 𝒜)))
    (⋃ (i : ℕ),
      Subtype.val (p := fun (x : ProjectiveSpectrum 𝒜) ↦
          Membership.mem (γ := Opens (ProjectiveSpectrum 𝒜)) (pbo f) x) ⁻¹'
        (↑(pbo (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ℕ), ↥(𝒜 i)) a : ⨁ (i : ℕ), ↥(𝒜 i)) : (a : ℕ) → ↥(𝒜 a)) i) : A)) :
          Set (ProjectiveSpectrum 𝒜)))
e : (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1) ≃
  (↑(↑(Proj.restrict (U := Functor.obj (C := Opens (↑Proj.T : Type u_1)) (Opens.toTopCat Proj.T) (pbo f))
              ⋯).toPresheafedSpace :
        TopCat) :
    Type u_1) :=
  { toFun := FromSpec.toFun f_deg hm, invFun := ToSpec.toFun f, left_inv := ⋯, right_inv := ⋯ }
rw :
  IsOpen.{u_1} (X := (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1))
    (⋃ (i : ℕ),
      Set.image (α :=
        (↑(↑(Proj.restrict (U := Functor.obj (C := Opens (↑Proj.T : Type u_1)) (Opens.toTopCat Proj.T) (pbo f))
                    ⋯).toPresheafedSpace :
              TopCat) :
          Type u_1))
        (⇑e.symm :
          (a : (↑(↑(Proj.restrict ⋯).toPresheafedSpace : TopCat) : Type u_1)) →
            (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1))
        (Subtype.val (p := fun (x : ProjectiveSpectrum 𝒜) ↦
            Membership.mem (γ := Opens (ProjectiveSpectrum 𝒜)) (pbo f) x) ⁻¹'
          (↑(pbo (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ℕ), ↥(𝒜 i)) a : ⨁ (i : ℕ), ↥(𝒜 i)) : (a : ℕ) → ↥(𝒜 a)) i) : A)) :
            Set (ProjectiveSpectrum 𝒜))))
⊢ IsOpen (X := (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1))
    (Set.preimage (β :=
      (↑(↑(Proj.restrict (U := Functor.obj (C := Opens (↑Proj.T : Type u_1)) (Opens.toTopCat Proj.T) (pbo f))
                  ⋯).toPresheafedSpace :
            TopCat) :
        Type u_1))
      (⇑e :
        (a : (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1)) →
          (↑(↑(Proj.restrict ⋯).toPresheafedSpace : TopCat) : Type u_1))
      (Subtype.val (p := fun (x : ProjectiveSpectrum 𝒜) ↦
          Membership.mem (γ := Opens (ProjectiveSpectrum 𝒜)) (pbo f) x) ⁻¹'
        (fun (r : A) ↦ (↑(pbo r) : Set (ProjectiveSpectrum 𝒜))) a))

Tactic:
rw [← Equiv.image_symm_eq_preimage, h₁, Set.image_iUnion]

Premises used: Set.image_iUnion, Equiv.image_symm_eq_preimage
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
a : A
h₁ :
  Eq (α := Set ↥(pbo f))
    (Subtype.val (p := fun (x : ProjectiveSpectrum 𝒜) ↦
        Membership.mem (γ := Opens (ProjectiveSpectrum 𝒜)) (pbo f) x) ⁻¹'
      (↑(pbo a) : Set (ProjectiveSpectrum 𝒜)))
    (⋃ (i : ℕ),
      Subtype.val (p := fun (x : ProjectiveSpectrum 𝒜) ↦
          Membership.mem (γ := Opens (ProjectiveSpectrum 𝒜)) (pbo f) x) ⁻¹'
        (↑(pbo (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ℕ), ↥(𝒜 i)) a : ⨁ (i : ℕ), ↥(𝒜 i)) : (a : ℕ) → ↥(𝒜 a)) i) : A)) :
          Set (ProjectiveSpectrum 𝒜)))
e : (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1) ≃
  (↑(↑(Proj.restrict (U := Functor.obj (C := Opens (↑Proj.T : Type u_1)) (Opens.toTopCat Proj.T) (pbo f))
              ⋯).toPresheafedSpace :
        TopCat) :
    Type u_1) :=
  { toFun := FromSpec.toFun f_deg hm, invFun := ToSpec.toFun f, left_inv := ⋯, right_inv := ⋯ }
⊢ IsOpen.{u_1} (X := (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1))
    (⋃ (i : ℕ),
      Set.image (α :=
        (↑(↑(Proj.restrict (U := Functor.obj (C := Opens (↑Proj.T : Type u_1)) (Opens.toTopCat Proj.T) (pbo f))
                    ⋯).toPresheafedSpace :
              TopCat) :
          Type u_1))
        (⇑e.symm :
          (a : (↑(↑(Proj.restrict ⋯).toPresheafedSpace : TopCat) : Type u_1)) →
            (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1))
        (Subtype.val (p := fun (x : ProjectiveSpectrum 𝒜) ↦
            Membership.mem (γ := Opens (ProjectiveSpectrum 𝒜)) (pbo f) x) ⁻¹'
          (↑(pbo (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ℕ), ↥(𝒜 i)) a : ⨁ (i : ℕ), ↥(𝒜 i)) : (a : ℕ) → ↥(𝒜 a)) i) : A)) :
            Set (ProjectiveSpectrum 𝒜))))

Tactic:
isOpen_iUnion fun i ↦ toSpec.image_basicOpen_eq_basicOpen f_deg hm a i ▸
        PrimeSpectrum.isOpen_basicOpen

Premises used: Eq.rec, PrimeSpectrum.isOpen_basicOpen, isOpen_iUnion, Eq.symm, AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec.image_basicOpen_eq_basicOpen
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
a : A
h₁ :
  Eq (α := Set ↥(pbo f))
    (Subtype.val (p := fun (x : ProjectiveSpectrum 𝒜) ↦
        Membership.mem (γ := Opens (ProjectiveSpectrum 𝒜)) (pbo f) x) ⁻¹'
      (↑(pbo a) : Set (ProjectiveSpectrum 𝒜)))
    (⋃ (i : ℕ),
      Subtype.val (p := fun (x : ProjectiveSpectrum 𝒜) ↦
          Membership.mem (γ := Opens (ProjectiveSpectrum 𝒜)) (pbo f) x) ⁻¹'
        (↑(pbo (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ℕ), ↥(𝒜 i)) a : ⨁ (i : ℕ), ↥(𝒜 i)) : (a : ℕ) → ↥(𝒜 a)) i) : A)) :
          Set (ProjectiveSpectrum 𝒜)))
e : (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1) ≃
  (↑(↑(Proj.restrict (U := Functor.obj (C := Opens (↑Proj.T : Type u_1)) (Opens.toTopCat Proj.T) (pbo f))
              ⋯).toPresheafedSpace :
        TopCat) :
    Type u_1) :=
  { toFun := FromSpec.toFun f_deg hm, invFun := ToSpec.toFun f, left_inv := ⋯, right_inv := ⋯ }
⊢ IsOpen.{u_1} (X := (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1))
    (⋃ (i : ℕ),
      Set.image (α :=
        (↑(↑(Proj.restrict (U := Functor.obj (C := Opens (↑Proj.T : Type u_1)) (Opens.toTopCat Proj.T) (pbo f))
                    ⋯).toPresheafedSpace :
              TopCat) :
          Type u_1))
        (⇑e.symm :
          (a : (↑(↑(Proj.restrict ⋯).toPresheafedSpace : TopCat) : Type u_1)) →
            (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1))
        (Subtype.val (p := fun (x : ProjectiveSpectrum 𝒜) ↦
            Membership.mem (γ := Opens (ProjectiveSpectrum 𝒜)) (pbo f) x) ⁻¹'
          (↑(pbo (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ℕ), ↥(𝒜 i)) a : ⨁ (i : ℕ), ↥(𝒜 i)) : (a : ℕ) → ↥(𝒜 a)) i) : A)) :
            Set (ProjectiveSpectrum 𝒜))))

Tactic:
exact isOpen_iUnion fun i ↦ toSpec.image_basicOpen_eq_basicOpen f_deg hm a i ▸
        PrimeSpectrum.isOpen_basicOpen

Premises used: isOpen_iUnion
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
f : A
x : ↥(unop (op (pbo f)))
s : HomogeneousLocalization.NumDenSameDeg 𝒜 (Submonoid.powers f)
n : ℕ
hn : f ^ n = (↑s.den : A)
⊢ ∃ (V : Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) (_ : (↑x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ∈ V) (i :
    V ⟶ unop (op (pbo f))),
    PrelocalPredicate.pred (X := ProjectiveSpectrum.top 𝒜) (T := fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦
      HomogeneousLocalization.AtPrime 𝒜 x.asHomogeneousIdeal.toIdeal)
      (isFractionPrelocal 𝒜 :
        PrelocalPredicate (X := ProjectiveSpectrum.top 𝒜) fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦
          HomogeneousLocalization.AtPrime 𝒜 x.asHomogeneousIdeal.toIdeal)
      (U := V) fun (x : ↥V) ↦
      ((fun (x : ↥(unop (op (pbo f)))) ↦
            ((HomogeneousLocalization.mapId 𝒜 ⋯ :
                  (a : HomogeneousLocalization 𝒜 (Submonoid.powers f)) →
                    HomogeneousLocalization 𝒜
                      (↑x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)).asHomogeneousIdeal.toIdeal.primeCompl)
                (HomogeneousLocalization.mk s) :
              HomogeneousLocalization 𝒜
                (↑x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)).asHomogeneousIdeal.toIdeal.primeCompl))
          ((i : (a : ↥V) → ↥(unop (op (pbo f)))) x) :
        HomogeneousLocalization 𝒜
          (Ideal.primeCompl
            (HomogeneousIdeal.toIdeal.{0, u_2, u_1} (σ := σ) (𝒜 := 𝒜)
              (ProjectiveSpectrum.asHomogeneousIdeal
                (↑((i : (a : ↥V) → ↥(unop (op (pbo f)))) x) : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))))))

Tactic:
⟨_, x.2, 𝟙 _, s.1, s.2, s.3,
          fun x hsx ↦ x.2 (Ideal.IsPrime.mem_of_pow_mem inferInstance n (hn ▸ hsx)), fun _ ↦ rfl⟩

Premises used: HomogeneousLocalization.NumDenSameDeg.num, Ideal.IsPrime.mem_of_pow_mem, CategoryTheory.CategoryStruct.id, Eq.rec, inferInstance, Exists.intro, HomogeneousLocalization.NumDenSameDeg.den, Eq.symm, HomogeneousLocalization.NumDenSameDeg.deg, rfl, Subtype.property
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
f : A
x : ↥(unop (op (pbo f)))
s : HomogeneousLocalization.NumDenSameDeg 𝒜 (Submonoid.powers f)
n : ℕ
hn : f ^ n = (↑s.den : A)
⊢ ∃ (V : Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) (_ : (↑x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ∈ V) (i :
    V ⟶ unop (op (pbo f))),
    PrelocalPredicate.pred (X := ProjectiveSpectrum.top 𝒜) (T := fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦
      HomogeneousLocalization.AtPrime 𝒜 x.asHomogeneousIdeal.toIdeal)
      (isFractionPrelocal 𝒜 :
        PrelocalPredicate (X := ProjectiveSpectrum.top 𝒜) fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦
          HomogeneousLocalization.AtPrime 𝒜 x.asHomogeneousIdeal.toIdeal)
      (U := V) fun (x : ↥V) ↦
      ((fun (x : ↥(unop (op (pbo f)))) ↦
            ((HomogeneousLocalization.mapId 𝒜 ⋯ :
                  (a : HomogeneousLocalization 𝒜 (Submonoid.powers f)) →
                    HomogeneousLocalization 𝒜
                      (↑x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)).asHomogeneousIdeal.toIdeal.primeCompl)
                (HomogeneousLocalization.mk s) :
              HomogeneousLocalization 𝒜
                (↑x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)).asHomogeneousIdeal.toIdeal.primeCompl))
          ((i : (a : ↥V) → ↥(unop (op (pbo f)))) x) :
        HomogeneousLocalization 𝒜
          (Ideal.primeCompl
            (HomogeneousIdeal.toIdeal.{0, u_2, u_1} (σ := σ) (𝒜 := 𝒜)
              (ProjectiveSpectrum.asHomogeneousIdeal
                (↑((i : (a : ↥V) → ↥(unop (op (pbo f)))) x) : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))))))

Tactic:
exact ⟨_, x.2, 𝟙 _, s.1, s.2, s.3,
          fun x hsx ↦ x.2 (Ideal.IsPrime.mem_of_pow_mem inferInstance n (hn ▸ hsx)), fun _ ↦ rfl⟩
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
f : A
x : ↥(unop (op (pbo f)))
⊢ Eq (α := Localization (M := A) (↑x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)).asHomogeneousIdeal.toIdeal.primeCompl)
    (HomogeneousLocalization.val.{0, u_1, u_2} (ι := ℕ) (σ := σ) (𝒜 := 𝒜)
      ((↑(Subtype.mk (p :=
              fun
                (f_1 :
                  (x : ↥(unop (op (pbo f)))) →
                    (fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦
                        HomogeneousLocalization.AtPrime 𝒜 x.asHomogeneousIdeal.toIdeal)
                      (↑x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))) ↦
              PrelocalPredicate.pred (X := ProjectiveSpectrum.top 𝒜) (T :=
                fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦
                HomogeneousLocalization.AtPrime 𝒜 x.asHomogeneousIdeal.toIdeal)
                (LocalPredicate.toPrelocalPredicate (T := fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦
                    HomogeneousLocalization.AtPrime 𝒜 x.asHomogeneousIdeal.toIdeal) (isLocallyFraction 𝒜) :
                  PrelocalPredicate (X := ProjectiveSpectrum.top 𝒜) fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦
                    HomogeneousLocalization.AtPrime 𝒜 x.asHomogeneousIdeal.toIdeal)
                f_1)
              (fun (x : ↥(unop (op (pbo f)))) ↦
                (HomogeneousLocalization.mapId 𝒜 ⋯ :
                    (a : HomogeneousLocalization 𝒜 (Submonoid.powers f)) →
                      HomogeneousLocalization 𝒜
                        (↑x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)).asHomogeneousIdeal.toIdeal.primeCompl)
                  1)
              ⋯) :
          (x : ↥(unop (op (pbo f)))) →
            (fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦
                HomogeneousLocalization.AtPrime 𝒜 x.asHomogeneousIdeal.toIdeal)
              (↑x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)))
        x))
    (HomogeneousLocalization.val.{0, u_1, u_2} (ι := ℕ) (σ := σ) (𝒜 := 𝒜)
      ((↑1 :
          (x : ↥(unop (op (pbo f)))) →
            (fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦
                HomogeneousLocalization.AtPrime 𝒜 x.asHomogeneousIdeal.toIdeal)
              (↑x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)))
        x))

Tactic:
simp only [map_one, HomogeneousLocalization.val_one, Proj.one_apply]

Premises used: AlgebraicGeometry.Proj.one_apply, HomogeneousLocalization.val_one, map_one
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
f : A
x : ↥(unop (op (pbo f)))
⊢ Eq (α := Localization (M := A) (↑x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)).asHomogeneousIdeal.toIdeal.primeCompl)
    (HomogeneousLocalization.val.{0, u_1, u_2} (ι := ℕ) (σ := σ) (𝒜 := 𝒜)
      ((↑(Subtype.mk (p :=
              fun
                (f_1 :
                  (x : ↥(unop (op (pbo f)))) →
                    (fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦
                        HomogeneousLocalization.AtPrime 𝒜 x.asHomogeneousIdeal.toIdeal)
                      (↑x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))) ↦
              PrelocalPredicate.pred (X := ProjectiveSpectrum.top 𝒜) (T :=
                fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦
                HomogeneousLocalization.AtPrime 𝒜 x.asHomogeneousIdeal.toIdeal)
                (LocalPredicate.toPrelocalPredicate (T := fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦
                    HomogeneousLocalization.AtPrime 𝒜 x.asHomogeneousIdeal.toIdeal) (isLocallyFraction 𝒜) :
                  PrelocalPredicate (X := ProjectiveSpectrum.top 𝒜) fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦
                    HomogeneousLocalization.AtPrime 𝒜 x.asHomogeneousIdeal.toIdeal)
                f_1)
              (fun (x : ↥(unop (op (pbo f)))) ↦
                (HomogeneousLocalization.mapId 𝒜 ⋯ :
                    (a : HomogeneousLocalization 𝒜 (Submonoid.powers f)) →
                      HomogeneousLocalization 𝒜
                        (↑x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)).asHomogeneousIdeal.toIdeal.primeCompl)
                  0)
              ⋯) :
          (x : ↥(unop (op (pbo f)))) →
            (fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦
                HomogeneousLocalization.AtPrime 𝒜 x.asHomogeneousIdeal.toIdeal)
              (↑x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)))
        x))
    (HomogeneousLocalization.val.{0, u_1, u_2} (ι := ℕ) (σ := σ) (𝒜 := 𝒜)
      ((↑0 :
          (x : ↥(unop (op (pbo f)))) →
            (fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦
                HomogeneousLocalization.AtPrime 𝒜 x.asHomogeneousIdeal.toIdeal)
              (↑x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)))
        x))

Tactic:
simp only [map_zero, HomogeneousLocalization.val_zero, Proj.zero_apply]

Premises used: HomogeneousLocalization.val_zero, map_zero, AlgebraicGeometry.Proj.zero_apply
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
f : A
x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)
hx : Membership.mem (γ := Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) (pbo f) x
hf :
  ∀ (z : (↑(CommRingCat.of (A⁰_ f)) : Type u_1)),
    Eq (α := (↑(Presheaf.stalk (Sheaf.presheaf (structureSheaf 𝒜)) x) : Type u_1))
      (((CommRingCat.Hom.hom (awayToSection 𝒜 f ≫ Presheaf.germ (Sheaf.presheaf (structureSheaf 𝒜)) (pbo f) x hx) :
              (↑(CommRingCat.of (A⁰_ f)) : Type u_1) →+*
                (↑(Presheaf.stalk (Sheaf.presheaf (structureSheaf 𝒜)) x) : Type u_1)) :
            (a : (↑(CommRingCat.of (A⁰_ f)) : Type u_1)) → (↑((structureSheaf 𝒜).presheaf.stalk x) : Type u_1))
          z :
        (↑(Presheaf.stalk (Sheaf.presheaf (structureSheaf 𝒜)) x) : Type u_1))
      ((CommRingCat.Hom.hom
              (CategoryStruct.comp (Y :=
                CommRingCat.of (HomogeneousLocalization 𝒜 x.asHomogeneousIdeal.toIdeal.primeCompl))
                (CommRingCat.ofHom (HomogeneousLocalization.mapId 𝒜 ⋯))
                (Iso.inv (RingEquiv.toCommRingCatIso («Proj».stalkIso' 𝒜 x)))) :
            (a : (↑(CommRingCat.of (A⁰_ f)) : Type u_1)) → (↑((structureSheaf 𝒜).presheaf.stalk x) : Type u_1))
          z :
        (↑(Presheaf.stalk (Sheaf.presheaf (structureSheaf 𝒜)) x) : Type u_1))
⊢ Eq (α := CommRingCat.of (A⁰_ f) ⟶ Presheaf.stalk (Sheaf.presheaf (structureSheaf 𝒜)) x)
    (awayToSection 𝒜 f ≫ Presheaf.germ (Sheaf.presheaf (structureSheaf 𝒜)) (pbo f) x hx :
      CommRingCat.of (A⁰_ f) ⟶ Presheaf.stalk (Sheaf.presheaf (structureSheaf 𝒜)) x)
    (CategoryStruct.comp (Y := CommRingCat.of (HomogeneousLocalization 𝒜 x.asHomogeneousIdeal.toIdeal.primeCompl))
        (CommRingCat.ofHom (HomogeneousLocalization.mapId 𝒜 ⋯))
        (Iso.inv (RingEquiv.toCommRingCatIso («Proj».stalkIso' 𝒜 x))) :
      CommRingCat.of (HomogeneousLocalization 𝒜 (Submonoid.powers f)) ⟶
        CommRingCat.of (↑(Presheaf.stalk (Sheaf.presheaf (structureSheaf 𝒜)) x) : Type u_1))

Tactic:
ext z