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
q : (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1)
x y : A
h_1 : IsHomogeneousElem 𝒜 x
h_2 : IsHomogeneousElem 𝒜 y
hxy : x * y ∈ asIdeal f_deg hm q
nx : ℕ
hnx : x ∈ 𝒜 nx
ny : ℕ
hny : y ∈ 𝒜 ny
h :
  Eq (α := Localization (Submonoid.powers f))
    (Localization.mk (x ^ m * y ^ m)
      (HMul.hMul (α := ↥(Submonoid.powers f))
        (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers f) x) (f ^ nx) ⋯)
        (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers f) x) (f ^ ny) ⋯)))
    (Localization.mk (x ^ m * y ^ m)
      (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers f) x) (f ^ nx * f ^ ny) ⋯))
⊢ HMul.hMul (α := A⁰_ f)
      (HomogeneousLocalization.mk
        { deg := m * nx, num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * nx)) (x ^ m) ⋯,
          den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * nx)) (f ^ nx) ⋯, den_mem := ⋯ :
          NumDenSameDeg 𝒜 (Submonoid.powers f) })
      (HomogeneousLocalization.mk
        { deg := m * ny, num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * ny)) (y ^ m) ⋯,
          den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * ny)) (f ^ ny) ⋯, den_mem := ⋯ :
          NumDenSameDeg 𝒜 (Submonoid.powers f) }) =
    HomogeneousLocalization.mk
      { deg := m * (nx + ny), num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * (nx + ny))) (x ^ m * y ^ m) ⋯,
        den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * (nx + ny))) (f ^ nx * f ^ ny) ⋯, den_mem := ⋯ }

Tactic:
simp only [HomogeneousLocalization.ext_iff_val, HomogeneousLocalization.val_mk,
          HomogeneousLocalization.val_mul, Localization.mk_mul]

Premises used: HomogeneousLocalization.val_mk, HomogeneousLocalization.ext_iff_val, HomogeneousLocalization.val_mul, Localization.mk_mul
-- 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
q : (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1)
x y : A
h : IsHomogeneousElem 𝒜 x
h_1 : IsHomogeneousElem 𝒜 y
hxy : x * y ∈ asIdeal f_deg hm q
nx : ℕ
hnx : x ∈ 𝒜 nx
ny : ℕ
hny : y ∈ 𝒜 ny
⊢ Eq (α := Localization (Submonoid.powers f))
    (Localization.mk (x ^ m * y ^ m)
      (HMul.hMul (α := ↥(Submonoid.powers f))
        (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers f) x) (f ^ nx) ⋯)
        (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers f) x) (f ^ ny) ⋯)))
    (Localization.mk (x ^ m * y ^ m)
      (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers f) x) (f ^ nx * f ^ ny) ⋯))

Tactic:
simp only [Submonoid.mk_mul_mk, mk_eq_monoidOf_mk']

Premises used: Localization.mk_eq_monoidOf_mk', Submonoid.mk_mul_mk
-- 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
q : (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1)
x y : A
h : IsHomogeneousElem 𝒜 x
h_1 : IsHomogeneousElem 𝒜 y
hxy : x * y ∈ asIdeal f_deg hm q
nx : ℕ
hnx : x ∈ 𝒜 nx
ny : ℕ
hny : y ∈ 𝒜 ny
n : ℕ
hn : n ≠ ny
⊢ 0 ∈ q.asIdeal

Tactic:
q.1.zero_mem

Premises used: Ideal.zero_mem, PrimeSpectrum.asIdeal
-- 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
q : (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1)
x y : A
h_1 : IsHomogeneousElem 𝒜 x
h_2 : IsHomogeneousElem 𝒜 y
hxy : x * y ∈ asIdeal f_deg hm q
nx : ℕ
hnx : x ∈ 𝒜 nx
ny : ℕ
hny : y ∈ 𝒜 ny
n : ℕ
hn : n ≠ ny
h :
  Eq (α := HomogeneousLocalization 𝒜 (Submonoid.powers f))
    (HomogeneousLocalization.mk
      { deg := m * n,
        num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * n)) (HPow.hPow (α := A) ((proj 𝒜 n : (a : A) → A) y : A) m) ⋯,
        den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * n)) (f ^ n) ⋯, den_mem := ⋯ })
    0
