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
x : ↥(pbo f)
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
this : Algebra (A⁰_ f) (AtPrime 𝒜 (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal) :=
  RingHom.toAlgebra (mapId 𝒜 ⋯)
y z : NumDenSameDeg 𝒜 (Submonoid.powers f)
e :
  Eq (α := Localization (M := A) (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl)
    (HomogeneousLocalization.val.{0, u_1, u_2} (ι := ℕ) (σ := σ) (𝒜 := 𝒜)
      ((algebraMap (A⁰_ f) (AtPrime 𝒜 (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal) :
          (a : A⁰_ f) → AtPrime 𝒜 (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal)
        (HomogeneousLocalization.mk y)))
    (HomogeneousLocalization.val.{0, u_1, u_2} (ι := ℕ) (σ := σ) (𝒜 := 𝒜)
      ((algebraMap (A⁰_ f) (AtPrime 𝒜 (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal) :
          (a : A⁰_ f) → AtPrime 𝒜 (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal)
        (HomogeneousLocalization.mk z)))
⊢ Eq (α := Localization (M := A) (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl)
    ((algebraMap A (Localization (M := A) (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl) :
          (a : A) → Localization (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl)
        ((↑z.den : A) * (↑y.num : A)) :
      Localization (M := A) (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl)
    ((algebraMap A (Localization (M := A) (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl) :
          (a : A) → Localization (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl)
        ((↑y.den : A) * (↑z.num : A)) :
      Localization (M := A) (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl)

Tactic:
simp only [RingHom.algebraMap_toAlgebra, map_mk, GradedRingHom.id_apply, val_mk, mk_eq_mk',
        IsLocalization.mk'_eq_iff_eq] at e

Premises used: HomogeneousLocalization.map_mk, Localization.mk_eq_mk', GradedRingHom.id_apply, HomogeneousLocalization.val_mk, IsLocalization.mk'_eq_iff_eq, RingHom.algebraMap_toAlgebra
-- 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 : ↥(pbo f)
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
this : Algebra (A⁰_ f) (AtPrime 𝒜 (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal) :=
  RingHom.toAlgebra (mapId 𝒜 ⋯)
y z : NumDenSameDeg 𝒜 (Submonoid.powers f)
e :
  Eq (α := Localization (M := A) (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl)
    ((algebraMap A (Localization (M := A) (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl) :
          (a : A) → Localization (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl)
        ((↑z.den : A) * (↑y.num : A)) :
      Localization (M := A) (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl)
    ((algebraMap A (Localization (M := A) (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl) :
          (a : A) → Localization (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl)
        ((↑y.den : A) * (↑z.num : A)) :
      Localization (M := A) (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl)
obtain :
  ∀ (c : A) (hcx : c ∈ (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl)
    (hc :
      (↑(Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl) c
                hcx) :
            A) *
          ((↑z.den : A) * (↑y.num : A)) =
        (↑(Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl) c
                hcx) :
            A) *
          ((↑y.den : A) * (↑z.num : A))),
    ∃ (i : ℕ),
      ∃ c ∈ 𝒜 i,
        c ∉ (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal ∧
          c * ((↑z.den : A) * (↑y.num : A)) = c * ((↑y.den : A) * (↑z.num : A))
⊢ ∃ (i : ℕ),
    ∃ c ∈ 𝒜 i,
      c ∉ (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal ∧
        c * ((↑z.den : A) * (↑y.num : A)) = c * ((↑y.den : A) * (↑z.num : A))

Tactic:
obtain ⟨⟨c, hcx⟩, hc⟩ := IsLocalization.exists_of_eq (M := x.1.1.toIdeal.primeCompl) e

Premises used: IsLocalization.exists_of_eq
-- 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 : ↥(pbo f)
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
this : Algebra (A⁰_ f) (AtPrime 𝒜 (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal) :=
  RingHom.toAlgebra (mapId 𝒜 ⋯)
y z : NumDenSameDeg 𝒜 (Submonoid.powers f)
e :
  Eq (α := Localization (M := A) (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl)
    ((algebraMap A (Localization (M := A) (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl) :
          (a : A) → Localization (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl)
        ((↑z.den : A) * (↑y.num : A)) :
      Localization (M := A) (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl)
    ((algebraMap A (Localization (M := A) (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl) :
          (a : A) → Localization (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl)
        ((↑y.den : A) * (↑z.num : A)) :
      Localization (M := A) (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl)
c : A
hcx : c ∈ (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl
hc :
  (↑(Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl) c hcx) :
        A) *
      ((↑z.den : A) * (↑y.num : A)) =
    (↑(Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl) c
            hcx) :
        A) *
      ((↑y.den : A) * (↑z.num : A))
obtain :
  ∀ (i : ℕ)
    (hi :
      (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ℕ), ↥(𝒜 i)) c : ⨁ (i : ℕ), ↥(𝒜 i)) : (a : ℕ) → ↥(𝒜 a)) i) : A) ∉
        (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal),
    ∃ (i : ℕ),
      ∃ c ∈ 𝒜 i,
        c ∉ (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal ∧
          c * ((↑z.den : A) * (↑y.num : A)) = c * ((↑y.den : A) * (↑z.num : A))
⊢ ∃ (i : ℕ),
    ∃ c ∈ 𝒜 i,
      c ∉ (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal ∧
        c * ((↑z.den : A) * (↑y.num : A)) = c * ((↑y.den : A) * (↑z.num : A))

Tactic:
obtain ⟨i, hi⟩ := not_forall.mp ((x.1.1.isHomogeneous.mem_iff _).not.mp hcx)

Premises used: Iff.not, HomogeneousIdeal.isHomogeneous, Iff.mp, Subtype.val, Classical.not_forall, ProjectiveSpectrum.asHomogeneousIdeal, Ideal.IsHomogeneous.mem_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
x : ↥(pbo f)
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
this : Algebra (A⁰_ f) (AtPrime 𝒜 (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal) :=
  RingHom.toAlgebra (mapId 𝒜 ⋯)
y z : NumDenSameDeg 𝒜 (Submonoid.powers f)
e :
  Eq (α := Localization (M := A) (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl)
    ((algebraMap A (Localization (M := A) (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl) :
          (a : A) → Localization (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl)
        ((↑z.den : A) * (↑y.num : A)) :
      Localization (M := A) (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl)
    ((algebraMap A (Localization (M := A) (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl) :
          (a : A) → Localization (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl)
        ((↑y.den : A) * (↑z.num : A)) :
      Localization (M := A) (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl)
c : A
hcx : c ∈ (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl
hc :
  (↑(Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl) c hcx) :
        A) *
      ((↑z.den : A) * (↑y.num : A)) =
    (↑(Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl) c
            hcx) :
        A) *
      ((↑y.den : A) * (↑z.num : A))
i : ℕ
hi :
  (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ℕ), ↥(𝒜 i)) c : ⨁ (i : ℕ), ↥(𝒜 i)) : (a : ℕ) → ↥(𝒜 a)) i) : A) ∉
    (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal
⊢ ∃ (i : ℕ),
    ∃ c ∈ 𝒜 i,
      c ∉ (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal ∧
        c * ((↑z.den : A) * (↑y.num : A)) = c * ((↑y.den : A) * (↑z.num : A))

Tactic:
⟨i, _, (decompose 𝒜 c i).2, hi, ?_⟩

Premises used: And.intro, Exists.intro, DFunLike.coe, Subtype.property, DirectSum.decompose
-- 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 : ↥(pbo f)
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
this : Algebra (A⁰_ f) (AtPrime 𝒜 (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal) :=
  RingHom.toAlgebra (mapId 𝒜 ⋯)
y z : NumDenSameDeg 𝒜 (Submonoid.powers f)
e :
  Eq (α := Localization (M := A) (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl)
    ((algebraMap A (Localization (M := A) (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl) :
          (a : A) → Localization (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl)
        ((↑z.den : A) * (↑y.num : A)) :
      Localization (M := A) (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl)
    ((algebraMap A (Localization (M := A) (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl) :
          (a : A) → Localization (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl)
        ((↑y.den : A) * (↑z.num : A)) :
      Localization (M := A) (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl)
c : A
hcx : c ∈ (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl
hc :
  (↑(Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl) c hcx) :
        A) *
      ((↑z.den : A) * (↑y.num : A)) =
    (↑(Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl) c
            hcx) :
        A) *
      ((↑y.den : A) * (↑z.num : A))
i : ℕ
hi :
  (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ℕ), ↥(𝒜 i)) c : ⨁ (i : ℕ), ↥(𝒜 i)) : (a : ℕ) → ↥(𝒜 a)) i) : A) ∉
    (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal
refine :
  (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ℕ), ↥(𝒜 i)) c : ⨁ (i : ℕ), ↥(𝒜 i)) : (a : ℕ) → ↥(𝒜 a)) i) : A) *
      ((↑z.den : A) * (↑y.num : A)) =
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ℕ), ↥(𝒜 i)) c : ⨁ (i : ℕ), ↥(𝒜 i)) : (a : ℕ) → ↥(𝒜 a)) i) : A) *
      ((↑y.den : A) * (↑z.num : A))
⊢ ∃ (i : ℕ),
    ∃ c ∈ 𝒜 i,
      c ∉ (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal ∧
        c * ((↑z.den : A) * (↑y.num : A)) = c * ((↑y.den : A) * (↑z.num : A))

Tactic:
refine ⟨i, _, (decompose 𝒜 c i).2, hi, ?_⟩
-- 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 : ↥(pbo f)
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
this : Algebra (A⁰_ f) (AtPrime 𝒜 (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal) :=
  RingHom.toAlgebra (mapId 𝒜 ⋯)
y z : NumDenSameDeg 𝒜 (Submonoid.powers f)
e :
  Eq (α := Localization (M := A) (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl)
    ((algebraMap A (Localization (M := A) (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl) :
          (a : A) → Localization (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl)
        ((↑z.den : A) * (↑y.num : A)) :
      Localization (M := A) (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl)
    ((algebraMap A (Localization (M := A) (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl) :
          (a : A) → Localization (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl)
        ((↑y.den : A) * (↑z.num : A)) :
      Localization (M := A) (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl)
c : A
hcx : c ∈ (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl
hc :
  (↑(Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl) c hcx) :
        A) *
      ((↑z.den : A) * (↑y.num : A)) =
    (↑(Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl) c
            hcx) :
        A) *
      ((↑y.den : A) * (↑z.num : A))
i : ℕ
hi :
  (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ℕ), ↥(𝒜 i)) c : ⨁ (i : ℕ), ↥(𝒜 i)) : (a : ℕ) → ↥(𝒜 a)) i) : A) ∉
    (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal
⊢ (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ℕ), ↥(𝒜 i))
                ((↑(Subtype.mk (p := fun (x_1 : A) ↦
                        x_1 ∈ (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl) c hcx) :
                    A) *
                  ((↑z.den : A) * (↑y.num : A))) :
              ⨁ (i : ℕ), ↥(𝒜 i)) :
            (a : ℕ) → ↥(𝒜 a))
          (i + z.deg + y.deg)) :
      A) =
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ℕ), ↥(𝒜 i))
                ((↑(Subtype.mk (p := fun (x_1 : A) ↦
                        x_1 ∈ (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl) c hcx) :
                    A) *
                  ((↑y.den : A) * (↑z.num : A))) :
              ⨁ (i : ℕ), ↥(𝒜 i)) :
            (a : ℕ) → ↥(𝒜 a))
          (i + z.deg + y.deg)) :
      A)

Tactic:
apply_fun fun x ↦ (decompose 𝒜 x (i + z.deg + y.deg)).1 at hc

Premises used: HAdd.hAdd, Subtype.val, HomogeneousLocalization.NumDenSameDeg.deg, DFunLike.coe, DirectSum.decompose
-- 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 : ↥(pbo f)
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
this : Algebra (A⁰_ f) (AtPrime 𝒜 (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal) :=
  RingHom.toAlgebra (mapId 𝒜 ⋯)
y z : NumDenSameDeg 𝒜 (Submonoid.powers f)
e :
  Eq (α := Localization (M := A) (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl)
    ((algebraMap A (Localization (M := A) (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl) :
          (a : A) → Localization (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl)
        ((↑z.den : A) * (↑y.num : A)) :
      Localization (M := A) (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl)
    ((algebraMap A (Localization (M := A) (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl) :
          (a : A) → Localization (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl)
        ((↑y.den : A) * (↑z.num : A)) :
      Localization (M := A) (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl)
c : A
hcx : c ∈ (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl
i : ℕ
hi :
  (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ℕ), ↥(𝒜 i)) c : ⨁ (i : ℕ), ↥(𝒜 i)) : (a : ℕ) → ↥(𝒜 a)) i) : A) ∉
    (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal
hc :
  (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ℕ), ↥(𝒜 i))
                ((↑(Subtype.mk (p := fun (x_1 : A) ↦
                        x_1 ∈ (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl) c hcx) :
                    A) *
                  ((↑z.den : A) * (↑y.num : A))) :
              ⨁ (i : ℕ), ↥(𝒜 i)) :
            (a : ℕ) → ↥(𝒜 a))
          (i + z.deg + y.deg)) :
      A) =
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ℕ), ↥(𝒜 i))
                ((↑(Subtype.mk (p := fun (x_1 : A) ↦
                        x_1 ∈ (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl) c hcx) :
                    A) *
                  ((↑y.den : A) * (↑z.num : A))) :
              ⨁ (i : ℕ), ↥(𝒜 i)) :
            (a : ℕ) → ↥(𝒜 a))
          (i + z.deg + y.deg)) :
      A)
rw :
  (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ℕ), ↥(𝒜 i))
              ((↑(Subtype.mk (p := fun (x_1 : A) ↦
                      x_1 ∈ (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl) c hcx) :
                  A) *
                ((↑y.den : A) * (↑z.num : A))) :
            ⨁ (i : ℕ), ↥(𝒜 i)) :
          (a : ℕ) → ↥(𝒜 a))
        (i + y.deg + z.deg)) :
    A)
| (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ℕ), ↥(𝒜 i))
              ((↑(Subtype.mk (p := fun (x_1 : A) ↦
                      x_1 ∈ (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl) c hcx) :
                  A) *
                ((↑y.den : A) * (↑z.num : A))) :
            ⨁ (i : ℕ), ↥(𝒜 i)) :
          (a : ℕ) → ↥(𝒜 a))
        (i + z.deg + y.deg)) :
    A)

Tactic:
rw [add_right_comm]

Premises used: add_right_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
x : ↥(pbo f)
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
this : Algebra (A⁰_ f) (AtPrime 𝒜 (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal) :=
  RingHom.toAlgebra (mapId 𝒜 ⋯)
y z : NumDenSameDeg 𝒜 (Submonoid.powers f)
e :
  Eq (α := Localization (M := A) (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl)
    ((algebraMap A (Localization (M := A) (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl) :
          (a : A) → Localization (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl)
        ((↑z.den : A) * (↑y.num : A)) :
      Localization (M := A) (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl)
    ((algebraMap A (Localization (M := A) (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl) :
          (a : A) → Localization (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl)
        ((↑y.den : A) * (↑z.num : A)) :
      Localization (M := A) (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl)
c : A
hcx : c ∈ (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl
i : ℕ
hi :
  (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ℕ), ↥(𝒜 i)) c : ⨁ (i : ℕ), ↥(𝒜 i)) : (a : ℕ) → ↥(𝒜 a)) i) : A) ∉
    (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal
hc :
  (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ℕ), ↥(𝒜 i))
                ((↑(Subtype.mk (p := fun (x_1 : A) ↦
                        x_1 ∈ (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl) c hcx) :
                    A) *
                  ((↑z.den : A) * (↑y.num : A))) :
              ⨁ (i : ℕ), ↥(𝒜 i)) :
            (a : ℕ) → ↥(𝒜 a))
          (i + z.deg + y.deg)) :
      A) =
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ℕ), ↥(𝒜 i))
                ((↑(Subtype.mk (p := fun (x_1 : A) ↦
                        x_1 ∈ (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl) c hcx) :
                    A) *
                  ((↑y.den : A) * (↑z.num : A))) :
              ⨁ (i : ℕ), ↥(𝒜 i)) :
            (a : ℕ) → ↥(𝒜 a))
          (i + z.deg + y.deg)) :
      A)
⊢ (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ℕ), ↥(𝒜 i))
                ((↑(Subtype.mk (p := fun (x_1 : A) ↦
                        x_1 ∈ (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl) c hcx) :
                    A) *
                  ((↑z.den : A) * (↑y.num : A))) :
              ⨁ (i : ℕ), ↥(𝒜 i)) :
            (a : ℕ) → ↥(𝒜 a))
          (i + z.deg + y.deg)) :
      A) =
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ℕ), ↥(𝒜 i))
                ((↑(Subtype.mk (p := fun (x_1 : A) ↦
                        x_1 ∈ (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl) c hcx) :
                    A) *
                  ((↑y.den : A) * (↑z.num : A))) :
              ⨁ (i : ℕ), ↥(𝒜 i)) :
            (a : ℕ) → ↥(𝒜 a))
          (i + y.deg + z.deg)) :
      A)

