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
x : (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1)
asIdeal :
  ∀ (z : (↑(CommRingCat.of (A⁰_ f)) : Type u_1)),
    Membership.mem (γ := Ideal (↑(CommRingCat.of (A⁰_ f)) : Type u_1))
        (PrimeSpectrum.asIdeal
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC := carrier)
                (X :=
                (↑(Proj.restrict (U := Functor.obj (C := Opens (↑Proj.T : Type u_1)) (Opens.toTopCat Proj.T) (pbo f))
                        ⋯).toPresheafedSpace :
                  TopCat))
                (toSpec 𝒜 f) :
              (a : (↑(↑(Proj.restrict ⋯).toPresheafedSpace : TopCat) : Type u_1)) →
                (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1))
            (FromSpec.toFun f_deg hm x)))
        z ↔
      z ∈ x.asIdeal
⊢ PrimeSpectrum.asIdeal
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC := carrier)
            (X :=
            (↑(Proj.restrict (U := Functor.obj (C := Opens (↑Proj.T : Type u_1)) (Opens.toTopCat Proj.T) (pbo f))
                    ⋯).toPresheafedSpace :
              TopCat))
            (toSpec 𝒜 f) :
          (a : (↑(↑(Proj.restrict ⋯).toPresheafedSpace : TopCat) : Type u_1)) →
            (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1))
        (FromSpec.toFun f_deg hm x)) =
    x.asIdeal

Tactic:
ext z
-- 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
x : (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1)
z : (↑(CommRingCat.of (A⁰_ f)) : Type u_1)
asIdeal :
  ∀ (z : HomogeneousLocalization.NumDenSameDeg 𝒜 (Submonoid.powers f)),
    Membership.mem (γ := Ideal (↑(CommRingCat.of (A⁰_ f)) : Type u_1))
        (PrimeSpectrum.asIdeal
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC := carrier)
                (X :=
                (↑(Proj.restrict (U := Functor.obj (C := Opens (↑Proj.T : Type u_1)) (Opens.toTopCat Proj.T) (pbo f))
                        ⋯).toPresheafedSpace :
                  TopCat))
                (toSpec 𝒜 f) :
              (a : (↑(↑(Proj.restrict ⋯).toPresheafedSpace : TopCat) : Type u_1)) →
                (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1))
            (FromSpec.toFun f_deg hm x)))
        (HomogeneousLocalization.mk z) ↔
      HomogeneousLocalization.mk z ∈ x.asIdeal
⊢ Membership.mem (γ := Ideal (↑(CommRingCat.of (A⁰_ f)) : Type u_1))
      (PrimeSpectrum.asIdeal
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC := carrier)
              (X :=
              (↑(Proj.restrict (U := Functor.obj (C := Opens (↑Proj.T : Type u_1)) (Opens.toTopCat Proj.T) (pbo f))
                      ⋯).toPresheafedSpace :
                TopCat))
              (toSpec 𝒜 f) :
            (a : (↑(↑(Proj.restrict ⋯).toPresheafedSpace : TopCat) : Type u_1)) →
              (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1))
          (FromSpec.toFun f_deg hm x)))
      z ↔
    z ∈ x.asIdeal

Tactic:
obtain ⟨z, rfl⟩ := HomogeneousLocalization.mk_surjective z

Premises used: HomogeneousLocalization.mk_surjective, 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
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
x : (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1)
z : HomogeneousLocalization.NumDenSameDeg 𝒜 (Submonoid.powers f)
asIdeal :
  Membership.mem (γ := Ideal (↑(CommRingCat.of (A⁰_ f)) : Type u_1))
      (PrimeSpectrum.asIdeal
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC := carrier)
              (X :=
              (↑(Proj.restrict (U := Functor.obj (C := Opens (↑Proj.T : Type u_1)) (Opens.toTopCat Proj.T) (pbo f))
                      ⋯).toPresheafedSpace :
                TopCat))
              (toSpec 𝒜 f) :
            (a : (↑(↑(Proj.restrict ⋯).toPresheafedSpace : TopCat) : Type u_1)) →
              (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1))
          (FromSpec.toFun f_deg hm x)))
      (HomogeneousLocalization.mk z) ↔
    (↑z.num : A) ∈ FromSpec.carrier f_deg x