⊢ HomogeneousLocalization.mk
      { deg := m * n,
        num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * n)) (HPow.hPow (α := A) ((proj 𝒜 n : (a : A) → A) y : A) m) ⋯,
        den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * n)) (f ^ n) ⋯, den_mem := ⋯ } ∈
    q.asIdeal

Tactic:
convert! q.1.zero_mem using 1

Premises used: Ideal.zero_mem, PrimeSpectrum.asIdeal
-- 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
q : (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1)
x y : A
h_1 : IsHomogeneousElem 𝒜 x
h_2 : IsHomogeneousElem 𝒜 y
hxy : x * y ∈ asIdeal f_deg hm q
nx : ℕ
hnx : x ∈ 𝒜 nx
ny : ℕ
hny : y ∈ 𝒜 ny
n : ℕ
hn : n ≠ ny
h :
  Eq (α := Localization (Submonoid.powers f))
    (Localization.mk
      (↑(NumDenSameDeg.num
            { deg := m * n,
              num :=
                Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * n)) (HPow.hPow (α := A) ((proj 𝒜 n : (a : A) → A) y : A) m) ⋯,
              den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * n)) (f ^ n) ⋯, den_mem := ⋯ }) :
        A)
      (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers f) x)
        (↑(NumDenSameDeg.den
              { deg := m * n,
                num :=
                  Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * n)) (HPow.hPow (α := A) ((proj 𝒜 n : (a : A) → A) y : A) m)
                    ⋯,
                den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * n)) (f ^ n) ⋯, den_mem := ⋯ }) :
          A)
        ⋯))
    0
⊢ Eq (α := HomogeneousLocalization 𝒜 (Submonoid.powers f))
    (HomogeneousLocalization.mk
      { deg := m * n,
        num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * n)) (HPow.hPow (α := A) ((proj 𝒜 n : (a : A) → A) y : A) m) ⋯,
        den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * n)) (f ^ n) ⋯, den_mem := ⋯ })
    0

Tactic:
rw [HomogeneousLocalization.ext_iff_val, HomogeneousLocalization.val_mk,
          HomogeneousLocalization.val_zero]

Premises used: HomogeneousLocalization.val_zero, HomogeneousLocalization.val_mk, HomogeneousLocalization.ext_iff_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
q : (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1)
x y : A
h_1 : IsHomogeneousElem 𝒜 x
h_2 : IsHomogeneousElem 𝒜 y
hxy : x * y ∈ asIdeal f_deg hm q
nx : ℕ
hnx : x ∈ 𝒜 nx
ny : ℕ
hny : y ∈ 𝒜 ny
n : ℕ
hn : n ≠ ny
h :
  Eq (α := Localization (Submonoid.powers f))
    (Localization.mk
      ((↑((((decompose 𝒜 : (a : A) → ⨁ (i : ℕ), ↥(𝒜 i)) y : ⨁ (i : ℕ), ↥(𝒜 i)) : (a : ℕ) → ↥(𝒜 a)) n) : A) ^ m)
      (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers f) x) (f ^ n) ⋯))
    0
⊢ Eq (α := Localization (Submonoid.powers f))
    (Localization.mk
      (↑(NumDenSameDeg.num
            { deg := m * n,
              num :=
                Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * n)) (HPow.hPow (α := A) ((proj 𝒜 n : (a : A) → A) y : A) m) ⋯,
              den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * n)) (f ^ n) ⋯, den_mem := ⋯ }) :
        A)
      (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers f) x)
        (↑(NumDenSameDeg.den
              { deg := m * n,
                num :=
                  Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * n)) (HPow.hPow (α := A) ((proj 𝒜 n : (a : A) → A) y : A) m)
                    ⋯,
                den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * n)) (f ^ n) ⋯, den_mem := ⋯ }) :
          A)
        ⋯))
    0

Tactic:
simp_rw [proj_apply]

Premises used: GradedRing.proj_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
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
q : (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1)
x y : A
h : IsHomogeneousElem 𝒜 x
h_1 : IsHomogeneousElem 𝒜 y
hxy : x * y ∈ asIdeal f_deg hm q
nx : ℕ
hnx : x ∈ 𝒜 nx
ny : ℕ
hny : y ∈ 𝒜 ny
n : ℕ
hn : n ≠ ny
⊢ Eq (α := Localization (Submonoid.powers f))
    (Localization.mk 0
      (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers f) x) (f ^ n) ⋯))
    0

Tactic:
mk_zero (S := Submonoid.powers f) _

