awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme (goal)
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 𝒜 ⋯)
i : ℕ
a : ↥(𝒜 i)
b : A
hb : b ∈ 𝒜 i
hb' : b ∉ (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal
⊢ 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)
        (f ^ i * ((↑a : A) * b ^ m)) :
      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)
        (b * f ^ i * ((↑a : A) * b ^ (m - 1))) :
      Localization (M := A) (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl)
have toIsLocalizationMap : 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)
      (f ^ i * ((↑a : A) * b ^ m)) :
    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)
      (f ^ i * b * ((↑a : A) * b ^ (m - 1))) :
    Localization (M := A) (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl)
Tactic: rw [mul_comm b, mul_mul_mul_comm, ← pow_succ', mul_assoc, tsub_add_cancel_of_le (by lia)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme (goal)
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 𝒜 ⋯)
i : ℕ
a : ↥(𝒜 i)
b : A
hb : b ∈ 𝒜 i
hb' : b ∉ (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal
toIsLocalizationMap :
  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)
        (f ^ i * ((↑a : A) * b ^ m)) :
      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)
        (f ^ i * b * ((↑a : A) * b ^ (m - 1))) :
      Localization (M := A) (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl)
⊢ 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)
        (f ^ i * ((↑a : A) * b ^ m)) :
      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)
        (b * f ^ i * ((↑a : A) * b ^ (m - 1))) :
      Localization (M := A) (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl)
have toIsLocalizationMap₁ : 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)
      (f ^ i * ((↑a : A) * b ^ m)) :
    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)
      (f ^ i * (↑a : A) * (b * b ^ (m - 1))) :
    Localization (M := A) (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl)
Tactic: rw [mul_comm b, mul_mul_mul_comm, ← pow_succ', mul_assoc, tsub_add_cancel_of_le (by lia)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme (hypothesis)
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 (α := 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 ∈ 𝒜 i,
      c ∉ (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal ∧
        c * ((↑z.den : A) * (↑y.num : A)) = c * ((↑y.den : A) * (↑z.num : A))
have 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)))
Tactic: apply_fun HomogeneousLocalization.val at e
Cleared hypotheses: e
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme (hypothesis)
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)))
⊢ ∃ (i : ℕ),
    ∃ c ∈ 𝒜 i,
      c ∉ (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal ∧
        c * ((↑z.den : A) * (↑y.num : A)) = c * ((↑y.den : A) * (↑z.num : A))
have 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)
Tactic: simp only [RingHom.algebraMap_toAlgebra, map_mk, GradedRingHom.id_apply, val_mk, mk_eq_mk',
        IsLocalization.mk'_eq_iff_eq] at e
Cleared hypotheses: e
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme (goal)
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)
⊢ ∃ (i : ℕ),
    ∃ c ∈ 𝒜 i,
      c ∉ (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal ∧
        c * ((↑z.den : A) * (↑y.num : A)) = c * ((↑y.den : A) * (↑z.num : A))
have 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))
Tactic: obtain ⟨⟨c, hcx⟩, hc⟩ := IsLocalization.exists_of_eq (M := x.1.1.toIdeal.primeCompl) e
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme (goal)
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 : ℕ),
    ∃ c ∈ 𝒜 i,
      c ∉ (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal ∧
        c * ((↑z.den : A) * (↑y.num : A)) = c * ((↑y.den : A) * (↑z.num : A))
have 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))
Tactic: obtain ⟨i, hi⟩ := not_forall.mp ((x.1.1.isHomogeneous.mem_iff _).not.mp hcx)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme (goal)
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))
have 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))
Tactic: refine ⟨i, _, (decompose 𝒜 c i).2, hi, ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme (hypothesis)
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)) 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))
have 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)
Tactic: apply_fun fun x ↦ (decompose 𝒜 x (i + z.deg + y.deg)).1 at hc
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme (goal)
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) *
                ((↑y.den : A) * (↑z.num : A))) :
            ⨁ (i : ℕ), ↥(𝒜 i)) :
          (a : ℕ) → ↥(𝒜 a))
        (i + z.deg + y.deg)) :
    A)
have 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)
Tactic: rw [add_right_comm]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme (goal)
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))
⊢ 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))
have toIsLocalizationMap : (↑z.den : A) * (c ^ m * (↑y.num : A)) = (↑y.den : A) * (c ^ m * (↑z.num : A))
Tactic: congr 2