⊢ Membership.mem (γ := Ideal (↑(CommRingCat.of (A⁰_ f)) : Type u_1))
      (PrimeSpectrum.asIdeal
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC := carrier)
              (X :=
              (↑(Proj.restrict (U := Functor.obj (C := Opens (↑Proj.T : Type u_1)) (Opens.toTopCat Proj.T) (pbo f))
                      ⋯).toPresheafedSpace :
                TopCat))
              (toSpec 𝒜 f) :
            (a : (↑(↑(Proj.restrict ⋯).toPresheafedSpace : TopCat) : Type u_1)) →
              (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1))
          (FromSpec.toFun f_deg hm x)))
      (HomogeneousLocalization.mk z) ↔
    HomogeneousLocalization.mk z ∈ x.asIdeal

Tactic:
rw [← FromSpec.num_mem_carrier_iff f_deg hm x]

Premises used: AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.num_mem_carrier_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
x : (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1)
z : HomogeneousLocalization.NumDenSameDeg 𝒜 (Submonoid.powers f)
⊢ Membership.mem (γ := Ideal (↑(CommRingCat.of (A⁰_ f)) : Type u_1))
      (PrimeSpectrum.asIdeal
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC := carrier)
              (X :=
              (↑(Proj.restrict (U := Functor.obj (C := Opens (↑Proj.T : Type u_1)) (Opens.toTopCat Proj.T) (pbo f))
                      ⋯).toPresheafedSpace :
                TopCat))
              (toSpec 𝒜 f) :
            (a : (↑(↑(Proj.restrict ⋯).toPresheafedSpace : TopCat) : Type u_1)) →
              (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1))
          (FromSpec.toFun f_deg hm x)))
      (HomogeneousLocalization.mk z) ↔
    (↑z.num : A) ∈ FromSpec.carrier f_deg x

Tactic:
ToSpec.mk_mem_carrier _ z

Premises used: Set.Mem, setOf, AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier, AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.mk_mem_carrier
-- 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
x : (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1)
z : HomogeneousLocalization.NumDenSameDeg 𝒜 (Submonoid.powers f)
⊢ Membership.mem (γ := Ideal (↑(CommRingCat.of (A⁰_ f)) : Type u_1))
      (PrimeSpectrum.asIdeal
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC := carrier)
              (X :=
              (↑(Proj.restrict (U := Functor.obj (C := Opens (↑Proj.T : Type u_1)) (Opens.toTopCat Proj.T) (pbo f))
                      ⋯).toPresheafedSpace :
                TopCat))
              (toSpec 𝒜 f) :
            (a : (↑(↑(Proj.restrict ⋯).toPresheafedSpace : TopCat) : Type u_1)) →
              (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1))
          (FromSpec.toFun f_deg hm x)))
      (HomogeneousLocalization.mk z) ↔
    (↑z.num : A) ∈ FromSpec.carrier f_deg x

Tactic:
exact ToSpec.mk_mem_carrier _ z

Premises used: AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.mk_mem_carrier
-- 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
x :
  (↑(↑(Proj.restrict (U := Functor.obj (C := Opens (↑Proj.T : Type u_1)) (Opens.toTopCat Proj.T) (pbo f))
              ⋯).toPresheafedSpace :
        TopCat) :
    Type u_1)
⊢ FromSpec.toFun f_deg hm
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC := carrier)
            (X :=
            (↑(Proj.restrict (U := Functor.obj (C := Opens (↑Proj.T : Type u_1)) (Opens.toTopCat Proj.T) (pbo f))
                    ⋯).toPresheafedSpace :
              TopCat))
            (toSpec 𝒜 f) :
          (a : (↑(↑(Proj.restrict ⋯).toPresheafedSpace : TopCat) : Type u_1)) →
            (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1))
        x) =
    x

Tactic:
Subtype.ext <| ProjectiveSpectrum.ext <| HomogeneousIdeal.ext' ?_

Premises used: HomogeneousIdeal.ext', ProjectiveSpectrum.ext, Subtype.ext
-- 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
x :
  (↑(↑(Proj.restrict (U := Functor.obj (C := Opens (↑Proj.T : Type u_1)) (Opens.toTopCat Proj.T) (pbo f))
              ⋯).toPresheafedSpace :
        TopCat) :
    Type u_1)
