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)
a : A
n : ℕ
hn : a ∈ 𝒜 (n * m)
rw : f ^ n ∈ 𝒜 (n * m)
⊢ f ^ n ∈ 𝒜 (m * n)

Tactic:
rw [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
q : (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1)
a : A
n : ℕ
hn : a ∈ 𝒜 (n * m)
⊢ f ^ n ∈ 𝒜 (n * m)

Tactic:
mem_tac
-- 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)
a : A
n : ℕ
hn : a ∈ 𝒜 (n * m)
rw :
  (HPow.hPow (α := A⁰_ f)
        (HomogeneousLocalization.mk
          { deg := m * n, num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * n)) a ⋯,
            den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * n)) (f ^ n) ⋯, den_mem := ⋯ :
            NumDenSameDeg 𝒜 (Submonoid.powers f) })
        m ∈
      q.asIdeal) =
    (HomogeneousLocalization.mk
        { deg := m * (n * m), num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * (n * m))) (a ^ m) ⋯,
          den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * (n * m))) (f ^ (n * m)) ⋯, den_mem := ⋯ } ∈
      q.asIdeal)
⊢ a ∈ carrier f_deg q ↔
    HomogeneousLocalization.mk
        { deg := m * n, num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * n)) a ⋯,
          den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * n)) (f ^ n) ⋯, den_mem := ⋯ } ∈
      q.asIdeal

Tactic:
rw [mem_carrier_iff_of_mem f_deg hm q a hn, iff_iff_eq, eq_comm,
    ← Ideal.IsPrime.pow_mem_iff_mem (α := A⁰_ f) inferInstance m hm]

Premises used: Ideal.IsPrime.pow_mem_iff_mem, iff_iff_eq, inferInstance, eq_comm, AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.mem_carrier_iff_of_mem
-- 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)
a : A
n : ℕ
hn : a ∈ 𝒜 (n * m)
e_a :
  HPow.hPow (α := A⁰_ f)
      (HomogeneousLocalization.mk
        { deg := m * n, num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * n)) a ⋯,
          den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * n)) (f ^ n) ⋯, den_mem := ⋯ :
          NumDenSameDeg 𝒜 (Submonoid.powers f) })
      m =
    HomogeneousLocalization.mk
      { deg := m * (n * m), num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * (n * m))) (a ^ m) ⋯,
        den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * (n * m))) (f ^ (n * m)) ⋯, den_mem := ⋯ }
⊢ (HPow.hPow (α := A⁰_ f)
        (HomogeneousLocalization.mk
          { deg := m * n, num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * n)) a ⋯,
            den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * n)) (f ^ n) ⋯, den_mem := ⋯ :
            NumDenSameDeg 𝒜 (Submonoid.powers f) })
        m ∈
      q.asIdeal) =
    (HomogeneousLocalization.mk
        { deg := m * (n * m), num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * (n * m))) (a ^ m) ⋯,
          den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * (n * m))) (f ^ (n * m)) ⋯, den_mem := ⋯ } ∈
      q.asIdeal)

Tactic:
congr 1
-- 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)
a : A
n : ℕ
hn : a ∈ 𝒜 (n * m)
e_a :
  HomogeneousLocalization.val
      (HPow.hPow (α := A⁰_ f)
        (HomogeneousLocalization.mk
          { deg := m * n, num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * n)) a ⋯,
            den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * n)) (f ^ n) ⋯, den_mem := ⋯ :
            NumDenSameDeg 𝒜 (Submonoid.powers f) })
        m) =
    HomogeneousLocalization.val
      (HomogeneousLocalization.mk
        { deg := m * (n * m), num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * (n * m))) (a ^ m) ⋯,
          den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * (n * m))) (f ^ (n * m)) ⋯, den_mem := ⋯ :
          NumDenSameDeg 𝒜 (Submonoid.powers f) })
