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)
    ((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) *
                  (↑z.num : A)) :
              ⨁ (i : ℕ), ↥(𝒜 i)) :
            (a : ℕ) → ↥(𝒜 a))
          (i + y.deg + z.deg)) :
      A)
⊢ (↑z.num : A) ∈ 𝒜 z.deg

Tactic:
z.num.2

Premises used: HomogeneousLocalization.NumDenSameDeg.num, 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 : ↥(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)) :
                ⨁ (i : ℕ), ↥(𝒜 i)) :
              (a : ℕ) → ↥(𝒜 a))
            (i + z.deg)) :
        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) * (↑z.num : A))) :
              ⨁ (i : ℕ), ↥(𝒜 i)) :
            (a : ℕ) → ↥(𝒜 a))
          (i + y.deg + z.deg)) :
      A)
⊢ (↑z.den : A) ∈ 𝒜 z.deg

Tactic:
z.den.2

Premises used: HomogeneousLocalization.NumDenSameDeg.den, 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 : ↥(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 + y.deg + z.deg)) :
      A)
⊢ (↑y.num : A) ∈ 𝒜 y.deg

Tactic:
y.num.2

Premises used: HomogeneousLocalization.NumDenSameDeg.num, 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 : ↥(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:
exacts [y.den.2, z.num.2, z.den.2, y.num.2]

Premises used: HomogeneousLocalization.NumDenSameDeg.num, HomogeneousLocalization.NumDenSameDeg.den, 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 : ↥(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_1 :
  Eq (α := AtPrime 𝒜 (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal)
    ((algebraMap (A⁰_ f) (AtPrime 𝒜 (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal) :
          (a : A⁰_ f) → AtPrime 𝒜 (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal)
        (HomogeneousLocalization.mk y) :
      AtPrime 𝒜 (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal)
    ((algebraMap (A⁰_ f) (AtPrime 𝒜 (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal) :
          (a : A⁰_ f) → AtPrime 𝒜 (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal)
        (HomogeneousLocalization.mk z) :
      AtPrime 𝒜 (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal)
i : ℕ
c : A
hc : c ∈ 𝒜 i
hc' : c ∉ (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal
e : c * ((↑z.den : A) * (↑y.num : A)) = c * ((↑y.den : A) * (↑z.num : A))
⊢ ∃ (c :
    ↥(Ideal.primeCompl
        (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))
                (PresheafedSpace.Hom.base (LocallyRingedSpace.Hom.toHom (toSpec 𝒜 f))) :
              (a : (↑(↑(Proj.restrict ⋯).toPresheafedSpace : TopCat) : Type u_1)) →
                (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1))
            x)))),
    (↑c : A⁰_ f) * HomogeneousLocalization.mk y = (↑c : A⁰_ f) * HomogeneousLocalization.mk z

Tactic:
⟨⟨HomogeneousLocalization.mk ⟨m * i, ⟨c ^ m, SetLike.pow_mem_graded _ hc⟩,
      ⟨f ^ i, mul_comm m i ▸ SetLike.pow_mem_graded _ f_deg⟩, ⟨_, rfl⟩⟩,
      (mk_mem_toSpec_base_apply _ _ _).not.mpr <| x.1.1.toIdeal.primeCompl.pow_mem hc' _⟩,
      val_injective _ ?_⟩

Premises used: Iff.mpr, HMul.hMul, Submonoid.pow_mem, HomogeneousLocalization.val_injective, Eq.rec, Iff.not, Subtype.mk, AlgebraicGeometry.ProjectiveSpectrum.Proj.mk_mem_toSpec_base_apply, HPow.hPow, HomogeneousLocalization.NumDenSameDeg.mk, SetLike.pow_mem_graded, Exists.intro, HomogeneousLocalization.mk, mul_comm, Ideal.primeCompl, Eq.symm, Subtype.val, HomogeneousIdeal.toIdeal, ProjectiveSpectrum.asHomogeneousIdeal, 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 : ↥(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_1 :
  Eq (α := AtPrime 𝒜 (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal)
    ((algebraMap (A⁰_ f) (AtPrime 𝒜 (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal) :
          (a : A⁰_ f) → AtPrime 𝒜 (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal)
        (HomogeneousLocalization.mk y) :
      AtPrime 𝒜 (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal)
    ((algebraMap (A⁰_ f) (AtPrime 𝒜 (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal) :
          (a : A⁰_ f) → AtPrime 𝒜 (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal)
        (HomogeneousLocalization.mk z) :
      AtPrime 𝒜 (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal)
i : ℕ
c : A
hc : c ∈ 𝒜 i
hc' : c ∉ (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal
e : c * ((↑z.den : A) * (↑y.num : A)) = c * ((↑y.den : A) * (↑z.num : A))
toIsLocalizationMap : (↑z.den : A) * (c ^ m * (↑y.num : A)) = (↑y.den : A) * (c ^ m * (↑z.num : A))
⊢ Eq (α := Localization (Submonoid.powers f))
    ((algebraMap A (Localization (Submonoid.powers f)) : (a : A) → Localization (Submonoid.powers f))
        (f ^ i * ((↑z.den : A) * (c ^ m * (↑y.num : A)))) :
      Localization (Submonoid.powers f))
    ((algebraMap A (Localization (Submonoid.powers f)) : (a : A) → Localization (Submonoid.powers f))
        (f ^ i * ((↑y.den : A) * (c ^ m * (↑z.num : A)))) :
      Localization (Submonoid.powers f))

Tactic:
congr 2
-- 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_1 :
  Eq (α := AtPrime 𝒜 (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal)
    ((algebraMap (A⁰_ f) (AtPrime 𝒜 (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal) :
          (a : A⁰_ f) → AtPrime 𝒜 (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal)
        (HomogeneousLocalization.mk y) :
      AtPrime 𝒜 (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal)
    ((algebraMap (A⁰_ f) (AtPrime 𝒜 (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal) :
          (a : A⁰_ f) → AtPrime 𝒜 (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal)
        (HomogeneousLocalization.mk z) :
      AtPrime 𝒜 (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal)
i : ℕ
c : A
hc : c ∈ 𝒜 i
hc' : c ∉ (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal
e : c * ((↑z.den : A) * (↑y.num : A)) = c * ((↑y.den : A) * (↑z.num : A))
toIsLocalizationMap : c ^ m * ((↑z.den : A) * (↑y.num : A)) = (↑y.den : A) * (c ^ m * (↑z.num : A))
toIsLocalizationMap₁ : c ^ m * ((↑z.den : A) * (↑y.num : A)) = c ^ m * ((↑y.den : A) * (↑z.num : A))
toIsLocalizationMap₂ : c ^ (m - 1 + 1) * ((↑z.den : A) * (↑y.num : A)) = c ^ (m - 1 + 1) * ((↑y.den : A) * (↑z.num : A))
toIsLocalizationMap₃ : c ^ (m - 1) * c * ((↑z.den : A) * (↑y.num : A)) = c ^ (m - 1) * c * ((↑y.den : A) * (↑z.num : A))
toIsLocalizationMap₄ :
  c ^ (m - 1) * (c * ((↑z.den : A) * (↑y.num : A))) = c ^ (m - 1) * c * ((↑y.den : A) * (↑z.num : A))
toIsLocalizationMap₅ :
  c ^ (m - 1) * (c * ((↑z.den : A) * (↑y.num : A))) = c ^ (m - 1) * (c * ((↑y.den : A) * (↑z.num : A)))
toIsLocalizationMap₆ toIsLocalizationMap₇ :
  c ^ (m - 1) * (c * ((↑y.den : A) * (↑z.num : A))) = c ^ (m - 1) * (c * ((↑y.den : A) * (↑z.num : A)))
⊢ (↑z.den : A) * (c ^ m * (↑y.num : A)) = (↑y.den : A) * (c ^ m * (↑z.num : A))

Tactic:
rw [mul_left_comm, mul_left_comm y.den.1, ← tsub_add_cancel_of_le (show 1 ≤ m from hm),
      pow_succ, mul_assoc, mul_assoc, e]

Premises used: pow_succ, mul_assoc, tsub_add_cancel_of_le, mul_left_comm, HomogeneousLocalization.NumDenSameDeg.den, 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
x : ↥(pbo f)
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
⊢ Eq (α := CommRingCat.of (A⁰_ f) ⟶ CommRingCat.of (AtPrime 𝒜 (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal))
    (StructureSheaf.toStalk (A⁰_ f)
        ((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))
              (PresheafedSpace.Hom.base (LocallyRingedSpace.Hom.toHom (toSpec 𝒜 f))) :
            (a : (↑(↑(Proj.restrict ⋯).toPresheafedSpace : TopCat) : Type u_1)) →
              (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1))
          x) ≫
      Iso.hom (specStalkEquiv 𝒜 f x f_deg hm))
    (CommRingCat.ofHom (mapId 𝒜 ⋯))

Tactic:
letI : Algebra (Away 𝒜 f) (AtPrime 𝒜 x.1.asHomogeneousIdeal.toIdeal) :=
    (mapId 𝒜 (Submonoid.powers_le.mpr x.2)).toAlgebra
  letI := isLocalization_atPrime 𝒜 f x f_deg hm
  CommRingCat.hom_ext (IsLocalization.algEquiv
    (R := A⁰_ f)
    (M := ((toSpec 𝒜 f).base x).asIdeal.primeCompl)
    (S := (Spec.structureSheaf (A⁰_ f)).presheaf.stalk ((toSpec 𝒜 f).base x))
    (Q := AtPrime 𝒜 x.1.asHomogeneousIdeal.toIdeal)).toAlgHom.comp_algebraMap

Premises used: AlgHom.comp_algebraMap, CommRingCat.hom_ext, CommRingCat.carrier, AlgEquiv.toAlgHom, CategoryTheory.ConcreteCategory.hom, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, TopCat.Presheaf.stalk, IsLocalization.algEquiv, AlgebraicGeometry.PresheafedSpace.Hom.base, AlgebraicGeometry.Spec.structureSheaf, Ideal.primeCompl, TopCat.Sheaf.presheaf, Subtype.val, HomogeneousIdeal.toIdeal, DFunLike.coe, PrimeSpectrum.asIdeal, AlgebraicGeometry.ProjectiveSpectrum.Proj.toSpec, ProjectiveSpectrum.asHomogeneousIdeal, HomogeneousLocalization.Away, HomogeneousLocalization.AtPrime
-- 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
⊢ Eq (α :=
    (Spec A⁰_ f).presheaf.stalk
        ((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))
              (PresheafedSpace.Hom.base (LocallyRingedSpace.Hom.toHom (toSpec 𝒜 f))) :
            (a : (↑(↑(Proj.restrict ⋯).toPresheafedSpace : TopCat) : Type u_1)) →
              (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1))
          x) ⟶
      (Proj.restrict (U := Functor.obj (C := Opens (↑Proj.T : Type u_1)) (Opens.toTopCat Proj.T) (pbo f))
              ⋯).presheaf.stalk
        x)
    (LocallyRingedSpace.Hom.stalkMap (toSpec 𝒜 f) x)
    (Iso.hom (specStalkEquiv 𝒜 f x f_deg hm) ≫
      Iso.inv (RingEquiv.toCommRingCatIso («Proj».stalkIso' 𝒜 (↑x : ProjectiveSpectrum 𝒜))) ≫
        Iso.inv (Proj.restrictStalkIso ⋯ x))

Tactic:
CommRingCat.hom_ext <|
    IsLocalization.ringHom_ext (R := A⁰_ f) ((toSpec 𝒜 f).base x).asIdeal.primeCompl
      (S := (Spec.structureSheaf (A⁰_ f)).presheaf.stalk ((toSpec 𝒜 f).base x)) <| ?_

Premises used: CommRingCat.hom_ext, CategoryTheory.ConcreteCategory.hom, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.PresheafedSpace.Hom.base, Ideal.primeCompl, DFunLike.coe, PrimeSpectrum.asIdeal, AlgebraicGeometry.ProjectiveSpectrum.Proj.toSpec, IsLocalization.ringHom_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
⊢ IsIso (X :=
    (↑(Proj.restrict (U := Functor.obj (C := Opens (↑Proj.T : Type u_1)) (Opens.toTopCat Proj.T) (pbo f))
            ⋯).toPresheafedSpace :
      TopCat))
    (PresheafedSpace.Hom.base (LocallyRingedSpace.Hom.toHom (toSpec 𝒜 f)))

Tactic:
haveI : IsIso (toSpec 𝒜 f).base := toSpec_base_isIso 𝒜 f_deg hm
-- 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
this :
  IsIso (X :=
    (↑(Proj.restrict (U := Functor.obj (C := Opens (↑Proj.T : Type u_1)) (Opens.toTopCat Proj.T) (pbo f))
            ⋯).toPresheafedSpace :
      TopCat))
    (PresheafedSpace.Hom.base (LocallyRingedSpace.Hom.toHom (toSpec 𝒜 f)))
x :
  (↑(Proj.restrict (U := Functor.obj (C := Opens (↑Proj.T : Type u_1)) (Opens.toTopCat Proj.T) (pbo f)) ⋯).toTopCat :
    Type u_1)
rw :
  IsIso (X :=
    (Spec A⁰_ f).presheaf.stalk
      ((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))
            (PresheafedSpace.Hom.base (LocallyRingedSpace.Hom.toHom (toSpec 𝒜 f))) :
          (a : (↑(↑(Proj.restrict ⋯).toPresheafedSpace : TopCat) : Type u_1)) →
            (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1))
        x))
    (Y :=
    (Proj.restrict (U := Functor.obj (C := Opens (↑Proj.T : Type u_1)) (Opens.toTopCat Proj.T) (pbo f))
            ⋯).presheaf.stalk
      x)
    (Iso.hom (specStalkEquiv 𝒜 f x f_deg hm) ≫
      Iso.inv (RingEquiv.toCommRingCatIso («Proj».stalkIso' 𝒜 (↑x : ProjectiveSpectrum 𝒜))) ≫
        Iso.inv (Proj.restrictStalkIso ⋯ x))
⊢ IsIso (X :=
    (Spec A⁰_ f).presheaf.stalk
      ((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))
            (PresheafedSpace.Hom.base (LocallyRingedSpace.Hom.toHom (toSpec 𝒜 f))) :
          (a : (↑(↑(Proj.restrict ⋯).toPresheafedSpace : TopCat) : Type u_1)) →
            (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1))
        x))
    (LocallyRingedSpace.Hom.stalkMap (toSpec 𝒜 f) x)

Tactic:
rw [stalkMap_toSpec 𝒜 f x f_deg hm]

Premises used: AlgebraicGeometry.ProjectiveSpectrum.Proj.stalkMap_toSpec