refine :
  ∀ (i : ℕ),
    ∀ x_1 ∈ 𝒜 i,
      Membership.mem (γ := HomogeneousIdeal 𝒜)
          (ProjectiveSpectrum.asHomogeneousIdeal
              (↑(FromSpec.toFun f_deg hm
                    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
                          carrier) (X :=
                          (↑(Proj.restrict (U :=
                                  Functor.obj (C := Opens (↑Proj.T : Type u_1)) (Opens.toTopCat Proj.T) (pbo f))
                                  ⋯).toPresheafedSpace :
                            TopCat))
                          (toSpec 𝒜 f) :
                        (a : (↑(↑(Proj.restrict ⋯).toPresheafedSpace : TopCat) : Type u_1)) →
                          (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1))
                      x)) :
                (↑Proj.T : Type u_1)) :
            HomogeneousIdeal 𝒜)
          x_1 ↔
        x_1 ∈ (↑x : (↑Proj.T : Type u_1)).asHomogeneousIdeal
⊢ FromSpec.toFun f_deg hm
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC := carrier)
            (X :=
            (↑(Proj.restrict (U := Functor.obj (C := Opens (↑Proj.T : Type u_1)) (Opens.toTopCat Proj.T) (pbo f))
                    ⋯).toPresheafedSpace :
              TopCat))
            (toSpec 𝒜 f) :
          (a : (↑(↑(Proj.restrict ⋯).toPresheafedSpace : TopCat) : Type u_1)) →
            (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1))
        x) =
    x

Tactic:
refine Subtype.ext <| ProjectiveSpectrum.ext <| HomogeneousIdeal.ext' ?_

Premises used: HomogeneousIdeal.ext', ProjectiveSpectrum.ext, Subtype.ext
-- 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
x :
  (↑(↑(Proj.restrict (U := Functor.obj (C := Opens (↑Proj.T : Type u_1)) (Opens.toTopCat Proj.T) (pbo f))
              ⋯).toPresheafedSpace :
        TopCat) :
    Type u_1)
i : ℕ
z : A
hzi : z ∈ 𝒜 i
⊢ Membership.mem (γ := HomogeneousIdeal 𝒜)
      (ProjectiveSpectrum.asHomogeneousIdeal
          (↑(FromSpec.toFun f_deg hm
                ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
                      carrier) (X :=
                      (↑(Proj.restrict (U :=
                              Functor.obj (C := Opens (↑Proj.T : Type u_1)) (Opens.toTopCat Proj.T) (pbo f))
                              ⋯).toPresheafedSpace :
                        TopCat))
                      (toSpec 𝒜 f) :
                    (a : (↑(↑(Proj.restrict ⋯).toPresheafedSpace : TopCat) : Type u_1)) →
                      (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1))
                  x)) :
            (↑Proj.T : Type u_1)) :
        HomogeneousIdeal 𝒜)
      z ↔
    z ∈ (↑x : (↑Proj.T : Type u_1)).asHomogeneousIdeal

Tactic:
(FromSpec.mem_carrier_iff_of_mem f_deg hm _ _ hzi).trans ?_

Premises used: Set.Mem, setOf, AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier, AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.mem_carrier_iff_of_mem, Iff.trans
-- 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
x :
  (↑(↑(Proj.restrict (U := Functor.obj (C := Opens (↑Proj.T : Type u_1)) (Opens.toTopCat Proj.T) (pbo f))
              ⋯).toPresheafedSpace :
        TopCat) :
    Type u_1)
i : ℕ
z : A
hzi : z ∈ 𝒜 i
refine :
  Membership.mem (γ := Ideal (↑(CommRingCat.of (A⁰_ f)) : Type u_1))
      (PrimeSpectrum.asIdeal
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC := carrier)
              (X :=
              (↑(Proj.restrict (U := Functor.obj (C := Opens (↑Proj.T : Type u_1)) (Opens.toTopCat Proj.T) (pbo f))
                      ⋯).toPresheafedSpace :
                TopCat))
              (toSpec 𝒜 f) :
            (a : (↑(↑(Proj.restrict ⋯).toPresheafedSpace : TopCat) : Type u_1)) →
              (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1))
          x))
      (HomogeneousLocalization.mk
        { deg := m * i, num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i)) (z ^ m) ⋯,
          den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i)) (f ^ i) ⋯, den_mem := ⋯ }) ↔
    z ∈ (↑x : (↑Proj.T : Type u_1)).asHomogeneousIdeal