⊢ HPow.hPow (α := A⁰_ f)
      (HomogeneousLocalization.mk
        { deg := m * n, num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * n)) a ⋯,
          den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * n)) (f ^ n) ⋯, den_mem := ⋯ :
          NumDenSameDeg 𝒜 (Submonoid.powers f) })
      m =
    HomogeneousLocalization.mk
      { deg := m * (n * m), num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * (n * m))) (a ^ m) ⋯,
        den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * (n * m))) (f ^ (n * m)) ⋯, den_mem := ⋯ }

Tactic:
apply HomogeneousLocalization.val_injective

Premises used: HomogeneousLocalization.val_injective
-- 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)
a : A
n : ℕ
hn : a ∈ 𝒜 (n * m)
e_a :
  Eq (α := Localization (Submonoid.powers f))
    (Localization.mk (a ^ m)
      (HPow.hPow (α := ↥(Submonoid.powers f))
        (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers f) x) (f ^ n) ⋯) m))
    (Localization.mk (a ^ m)
      (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers f) x) ((f ^ n) ^ m) ⋯))
⊢ HomogeneousLocalization.val
      (HPow.hPow (α := A⁰_ f)
        (HomogeneousLocalization.mk
          { deg := m * n, num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * n)) a ⋯,
            den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * n)) (f ^ n) ⋯, den_mem := ⋯ :
            NumDenSameDeg 𝒜 (Submonoid.powers f) })
        m) =
    HomogeneousLocalization.val
      (HomogeneousLocalization.mk
        { deg := m * (n * m), num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * (n * m))) (a ^ m) ⋯,
          den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * (n * m))) (f ^ (n * m)) ⋯, den_mem := ⋯ :
          NumDenSameDeg 𝒜 (Submonoid.powers f) })

Tactic:
simp only [HomogeneousLocalization.val_mk, HomogeneousLocalization.val_pow,
    Localization.mk_pow, pow_mul]

Premises used: HomogeneousLocalization.val_pow, HomogeneousLocalization.val_mk, pow_mul, Localization.mk_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)
a : A
n : ℕ
hn : a ∈ 𝒜 (n * m)
⊢ Eq (α := Localization (Submonoid.powers f))
    (Localization.mk (a ^ m)
      (HPow.hPow (α := ↥(Submonoid.powers f))
        (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers f) x) (f ^ n) ⋯) m))
    (Localization.mk (a ^ m)
      (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers f) x) ((f ^ n) ^ m) ⋯))

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
q : (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1)
z : NumDenSameDeg 𝒜 (Submonoid.powers f)
obtain :
  ∀ (n : ℕ) (hn : f ^ n = (↑z.den : A)), (↑z.num : A) ∈ carrier f_deg q ↔ HomogeneousLocalization.mk z ∈ q.asIdeal
⊢ (↑z.num : A) ∈ carrier f_deg q ↔ HomogeneousLocalization.mk z ∈ q.asIdeal

Tactic:
obtain ⟨n, hn : f ^ n = _⟩ := z.den_mem

Premises used: HomogeneousLocalization.NumDenSameDeg.den_mem
-- 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)
z : NumDenSameDeg 𝒜 (Submonoid.powers f)
n : ℕ
hn : f ^ n = (↑z.den : A)
e : f ^ n = 0
⊢ Subsingleton.{max (u_1 + 1) 1} (HomogeneousLocalization 𝒜 (Submonoid.powers f))

Tactic:
have := HomogeneousLocalization.subsingleton 𝒜 (x := .powers f) ⟨n, e⟩
-- 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)
z : NumDenSameDeg 𝒜 (Submonoid.powers f)
n : ℕ
hn : f ^ n = (↑z.den : A)
e : f ^ n = 0
this : Subsingleton.{max (u_1 + 1) 1} (HomogeneousLocalization 𝒜 (Submonoid.powers f))
⊢ False

Tactic:
IsEmpty.elim (inferInstanceAs (IsEmpty (PrimeSpectrum (A⁰_ f)))) q