Premises used: Localization.mk_zero
-- 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
q : (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1)
x y : A
h_1 : IsHomogeneousElem 𝒜 x
h_2 : IsHomogeneousElem 𝒜 y
hxy : x * y ∈ asIdeal f_deg hm q
nx : ℕ
hnx : x ∈ 𝒜 nx
ny : ℕ
hny : y ∈ 𝒜 ny
n : ℕ
hn : n ≠ ny
h : (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ℕ), ↥(𝒜 i)) y : ⨁ (i : ℕ), ↥(𝒜 i)) : (a : ℕ) → ↥(𝒜 a)) n) : A) ^ m = 0
⊢ Eq (α := Localization (Submonoid.powers f))
    (Localization.mk
      ((↑((((decompose 𝒜 : (a : A) → ⨁ (i : ℕ), ↥(𝒜 i)) y : ⨁ (i : ℕ), ↥(𝒜 i)) : (a : ℕ) → ↥(𝒜 a)) n) : A) ^ m)
      (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers f) x) (f ^ n) ⋯))
    0

Tactic:
convert! mk_zero (S := Submonoid.powers f) _

Premises used: Localization.mk_zero
-- 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
q : (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1)
x y : A
h : IsHomogeneousElem 𝒜 x
h_1 : IsHomogeneousElem 𝒜 y
hxy : x * y ∈ asIdeal f_deg hm q
nx : ℕ
hnx : x ∈ 𝒜 nx
ny : ℕ
hny : y ∈ 𝒜 ny
n : ℕ
hn : n ≠ ny
rw : y ∈ 𝒜 ny
⊢ (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ℕ), ↥(𝒜 i)) y : ⨁ (i : ℕ), ↥(𝒜 i)) : (a : ℕ) → ↥(𝒜 a)) n) : A) ^ m = 0

Tactic:
rw [decompose_of_mem_ne 𝒜 _ hn.symm, zero_pow hm.ne']

Premises used: Ne.symm, LT.lt.ne', DirectSum.decompose_of_mem_ne, zero_pow
-- 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
q : (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1)
x y : A
h : IsHomogeneousElem 𝒜 x
h_1 : IsHomogeneousElem 𝒜 y
hxy : x * y ∈ asIdeal f_deg hm q
nx : ℕ
hnx : x ∈ 𝒜 nx
ny : ℕ
hny : y ∈ 𝒜 ny
n : ℕ
hn : n ≠ ny
⊢ y ∈ 𝒜 ny

Tactic:
hnx
-- 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
q : (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1)
x y : A
h : IsHomogeneousElem 𝒜 x
h_1 : IsHomogeneousElem 𝒜 y
hxy : x * y ∈ asIdeal f_deg hm q
nx : ℕ
hnx : x ∈ 𝒜 nx
ny : ℕ
hny : y ∈ 𝒜 ny
n : ℕ
hn : n ≠ ny
⊢ y ∈ 𝒜 ny

Tactic:
hny
-- 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
q : (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1)
x y : A
h : IsHomogeneousElem 𝒜 x
h_1 : IsHomogeneousElem 𝒜 y
hxy : x * y ∈ asIdeal f_deg hm q
nx : ℕ
hnx : x ∈ 𝒜 nx
ny : ℕ
hny : y ∈ 𝒜 ny
n : ℕ
hn : n ≠ ny
⊢ y ∈ 𝒜 ny

Tactic:
exact hny
-- 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
q : (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1)
x y : A
h : IsHomogeneousElem 𝒜 x
h_1 : IsHomogeneousElem 𝒜 y
hxy : x * y ∈ asIdeal f_deg hm q
nx : ℕ
hnx : x ∈ 𝒜 nx
ny : ℕ
hny : y ∈ 𝒜 ny
n : ℕ
hn : n ≠ ny
⊢ y ∈ 𝒜 ny

Tactic:
first | exact hnx | exact hny
-- 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
q : (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1)
x y : A
h : IsHomogeneousElem 𝒜 x
h_1 : IsHomogeneousElem 𝒜 y
hxy : x * y ∈ asIdeal f_deg hm q
nx : ℕ
hnx : x ∈ 𝒜 nx
ny : ℕ
hny : y ∈ 𝒜 ny
n : ℕ
hn : n ≠ nx
⊢ 0 ∈ q.asIdeal

Tactic:
q.1.zero_mem

Premises used: Ideal.zero_mem, PrimeSpectrum.asIdeal
-- 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
q : (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1)
x y : A
h_1 : IsHomogeneousElem 𝒜 x
h_2 : IsHomogeneousElem 𝒜 y
hxy : x * y ∈ asIdeal f_deg hm q
nx : ℕ
hnx : x ∈ 𝒜 nx
ny : ℕ
hny : y ∈ 𝒜 ny
n : ℕ
hn : n ≠ nx
h :
  Eq (α := HomogeneousLocalization 𝒜 (Submonoid.powers f))
    (HomogeneousLocalization.mk
      { deg := m * n,
        num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * n)) (HPow.hPow (α := A) ((proj 𝒜 n : (a : A) → A) x : A) m) ⋯,
        den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * n)) (f ^ n) ⋯, den_mem := ⋯ })
    0