Tactic:
conv_rhs at hc => rw [add_right_comm]

Premises used: add_right_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
x : ↥(pbo f)
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
this : Algebra (A⁰_ f) (AtPrime 𝒜 (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal) :=
  RingHom.toAlgebra (mapId 𝒜 ⋯)
y z : NumDenSameDeg 𝒜 (Submonoid.powers f)
e :
  Eq (α := Localization (M := A) (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl)
    ((algebraMap A (Localization (M := A) (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl) :
          (a : A) → Localization (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl)
        ((↑z.den : A) * (↑y.num : A)) :
      Localization (M := A) (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl)
    ((algebraMap A (Localization (M := A) (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl) :
          (a : A) → Localization (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl)
        ((↑y.den : A) * (↑z.num : A)) :
      Localization (M := A) (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl)
c : A
hcx : c ∈ (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl
i : ℕ
hi :
  (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ℕ), ↥(𝒜 i)) c : ⨁ (i : ℕ), ↥(𝒜 i)) : (a : ℕ) → ↥(𝒜 a)) i) : A) ∉
    (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal
hc :
  (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ℕ), ↥(𝒜 i))
                    (↑(Subtype.mk (p := fun (x_1 : A) ↦
                          x_1 ∈ (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl) c hcx) :
                      A) :
                  ⨁ (i : ℕ), ↥(𝒜 i)) :
                (a : ℕ) → ↥(𝒜 a))
              i) :
          A) *
        (↑z.den : A) *
      (↑y.num : A) =
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ℕ), ↥(𝒜 i))
                  ((↑(Subtype.mk (p := fun (x_1 : A) ↦
                          x_1 ∈ (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl) c hcx) :
                      A) *
                    (↑y.den : A)) :
                ⨁ (i : ℕ), ↥(𝒜 i)) :
              (a : ℕ) → ↥(𝒜 a))
            (i + y.deg)) :
        A) *
      (↑z.num : A)
⊢ (↑y.den : A) ∈ 𝒜 y.deg

Tactic:
y.den.2

Premises used: HomogeneousLocalization.NumDenSameDeg.den, Subtype.property