Premises used: IsEmpty.elim
-- 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)
z : NumDenSameDeg 𝒜 (Submonoid.powers f)
n : ℕ
hn : f ^ n = (↑z.den : A)
e : f ^ n = 0
this : Subsingleton.{max (u_1 + 1) 1} (HomogeneousLocalization 𝒜 (Submonoid.powers f))
⊢ False

Tactic:
exact IsEmpty.elim (inferInstanceAs (IsEmpty (PrimeSpectrum (A⁰_ f)))) q
-- 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)
z : NumDenSameDeg 𝒜 (Submonoid.powers f)
n : ℕ
hn : f ^ n = (↑z.den : A)
⊢ f ^ n ≠ 0

Tactic:
have : f ^ n ≠ 0 := fun e ↦ by
    have := HomogeneousLocalization.subsingleton 𝒜 (x := .powers f) ⟨n, e⟩
    exact IsEmpty.elim (inferInstanceAs (IsEmpty (PrimeSpectrum (A⁰_ f)))) q
-- 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)
z : NumDenSameDeg 𝒜 (Submonoid.powers f)
n : ℕ
hn : f ^ n = (↑z.den : A)
this : f ^ n ≠ 0
⊢ (↑z.num : A) ∈ carrier f_deg q ↔
    HomogeneousLocalization.mk
        { deg := m * n, num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * n)) (↑z.num : A) ⋯,
          den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * n)) (f ^ n) ⋯, den_mem := ⋯ } ∈
      q.asIdeal

Tactic:
mem_carrier_iff_of_mem_mul f_deg hm q z.num.1 (n := n) ?_

Premises used: HomogeneousLocalization.NumDenSameDeg.num, AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.mem_carrier_iff_of_mem_mul, Subtype.val
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
q : (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1)
z : NumDenSameDeg 𝒜 (Submonoid.powers f)
n : ℕ
hn : f ^ n = (↑z.den : A)
this : f ^ n ≠ 0
h :
  HomogeneousLocalization.mk z =
    HomogeneousLocalization.mk
      { deg := m * n, num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * n)) (↑z.num : A) ⋯,
        den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * n)) (f ^ n) ⋯, den_mem := ⋯ }
convert! : (↑z.num : A) ∈ 𝒜 (n * m)
⊢ (↑z.num : A) ∈ carrier f_deg q ↔ HomogeneousLocalization.mk z ∈ q.asIdeal

Tactic:
convert! mem_carrier_iff_of_mem_mul f_deg hm q z.num.1 (n := n) ?_ using 2

Premises used: HomogeneousLocalization.NumDenSameDeg.num, AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.mem_carrier_iff_of_mem_mul, Subtype.val
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
q : (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1)
z : NumDenSameDeg 𝒜 (Submonoid.powers f)
n : ℕ
hn : f ^ n = (↑z.den : A)
this : f ^ n ≠ 0
h :
  (HomogeneousLocalization.mk z).val =
    HomogeneousLocalization.val
      (HomogeneousLocalization.mk
        { deg := m * n, num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * n)) (↑z.num : A) ⋯,
          den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * n)) (f ^ n) ⋯, den_mem := ⋯ :
          NumDenSameDeg 𝒜 (Submonoid.powers f) })
⊢ HomogeneousLocalization.mk z =
    HomogeneousLocalization.mk
      { deg := m * n, num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * n)) (↑z.num : A) ⋯,
        den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * n)) (f ^ n) ⋯, den_mem := ⋯ }

Tactic:
apply HomogeneousLocalization.val_injective

Premises used: HomogeneousLocalization.val_injective
-- 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)
z : NumDenSameDeg 𝒜 (Submonoid.powers f)
n : ℕ
hn : f ^ n = (↑z.den : A)
this : f ^ n ≠ 0
⊢ (HomogeneousLocalization.mk z).val =
    HomogeneousLocalization.val
      (HomogeneousLocalization.mk
        { deg := m * n, num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * n)) (↑z.num : A) ⋯,
          den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * n)) (f ^ n) ⋯, den_mem := ⋯ :
          NumDenSameDeg 𝒜 (Submonoid.powers f) })