⊢ HomogeneousLocalization.mk
      { deg := m * n,
        num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * n)) (HPow.hPow (α := A) ((proj 𝒜 n : (a : A) → A) x : A) m) ⋯,
        den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * n)) (f ^ n) ⋯, den_mem := ⋯ } ∈
    q.asIdeal

Tactic:
convert! q.1.zero_mem using 1

Premises used: Ideal.zero_mem, PrimeSpectrum.asIdeal
-- 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
q : (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1)
x y : A
h_1 : IsHomogeneousElem 𝒜 x
h_2 : IsHomogeneousElem 𝒜 y
hxy : x * y ∈ asIdeal f_deg hm q
nx : ℕ
hnx : x ∈ 𝒜 nx
ny : ℕ
hny : y ∈ 𝒜 ny
n : ℕ
hn : n ≠ nx
h :
  Eq (α := Localization (Submonoid.powers f))
    (Localization.mk
      (↑(NumDenSameDeg.num
            { deg := m * n,
              num :=
                Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * n)) (HPow.hPow (α := A) ((proj 𝒜 n : (a : A) → A) x : A) m) ⋯,
              den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * n)) (f ^ n) ⋯, den_mem := ⋯ }) :
        A)
      (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers f) x)
        (↑(NumDenSameDeg.den
              { deg := m * n,
                num :=
                  Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * n)) (HPow.hPow (α := A) ((proj 𝒜 n : (a : A) → A) x : A) m)
                    ⋯,
                den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * n)) (f ^ n) ⋯, den_mem := ⋯ }) :
          A)
        ⋯))
    0
⊢ Eq (α := HomogeneousLocalization 𝒜 (Submonoid.powers f))
    (HomogeneousLocalization.mk
      { deg := m * n,
        num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * n)) (HPow.hPow (α := A) ((proj 𝒜 n : (a : A) → A) x : A) m) ⋯,
        den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * n)) (f ^ n) ⋯, den_mem := ⋯ })
    0

Tactic:
rw [HomogeneousLocalization.ext_iff_val, HomogeneousLocalization.val_mk,
          HomogeneousLocalization.val_zero]

Premises used: HomogeneousLocalization.val_zero, HomogeneousLocalization.val_mk, HomogeneousLocalization.ext_iff_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
q : (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1)
x y : A
h_1 : IsHomogeneousElem 𝒜 x
h_2 : IsHomogeneousElem 𝒜 y
hxy : x * y ∈ asIdeal f_deg hm q
nx : ℕ
hnx : x ∈ 𝒜 nx
ny : ℕ
hny : y ∈ 𝒜 ny
n : ℕ
hn : n ≠ nx
h :
  Eq (α := Localization (Submonoid.powers f))
    (Localization.mk
      ((↑((((decompose 𝒜 : (a : A) → ⨁ (i : ℕ), ↥(𝒜 i)) x : ⨁ (i : ℕ), ↥(𝒜 i)) : (a : ℕ) → ↥(𝒜 a)) n) : A) ^ m)
      (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers f) x) (f ^ n) ⋯))
    0
⊢ Eq (α := Localization (Submonoid.powers f))
    (Localization.mk
      (↑(NumDenSameDeg.num
            { deg := m * n,
              num :=
                Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * n)) (HPow.hPow (α := A) ((proj 𝒜 n : (a : A) → A) x : A) m) ⋯,
              den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * n)) (f ^ n) ⋯, den_mem := ⋯ }) :
        A)
      (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers f) x)
        (↑(NumDenSameDeg.den
              { deg := m * n,
                num :=
                  Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * n)) (HPow.hPow (α := A) ((proj 𝒜 n : (a : A) → A) x : A) m)
                    ⋯,
                den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * n)) (f ^ n) ⋯, den_mem := ⋯ }) :
          A)
        ⋯))
    0