⊢ Membership.mem (γ := HomogeneousIdeal 𝒜)
      (ProjectiveSpectrum.asHomogeneousIdeal
          (↑(FromSpec.toFun f_deg hm
                ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
                      carrier) (X :=
                      (↑(Proj.restrict (U :=
                              Functor.obj (C := Opens (↑Proj.T : Type u_1)) (Opens.toTopCat Proj.T) (pbo f))
                              ⋯).toPresheafedSpace :
                        TopCat))
                      (toSpec 𝒜 f) :
                    (a : (↑(↑(Proj.restrict ⋯).toPresheafedSpace : TopCat) : Type u_1)) →
                      (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1))
                  x)) :
            (↑Proj.T : Type u_1)) :
        HomogeneousIdeal 𝒜)
      z ↔
    z ∈ (↑x : (↑Proj.T : Type u_1)).asHomogeneousIdeal

Tactic:
refine (FromSpec.mem_carrier_iff_of_mem f_deg hm _ _ hzi).trans ?_

Premises used: AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.mem_carrier_iff_of_mem, Iff.trans
-- 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
x :
  (↑(↑(Proj.restrict (U := Functor.obj (C := Opens (↑Proj.T : Type u_1)) (Opens.toTopCat Proj.T) (pbo f))
              ⋯).toPresheafedSpace :
        TopCat) :
    Type u_1)
i : ℕ
z : A
hzi : z ∈ 𝒜 i
⊢ Membership.mem (γ := Ideal (↑(CommRingCat.of (A⁰_ f)) : Type u_1))
      (PrimeSpectrum.asIdeal
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC := carrier)
              (X :=
              (↑(Proj.restrict (U := Functor.obj (C := Opens (↑Proj.T : Type u_1)) (Opens.toTopCat Proj.T) (pbo f))
                      ⋯).toPresheafedSpace :
                TopCat))
              (toSpec 𝒜 f) :
            (a : (↑(↑(Proj.restrict ⋯).toPresheafedSpace : TopCat) : Type u_1)) →
              (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1))
          x))
      (HomogeneousLocalization.mk
        { deg := m * i, num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i)) (z ^ m) ⋯,
          den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i)) (f ^ i) ⋯, den_mem := ⋯ }) ↔
    z ∈ (↑x : (↑Proj.T : Type u_1)).asHomogeneousIdeal

Tactic:
(ToSpec.mk_mem_carrier _ _).trans (x.1.2.pow_mem_iff_mem m hm)

Premises used: Ideal.IsPrime.pow_mem_iff_mem, Set.Mem, ProjectiveSpectrum.isPrime, AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.mk_mem_carrier, Iff.trans, Subtype.val
-- 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
x :
  (↑(↑(Proj.restrict (U := Functor.obj (C := Opens (↑Proj.T : Type u_1)) (Opens.toTopCat Proj.T) (pbo f))
              ⋯).toPresheafedSpace :
        TopCat) :
    Type u_1)
i : ℕ
z : A
hzi : z ∈ 𝒜 i
⊢ Membership.mem (γ := Ideal (↑(CommRingCat.of (A⁰_ f)) : Type u_1))
      (PrimeSpectrum.asIdeal
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC := carrier)
              (X :=
              (↑(Proj.restrict (U := Functor.obj (C := Opens (↑Proj.T : Type u_1)) (Opens.toTopCat Proj.T) (pbo f))
                      ⋯).toPresheafedSpace :
                TopCat))
              (toSpec 𝒜 f) :
            (a : (↑(↑(Proj.restrict ⋯).toPresheafedSpace : TopCat) : Type u_1)) →
              (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1))
          x))
      (HomogeneousLocalization.mk
        { deg := m * i, num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i)) (z ^ m) ⋯,
          den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i)) (f ^ i) ⋯, den_mem := ⋯ }) ↔
    z ∈ (↑x : (↑Proj.T : Type u_1)).asHomogeneousIdeal

Tactic:
exact (ToSpec.mk_mem_carrier _ _).trans (x.1.2.pow_mem_iff_mem m hm)

Premises used: AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.mk_mem_carrier, Iff.trans
-- 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
x₁ x₂ :
  (↑(↑(Proj.restrict (U := Functor.obj (C := Opens (↑Proj.T : Type u_1)) (Opens.toTopCat Proj.T) (pbo f))
              ⋯).toPresheafedSpace :
        TopCat) :
    Type u_1)