Tactic:
simp only [hn, HomogeneousLocalization.val_mk]

Premises used: HomogeneousLocalization.val_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)
z : NumDenSameDeg 𝒜 (Submonoid.powers f)
n : ℕ
hn : f ^ n = (↑z.den : A)
this : f ^ n ≠ 0
⊢ n • m = z.deg

Tactic:
have := degree_eq_of_mem_mem 𝒜 (SetLike.pow_mem_graded n f_deg) (hn.symm ▸ z.den.2) this
-- 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)
z : NumDenSameDeg 𝒜 (Submonoid.powers f)
n : ℕ
hn : f ^ n = (↑z.den : A)
this_1 : f ^ n ≠ 0
this : n • m = z.deg
rw : (↑z.num : A) ∈ 𝒜 z.deg
⊢ (↑z.num : A) ∈ 𝒜 (n * m)

Tactic:
rw [← smul_eq_mul, this]

Premises used: smul_eq_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)
z : NumDenSameDeg 𝒜 (Submonoid.powers f)
n : ℕ
hn : f ^ n = (↑z.den : A)
this_1 : f ^ n ≠ 0
this : n • m = z.deg
⊢ (↑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
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
q : (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1)
z : NumDenSameDeg 𝒜 (Submonoid.powers f)
n : ℕ
hn : f ^ n = (↑z.den : A)
this_1 : f ^ n ≠ 0
this : n • m = z.deg
⊢ (↑z.num : A) ∈ 𝒜 z.deg

Tactic:
exact 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
m : ℕ
f_deg : f ∈ 𝒜 m
q : (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1)
a b : A
ha : a ∈ carrier f_deg q
hb : b ∈ carrier f_deg q
⊢ a + b ∈ carrier f_deg q

Tactic:
fun i => (q.2.mem_or_mem ?_).elim id id

Premises used: PrimeSpectrum.isPrime, Set.Mem, setOf, AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier, id, Ideal.IsPrime.mem_or_mem, Or.elim
-- 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
q : (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1)
a b : A
ha : a ∈ carrier f_deg q
hb : b ∈ carrier f_deg q
refine :
  ∀ (i : ℕ),
    HMul.hMul (α := (↑(CommRingCat.of (A⁰_ f)) : Type u_1))
        (HomogeneousLocalization.mk
          { deg := m * i,
            num :=
              Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i))
                (HPow.hPow (α := A) ((proj 𝒜 i : (a : A) → A) (a + b) : A) m) ⋯,
            den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i)) (f ^ i) ⋯, den_mem := ⋯ :
            NumDenSameDeg 𝒜 (Submonoid.powers f) })
        (HomogeneousLocalization.mk
          { deg := m * i,
            num :=
              Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i))
                (HPow.hPow (α := A) ((proj 𝒜 i : (a : A) → A) (a + b) : A) m) ⋯,
            den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i)) (f ^ i) ⋯, den_mem := ⋯ :
            NumDenSameDeg 𝒜 (Submonoid.powers f) }) ∈
      q.asIdeal
⊢ a + b ∈ carrier f_deg q

Tactic:
refine fun i => (q.2.mem_or_mem ?_).elim id id

Premises used: PrimeSpectrum.isPrime, id, Ideal.IsPrime.mem_or_mem, Or.elim
-- 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
q : (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1)
a b : A
ha : a ∈ carrier f_deg q
hb : b ∈ carrier f_deg q
i : ℕ
simp_rw :
  HomogeneousLocalization.mk
      { deg := m * i + m * i,
        num :=
          (Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i + m * i))
              (∑ x ∈ range (m + m + 1),
                (m + m).choose x •
                  (HPow.hPow (α := A) ((proj 𝒜 i : (a : A) → A) a : A) x *
                    HPow.hPow (α := A) ((proj 𝒜 i : (a : A) → A) b : A) (m + m - x)))
              ⋯ :
            ↥(𝒜 (m * i + m * i))),
        den := (Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i + m * i)) (f ^ (i + i)) ⋯ : ↥(𝒜 (m * i + m * i))),
        den_mem := ⋯ } ∈
    q.asIdeal