Tactic:
simp_rw [proj_apply]

Premises used: GradedRing.proj_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
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
q : (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1)
x y : A
h : IsHomogeneousElem 𝒜 x
h_1 : IsHomogeneousElem 𝒜 y
hxy : x * y ∈ asIdeal f_deg hm q
nx : ℕ
hnx : x ∈ 𝒜 nx
ny : ℕ
hny : y ∈ 𝒜 ny
n : ℕ
hn : n ≠ nx
⊢ Eq (α := Localization (Submonoid.powers f))
    (Localization.mk 0
      (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers f) x) (f ^ n) ⋯))
    0

Tactic:
mk_zero (S := Submonoid.powers f) _

Premises used: Localization.mk_zero
-- 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
q : (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1)
x y : A
h_1 : IsHomogeneousElem 𝒜 x
h_2 : IsHomogeneousElem 𝒜 y
hxy : x * y ∈ asIdeal f_deg hm q
nx : ℕ
hnx : x ∈ 𝒜 nx
ny : ℕ
hny : y ∈ 𝒜 ny
n : ℕ
hn : n ≠ nx
h : (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ℕ), ↥(𝒜 i)) x : ⨁ (i : ℕ), ↥(𝒜 i)) : (a : ℕ) → ↥(𝒜 a)) n) : A) ^ m = 0
⊢ Eq (α := Localization (Submonoid.powers f))
    (Localization.mk
      ((↑((((decompose 𝒜 : (a : A) → ⨁ (i : ℕ), ↥(𝒜 i)) x : ⨁ (i : ℕ), ↥(𝒜 i)) : (a : ℕ) → ↥(𝒜 a)) n) : A) ^ m)
      (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers f) x) (f ^ n) ⋯))
    0

Tactic:
convert! mk_zero (S := Submonoid.powers f) _

Premises used: Localization.mk_zero
-- 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
q : (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1)
x y : A
h : IsHomogeneousElem 𝒜 x
h_1 : IsHomogeneousElem 𝒜 y
hxy : x * y ∈ asIdeal f_deg hm q
nx : ℕ
hnx : x ∈ 𝒜 nx
ny : ℕ
hny : y ∈ 𝒜 ny
n : ℕ
hn : n ≠ nx
rw : x ∈ 𝒜 nx
⊢ (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ℕ), ↥(𝒜 i)) x : ⨁ (i : ℕ), ↥(𝒜 i)) : (a : ℕ) → ↥(𝒜 a)) n) : A) ^ m = 0

Tactic:
rw [decompose_of_mem_ne 𝒜 _ hn.symm, zero_pow hm.ne']

Premises used: Ne.symm, LT.lt.ne', DirectSum.decompose_of_mem_ne, zero_pow
-- 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
q : (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1)
x y : A
h : IsHomogeneousElem 𝒜 x
h_1 : IsHomogeneousElem 𝒜 y
hxy : x * y ∈ asIdeal f_deg hm q
nx : ℕ
hnx : x ∈ 𝒜 nx
ny : ℕ
hny : y ∈ 𝒜 ny
n : ℕ
hn : n ≠ nx
⊢ x ∈ 𝒜 nx

Tactic:
hnx
-- 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
q : (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1)
x y : A
h : IsHomogeneousElem 𝒜 x
h_1 : IsHomogeneousElem 𝒜 y
hxy : x * y ∈ asIdeal f_deg hm q
nx : ℕ
hnx : x ∈ 𝒜 nx
ny : ℕ
hny : y ∈ 𝒜 ny
n : ℕ
hn : n ≠ nx
⊢ x ∈ 𝒜 nx

Tactic:
exact hnx
-- 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
q : (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1)
x y : A
h : IsHomogeneousElem 𝒜 x
h_1 : IsHomogeneousElem 𝒜 y
hxy : x * y ∈ asIdeal f_deg hm q
nx : ℕ
hnx : x ∈ 𝒜 nx
ny : ℕ
hny : y ∈ 𝒜 ny
n : ℕ
hn : n ≠ nx
⊢ x ∈ 𝒜 nx

Tactic:
first | exact hnx | exact hny
-- 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 :
  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
⊢ (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

Tactic:
apply PrimeSpectrum.ext

Premises used: PrimeSpectrum.ext