h :
  Eq (α := (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC := carrier) (X :=
            (↑(Proj.restrict (U := Functor.obj (C := Opens (↑Proj.T : Type u_1)) (Opens.toTopCat Proj.T) (pbo f))
                    ⋯).toPresheafedSpace :
              TopCat))
            (toSpec 𝒜 f) :
          (a : (↑(↑(Proj.restrict ⋯).toPresheafedSpace : TopCat) : Type u_1)) →
            (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1))
        x₁ :
      (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC := carrier) (X :=
            (↑(Proj.restrict (U := Functor.obj (C := Opens (↑Proj.T : Type u_1)) (Opens.toTopCat Proj.T) (pbo f))
                    ⋯).toPresheafedSpace :
              TopCat))
            (toSpec 𝒜 f) :
          (a : (↑(↑(Proj.restrict ⋯).toPresheafedSpace : TopCat) : Type u_1)) →
            (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1))
        x₂ :
      (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1))
⊢ Eq (α :=
    (↑(↑(Proj.restrict (U := Functor.obj (C := Opens (↑Proj.T : Type u_1)) (Opens.toTopCat Proj.T) (pbo f))
                ⋯).toPresheafedSpace :
          TopCat) :
      Type u_1))
    (FromSpec.toFun f_deg hm
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC := carrier)
            (X :=
            (↑(Proj.restrict (U := Functor.obj (C := Opens (↑Proj.T : Type u_1)) (Opens.toTopCat Proj.T) (pbo f))
                    ⋯).toPresheafedSpace :
              TopCat))
            (toSpec 𝒜 f) :
          (a : (↑(↑(Proj.restrict ⋯).toPresheafedSpace : TopCat) : Type u_1)) →
            (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1))
        x₁))
    (FromSpec.toFun f_deg hm
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC := carrier)
            (X :=
            (↑(Proj.restrict (U := Functor.obj (C := Opens (↑Proj.T : Type u_1)) (Opens.toTopCat Proj.T) (pbo f))
                    ⋯).toPresheafedSpace :
              TopCat))
            (toSpec 𝒜 f) :
          (a : (↑(↑(Proj.restrict ⋯).toPresheafedSpace : TopCat) : Type u_1)) →
            (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1))
        x₂))

Tactic:
have := congr_arg (FromSpec.toFun f_deg hm) h
-- 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
⊢ Function.Surjective (α :=
    (↑(↑(Proj.restrict (U := Functor.obj (C := Opens (↑Proj.T : Type u_1)) (Opens.toTopCat Proj.T) (pbo f))
                ⋯).toPresheafedSpace :
          TopCat) :
      Type u_1))
    (β := (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC := carrier) (X :=
          (↑(Proj.restrict (U := Functor.obj (C := Opens (↑Proj.T : Type u_1)) (Opens.toTopCat Proj.T) (pbo f))
                  ⋯).toPresheafedSpace :
            TopCat))
          (toSpec 𝒜 f)) :
      (a : (↑(↑(Proj.restrict ⋯).toPresheafedSpace : TopCat) : Type u_1)) →
        (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1))

Tactic:
Function.surjective_iff_hasRightInverse |>.mpr
    ⟨FromSpec.toFun f_deg hm, toSpec_fromSpec 𝒜 f_deg hm⟩

Premises used: Iff.mpr, AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_fromSpec, Function.surjective_iff_hasRightInverse, Exists.intro, AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.toFun
-- 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
⊢ Function.Bijective (α :=
    (↑(↑(Proj.restrict (U := Functor.obj (C := Opens (↑Proj.T : Type u_1)) (Opens.toTopCat Proj.T) (pbo f))
                ⋯).toPresheafedSpace :
          TopCat) :
      Type u_1))
    (β := (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC := carrier) (X :=
          (↑(Proj.restrict (U := Functor.obj (C := Opens (↑Proj.T : Type u_1)) (Opens.toTopCat Proj.T) (pbo f))
                  ⋯).toPresheafedSpace :
            TopCat))
          (toSpec 𝒜 f)) :
      (a : (↑(↑(Proj.restrict ⋯).toPresheafedSpace : TopCat) : Type u_1)) →
        (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1))

Tactic:
⟨toSpec_injective 𝒜 f_deg hm, toSpec_surjective 𝒜 f_deg hm⟩

Premises used: AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_injective, AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_surjective, And.intro, Function.Bijective
-- 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 : ℕ
rw : f ^ i ∈ 𝒜 (i * m)
⊢ f ^ i ∈ 𝒜 (m * i)

Tactic:
rw [mul_comm]

Premises used: mul_comm
-- 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:
SetLike.pow_mem_graded _ f_deg

Premises used: Set.Mem, SetLike.pow_mem_graded