⊢ HomogeneousLocalization.mk
      { deg := m * i + m * i,
        num :=
          Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i + m * i))
            (HPow.hPow (α := A) ((proj 𝒜 i : (a : A) → A) (a + b) : A) m *
              HPow.hPow (α := A) ((proj 𝒜 i : (a : A) → A) (a + b) : A) m)
            ⋯,
        den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i + m * i)) (f ^ i * f ^ i) ⋯, den_mem := ⋯ } ∈
    q.asIdeal

Tactic:
simp_rw [← pow_add, map_add, add_pow, mul_comm, ← nsmul_eq_mul]

Premises used: pow_add, map_add, add_pow, mul_comm, nsmul_eq_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
q : (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1)
a b : A
ha : a ∈ carrier f_deg q
hb : b ∈ carrier f_deg q
i j : ℕ
h2 : ¬m + m < j
h1 : j ≤ m
rw : f ^ i ∈ 𝒜 (i * m)
⊢ f ^ i ∈ 𝒜 (m * i)

Tactic:
rw [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
q : (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1)
a b : A
ha : a ∈ carrier f_deg q
hb : b ∈ carrier f_deg q
i j : ℕ
h2 : ¬m + m < j
h1 : j ≤ m
⊢ f ^ i ∈ 𝒜 (i * m)

Tactic:
mem_tac
-- 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
q : (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1)
a b : A
ha : a ∈ carrier f_deg q
hb : b ∈ carrier f_deg q
i j : ℕ
h2 : ¬m + m < j
h1 : j ≤ m
rw : HPow.hPow (α := A) ((proj 𝒜 i : (a : A) → A) b : A) m ∈ 𝒜 (m • i)
⊢ HPow.hPow (α := A) ((proj 𝒜 i : (a : A) → A) b : A) m ∈ 𝒜 (m * i)

Tactic:
rw [← smul_eq_mul]

Premises used: smul_eq_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
q : (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1)
a b : A
ha : a ∈ carrier f_deg q
hb : b ∈ carrier f_deg q
i j : ℕ
h2 : ¬m + m < j
h1 : j ≤ m
⊢ HPow.hPow (α := A) ((proj 𝒜 i : (a : A) → A) b : A) m ∈ 𝒜 (m • i)

Tactic:
mem_tac
-- 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
q : (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1)
a b : A
ha : a ∈ carrier f_deg q
hb : b ∈ carrier f_deg q
i j : ℕ
h2 : ¬m + m < j
h1 : ¬j ≤ m
rw : HPow.hPow (α := A) ((proj 𝒜 i : (a : A) → A) a : A) m ∈ 𝒜 (m • i)
⊢ HPow.hPow (α := A) ((proj 𝒜 i : (a : A) → A) a : A) m ∈ 𝒜 (m * i)

Tactic:
rw [← smul_eq_mul]

Premises used: smul_eq_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
q : (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1)
a b : A
ha : a ∈ carrier f_deg q
hb : b ∈ carrier f_deg q
i j : ℕ
h2 : ¬m + m < j
h1 : ¬j ≤ m
⊢ HPow.hPow (α := A) ((proj 𝒜 i : (a : A) → A) a : A) m ∈ 𝒜 (m • i)

Tactic:
mem_tac
-- 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
q : (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1)
a b : A
ha : a ∈ carrier f_deg q
hb : b ∈ carrier f_deg q
i j : ℕ
h2 : ¬m + m < j
h1 : ¬j ≤ m
rw : f ^ i ∈ 𝒜 (i * m)
⊢ f ^ i ∈ 𝒜 (m * i)

Tactic:
rw [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
q : (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1)
a b : A
ha : a ∈ carrier f_deg q
hb : b ∈ carrier f_deg q
i j : ℕ
h2 : ¬m + m < j
h1 : ¬j ≤ m
⊢ f ^ i ∈ 𝒜 (i * m)

Tactic:
mem_tac