awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
q : (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1)
x : A
hx : x ∈ carrier f_deg q
refine_1 : HSMul.hSMul (α := A) 0 x ∈ carrier f_deg q
refine_2 : ∀ {i : ℕ} (m_1 : ↥(𝒜 i)), (↑m_1 : A) • x ∈ carrier f_deg q
refine_3 : ∀ (m_1 m' : A), m_1 • x ∈ carrier f_deg q → m' • x ∈ carrier f_deg q → (m_1 + m') • x ∈ carrier f_deg q
⊢ ∀ (c : A), c • x ∈ carrier f_deg q

Tactic:
refine DirectSum.Decomposition.inductionOn 𝒜 ?_ ?_ ?_
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
q : (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1)
x : A
hx : x ∈ carrier f_deg q
refine_1 : 0 ∈ carrier f_deg q
⊢ HSMul.hSMul (α := A) 0 x ∈ carrier f_deg q

Tactic:
rw [zero_smul]

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

Tactic:
carrier.zero_mem f_deg hm _

Premises used: AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier.zero_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)
x : A
hx : x ∈ carrier f_deg q
⊢ 0 ∈ carrier f_deg q

Tactic:
exact carrier.zero_mem f_deg hm _

Premises used: AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier.zero_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)
x : A
hx : x ∈ carrier f_deg q
n : ℕ
a : A
ha : a ∈ 𝒜 n
i : ℕ
refine_2 :
  HomogeneousLocalization.mk
      { deg := m * i,
        num :=
          Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i))
            ((if n ≤ i then
                a *
                  (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ℕ), ↥(𝒜 i)) x : ⨁ (i : ℕ), ↥(𝒜 i)) : (a : ℕ) → ↥(𝒜 a)) (i - n)) :
                    A)
              else 0) ^
              m)
            ⋯,
        den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i)) (f ^ i) ⋯, den_mem := ⋯ } ∈
    q.asIdeal
⊢ HomogeneousLocalization.mk
      { deg := m * i,
        num :=
          Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i))
            (HPow.hPow (α := A)
              ((proj 𝒜 i : (a : A) → A) ((↑(Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 n) a ha) : A) • x) : A) m)
            ⋯,
        den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i)) (f ^ i) ⋯, den_mem := ⋯ } ∈
    q.asIdeal

Tactic:
simp_rw [proj_apply, smul_eq_mul, coe_decompose_mul_of_left_mem 𝒜 i ha]

Premises used: DirectSum.coe_decompose_mul_of_left_mem, smul_eq_mul, GradedRing.proj_apply
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
q : (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1)
x : A
hx : x ∈ carrier f_deg q
n : ℕ
a : A
ha : a ∈ 𝒜 n
i : ℕ
⊢ HPow.hPow (α := A) ((proj 𝒜 (i - n) : (a : A) → A) x : A) m ∈ 𝒜 (m • (i - n))

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)
x : A
hx : x ∈ carrier f_deg q
n : ℕ
a : A
ha : a ∈ 𝒜 n
i : ℕ
refine_2 :
  HomogeneousLocalization.mk
      { deg := m * i,
        num :=
          Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i))
            ((if n ≤ i then
                a *
                  (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ℕ), ↥(𝒜 i)) x : ⨁ (i : ℕ), ↥(𝒜 i)) : (a : ℕ) → ↥(𝒜 a)) (i - n)) :
                    A)
              else 0) ^
              m)
            ⋯,
        den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i)) (f ^ i) ⋯, den_mem := ⋯ } ∈
    q.asIdeal
refine_2₁ : f ^ n ∈ 𝒜 (m • n)
refine_2₂ : f ^ (i - n) ∈ 𝒜 (m • (i - n))
⊢ HomogeneousLocalization.mk
      { deg := m * i,
        num :=
          Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i))
            ((if n ≤ i then
                a *
                  (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ℕ), ↥(𝒜 i)) x : ⨁ (i : ℕ), ↥(𝒜 i)) : (a : ℕ) → ↥(𝒜 a)) (i - n)) :
                    A)
              else 0) ^
              m)
            ⋯,
        den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i)) (f ^ i) ⋯, den_mem := ⋯ } ∈
    q.asIdeal

Tactic:
let product : A⁰_ f :=
      (HomogeneousLocalization.mk
          ⟨_, ⟨a ^ m, pow_mem_graded m ha⟩, ⟨_, ?_⟩, ⟨n, rfl⟩⟩ : A⁰_ f) *
        (HomogeneousLocalization.mk
          ⟨_, ⟨proj 𝒜 (i - n) x ^ m, by mem_tac⟩, ⟨_, ?_⟩, ⟨i - n, rfl⟩⟩ : A⁰_ f)
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
q : (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1)
x : A
hx : x ∈ carrier f_deg q
n : ℕ
a : A
ha : a ∈ 𝒜 n
i : ℕ
product : A⁰_ f :=
  HMul.hMul (α := HomogeneousLocalization 𝒜 (Submonoid.powers f))
    (HomogeneousLocalization.mk
      { deg := m • n, num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m • n)) (a ^ m) ⋯,
        den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m • n)) (f ^ n) ⋯, den_mem := ⋯ })
    (HomogeneousLocalization.mk
      { deg := m • (i - n),
        num :=
          Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m • (i - n)))
            (HPow.hPow (α := A) ((proj 𝒜 (i - n) : (a : A) → A) x : A) m) ⋯,
        den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m • (i - n))) (f ^ (i - n)) ⋯, den_mem := ⋯ })
pos :
  ∀ (h : n ≤ i),
    HomogeneousLocalization.mk
        { deg := m * i,
          num :=
            Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i))
              ((a *
                  (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ℕ), ↥(𝒜 i)) x : ⨁ (i : ℕ), ↥(𝒜 i)) : (a : ℕ) → ↥(𝒜 a)) (i - n)) :
                    A)) ^
                m)
              ⋯,
          den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i)) (f ^ i) ⋯, den_mem := ⋯ } ∈
      q.asIdeal
neg :
  ∀ (h : ¬n ≤ i),
    HomogeneousLocalization.mk
        { deg := m * i, num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i)) (HPow.hPow (α := A) 0 m) ⋯,
          den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i)) (f ^ i) ⋯, den_mem := ⋯ } ∈
      q.asIdeal
⊢ HomogeneousLocalization.mk
      { deg := m * i,
        num :=
          Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i))
            ((if n ≤ i then
                a *
                  (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ℕ), ↥(𝒜 i)) x : ⨁ (i : ℕ), ↥(𝒜 i)) : (a : ℕ) → ↥(𝒜 a)) (i - n)) :
                    A)
              else 0) ^
              m)
            ⋯,
        den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i)) (f ^ i) ⋯, den_mem := ⋯ } ∈
    q.asIdeal

Tactic:
split_ifs with h
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
q : (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1)
x : A
hx : x ∈ carrier f_deg q
n : ℕ
a : A
ha : a ∈ 𝒜 n
i : ℕ
product : A⁰_ f :=
  HMul.hMul (α := HomogeneousLocalization 𝒜 (Submonoid.powers f))
    (HomogeneousLocalization.mk
      { deg := m • n, num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m • n)) (a ^ m) ⋯,
        den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m • n)) (f ^ n) ⋯, den_mem := ⋯ })
    (HomogeneousLocalization.mk
      { deg := m • (i - n),
        num :=
          Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m • (i - n)))
            (HPow.hPow (α := A) ((proj 𝒜 (i - n) : (a : A) → A) x : A) m) ⋯,
        den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m • (i - n))) (f ^ (i - n)) ⋯, den_mem := ⋯ })
h : n ≤ i
h₁ :
  HomogeneousLocalization.mk
      { deg := m * i,
        num :=
          Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i))
            ((a *
                (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ℕ), ↥(𝒜 i)) x : ⨁ (i : ℕ), ↥(𝒜 i)) : (a : ℕ) → ↥(𝒜 a)) (i - n)) :
                  A)) ^
              m)
            ⋯,
        den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i)) (f ^ i) ⋯, den_mem := ⋯ } =
    product
pos : product ∈ q.asIdeal
⊢ HomogeneousLocalization.mk
      { deg := m * i,
        num :=
          Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i))
            ((a *
                (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ℕ), ↥(𝒜 i)) x : ⨁ (i : ℕ), ↥(𝒜 i)) : (a : ℕ) → ↥(𝒜 a)) (i - n)) :
                  A)) ^
              m)
            ⋯,
        den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i)) (f ^ i) ⋯, den_mem := ⋯ } ∈
    q.asIdeal

Tactic:
convert_to product ∈ q.1

Premises used: PrimeSpectrum.asIdeal
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
q : (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1)
x : A
hx : x ∈ carrier f_deg q
n : ℕ
a : A
ha : a ∈ 𝒜 n
i : ℕ
product : A⁰_ f :=
  HMul.hMul (α := HomogeneousLocalization 𝒜 (Submonoid.powers f))
    (HomogeneousLocalization.mk
      { deg := m • n, num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m • n)) (a ^ m) ⋯,
        den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m • n)) (f ^ n) ⋯, den_mem := ⋯ })
    (HomogeneousLocalization.mk
      { deg := m • (i - n),
        num :=
          Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m • (i - n)))
            (HPow.hPow (α := A) ((proj 𝒜 (i - n) : (a : A) → A) x : A) m) ⋯,
        den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m • (i - n))) (f ^ (i - n)) ⋯, den_mem := ⋯ })
h : n ≤ i
h₁ :
  HomogeneousLocalization.mk
      { deg := m * i,
        num :=
          Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i))
            ((a *
                (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ℕ), ↥(𝒜 i)) x : ⨁ (i : ℕ), ↥(𝒜 i)) : (a : ℕ) → ↥(𝒜 a)) (i - n)) :
                  A)) ^
              m)
            ⋯,
        den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i)) (f ^ i) ⋯, den_mem := ⋯ } =
    HMul.hMul (α := HomogeneousLocalization 𝒜 (Submonoid.powers f))
      (HomogeneousLocalization.mk
        { deg := m * n, num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * n)) (a ^ m) ⋯,
          den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * n)) (f ^ n) ⋯, den_mem := ⋯ :
          NumDenSameDeg 𝒜 (Submonoid.powers f) })
      (HomogeneousLocalization.mk
        { deg := m * (i - n),
          num :=
            Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * (i - n)))
              ((↑((((decompose 𝒜 : (a : A) → ⨁ (i : ℕ), ↥(𝒜 i)) x : ⨁ (i : ℕ), ↥(𝒜 i)) : (a : ℕ) → ↥(𝒜 a)) (i - n)) :
                  A) ^
                m)
              ⋯,
          den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * (i - n))) (f ^ (i - n)) ⋯, den_mem := ⋯ :
          NumDenSameDeg 𝒜 (Submonoid.powers f) })
⊢ HomogeneousLocalization.mk
      { deg := m * i,
        num :=
          Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i))
            ((a *
                (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ℕ), ↥(𝒜 i)) x : ⨁ (i : ℕ), ↥(𝒜 i)) : (a : ℕ) → ↥(𝒜 a)) (i - n)) :
                  A)) ^
              m)
            ⋯,
        den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i)) (f ^ i) ⋯, den_mem := ⋯ } =
    product

Tactic:
dsimp [product]
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
q : (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1)
x : A
hx : x ∈ carrier f_deg q
n : ℕ
a : A
ha : a ∈ 𝒜 n
i : ℕ
product : A⁰_ f :=
  HMul.hMul (α := HomogeneousLocalization 𝒜 (Submonoid.powers f))
    (HomogeneousLocalization.mk
      { deg := m • n, num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m • n)) (a ^ m) ⋯,
        den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m • n)) (f ^ n) ⋯, den_mem := ⋯ })
    (HomogeneousLocalization.mk
      { deg := m • (i - n),
        num :=
          Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m • (i - n)))
            (HPow.hPow (α := A) ((proj 𝒜 (i - n) : (a : A) → A) x : A) m) ⋯,
        den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m • (i - n))) (f ^ (i - n)) ⋯, den_mem := ⋯ })
h : n ≤ i
h₁ :
  Eq (α := Localization (Submonoid.powers f))
    (Localization.mk
      (a ^ m *
        (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ℕ), ↥(𝒜 i)) x : ⨁ (i : ℕ), ↥(𝒜 i)) : (a : ℕ) → ↥(𝒜 a)) (i - n)) : A) ^ m)
      (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers f) x) (f ^ i) ⋯))
    (Localization.mk
      (a ^ m *
        (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ℕ), ↥(𝒜 i)) x : ⨁ (i : ℕ), ↥(𝒜 i)) : (a : ℕ) → ↥(𝒜 a)) (i - n)) : A) ^ m)
      (HMul.hMul (α := ↥(Submonoid.powers f))
        (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers f) x) (f ^ n) ⋯)
        (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers f) x) (f ^ (i - n)) ⋯)))
⊢ Localization.mk
      (a ^ m *
        (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ℕ), ↥(𝒜 i)) x : ⨁ (i : ℕ), ↥(𝒜 i)) : (a : ℕ) → ↥(𝒜 a)) (i - n)) : A) ^ m)
      (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers f) x) (f ^ i) ⋯) =
    HMul.hMul (α := Localization (Submonoid.powers f))
      (Localization.mk (a ^ m)
        (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers f) x) (f ^ n) ⋯))
      (Localization.mk
        ((↑((((decompose 𝒜 : (a : A) → ⨁ (i : ℕ), ↥(𝒜 i)) x : ⨁ (i : ℕ), ↥(𝒜 i)) : (a : ℕ) → ↥(𝒜 a)) (i - n)) : A) ^ m)
        (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers f) x) (f ^ (i - n)) ⋯))

Tactic:
rw [Localization.mk_mul]

Premises used: Localization.mk_mul
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
q : (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1)
x : A
hx : x ∈ carrier f_deg q
n : ℕ
a : A
ha : a ∈ 𝒜 n
i : ℕ
product : A⁰_ f :=
  HMul.hMul (α := HomogeneousLocalization 𝒜 (Submonoid.powers f))
    (HomogeneousLocalization.mk
      { deg := m • n, num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m • n)) (a ^ m) ⋯,
        den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m • n)) (f ^ n) ⋯, den_mem := ⋯ })
    (HomogeneousLocalization.mk
      { deg := m • (i - n),
        num :=
          Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m • (i - n)))
            (HPow.hPow (α := A) ((proj 𝒜 (i - n) : (a : A) → A) x : A) m) ⋯,
        den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m • (i - n))) (f ^ (i - n)) ⋯, den_mem := ⋯ })
h : n ≤ i
h₁ :
  f ^ i =
    (↑(Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers f) x) (f ^ n) ⋯) : A) *
      (↑(Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers f) x) (f ^ (i - n)) ⋯) : A)
⊢ Eq (α := Localization (Submonoid.powers f))
    (Localization.mk
      (a ^ m *
        (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ℕ), ↥(𝒜 i)) x : ⨁ (i : ℕ), ↥(𝒜 i)) : (a : ℕ) → ↥(𝒜 a)) (i - n)) : A) ^ m)
      (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers f) x) (f ^ i) ⋯))
    (Localization.mk
      (a ^ m *
        (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ℕ), ↥(𝒜 i)) x : ⨁ (i : ℕ), ↥(𝒜 i)) : (a : ℕ) → ↥(𝒜 a)) (i - n)) : A) ^ m)
      (HMul.hMul (α := ↥(Submonoid.powers f))
        (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers f) x) (f ^ n) ⋯)
        (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers f) x) (f ^ (i - n)) ⋯)))

Tactic:
congr
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
q : (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1)
x : A
hx : x ∈ carrier f_deg q
n : ℕ
a : A
ha : a ∈ 𝒜 n
i : ℕ
product : A⁰_ f :=
  HMul.hMul (α := HomogeneousLocalization 𝒜 (Submonoid.powers f))
    (HomogeneousLocalization.mk
      { deg := m • n, num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m • n)) (a ^ m) ⋯,
        den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m • n)) (f ^ n) ⋯, den_mem := ⋯ })
    (HomogeneousLocalization.mk
      { deg := m • (i - n),
        num :=
          Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m • (i - n)))
            (HPow.hPow (α := A) ((proj 𝒜 (i - n) : (a : A) → A) x : A) m) ⋯,
        den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m • (i - n))) (f ^ (i - n)) ⋯, den_mem := ⋯ })
h : n ≤ i
h₁ : f ^ i = f ^ (n + (i - n))
h₂ h₃ : f ^ i = f ^ i
⊢ f ^ i =
    (↑(Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers f) x) (f ^ n) ⋯) : A) *
      (↑(Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers f) x) (f ^ (i - n)) ⋯) : A)

Tactic:
rw [← pow_add, Nat.add_sub_of_le h]

Premises used: pow_add, Nat.add_sub_of_le
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
q : (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1)
x : A
hx : x ∈ carrier f_deg q
n : ℕ
a : A
ha : a ∈ 𝒜 n
i : ℕ
product : A⁰_ f :=
  HMul.hMul (α := HomogeneousLocalization 𝒜 (Submonoid.powers f))
    (HomogeneousLocalization.mk
      { deg := m • n, num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m • n)) (a ^ m) ⋯,
        den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m • n)) (f ^ n) ⋯, den_mem := ⋯ })
    (HomogeneousLocalization.mk
      { deg := m • (i - n),
        num :=
          Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m • (i - n)))
            (HPow.hPow (α := A) ((proj 𝒜 (i - n) : (a : A) → A) x : A) m) ⋯,
        den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m • (i - n))) (f ^ (i - n)) ⋯, den_mem := ⋯ })
h : n ≤ i
refine_2 : f ^ n ∈ 𝒜 (m • n)
⊢ product ∈ q.asIdeal

Tactic:
apply Ideal.mul_mem_left (α := A⁰_ f) _ _ (hx _)

Premises used: Ideal.mul_mem_left
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
q : (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1)
x : A
hx : x ∈ carrier f_deg q
n : ℕ
a : A
ha : a ∈ 𝒜 n
i : ℕ
refine_2 : f ^ n ∈ 𝒜 (n • m)
rw : m • n = n • m
⊢ f ^ n ∈ 𝒜 (m • n)

Tactic:
rw [(_ : m • n = _)]
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
q : (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1)
x : A
hx : x ∈ carrier f_deg q
n : ℕ
a : A
ha : a ∈ 𝒜 n
i : ℕ
⊢ 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)
x : A
hx : x ∈ carrier f_deg q
n : ℕ
a : A
ha : a ∈ 𝒜 n
i : ℕ
⊢ m • n = n • m

Tactic:
simp only [smul_eq_mul, mul_comm]

Premises used: mul_comm, 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)
x : A
hx : x ∈ carrier f_deg q
n : ℕ
a : A
ha : a ∈ 𝒜 n
i : ℕ
product : A⁰_ f :=
  HMul.hMul (α := HomogeneousLocalization 𝒜 (Submonoid.powers f))
    (HomogeneousLocalization.mk
      { deg := m • n, num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m • n)) (a ^ m) ⋯,
        den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m • n)) (f ^ n) ⋯, den_mem := ⋯ })
    (HomogeneousLocalization.mk
      { deg := m • (i - n),
        num :=
          Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m • (i - n)))
            (HPow.hPow (α := A) ((proj 𝒜 (i - n) : (a : A) → A) x : A) m) ⋯,
        den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m • (i - n))) (f ^ (i - n)) ⋯, den_mem := ⋯ })
h : ¬n ≤ i
⊢ HomogeneousLocalization.mk
      { deg := m * i, num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i)) (HPow.hPow (α := A) 0 m) ⋯,
        den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i)) (f ^ i) ⋯, den_mem := ⋯ } ∈
    q.asIdeal

Tactic:
simpa only [map_zero, zero_pow hm.ne'] using zero_mem f_deg hm q i

Premises used: AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier.zero_mem, map_zero, LT.lt.ne', zero_pow
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
q : (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1)
x : A
hx : x ∈ carrier f_deg q
n : ℕ
a : A
ha : a ∈ 𝒜 n
i : ℕ
refine_2 : f ^ (i - n) ∈ 𝒜 ((i - n) • m)
rw : m • (i - n) = (i - n) • m
⊢ f ^ (i - n) ∈ 𝒜 (m • (i - n))

Tactic:
rw [(_ : m • (i - n) = _)]
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
q : (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1)
x : A
hx : x ∈ carrier f_deg q
n : ℕ
a : A
ha : a ∈ 𝒜 n
i : ℕ
⊢ f ^ (i - n) ∈ 𝒜 ((i - 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)
x : A
hx : x ∈ carrier f_deg q
n : ℕ
a : A
ha : a ∈ 𝒜 n
i : ℕ
⊢ m • (i - n) = (i - n) • m

Tactic:
simp only [smul_eq_mul, mul_comm]

Premises used: mul_comm, 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)
x : A
hx : x ∈ carrier f_deg q
refine_3 : ∀ (m_1 m' : A), m_1 • x ∈ carrier f_deg q → m' • x ∈ carrier f_deg q → m_1 • x + m' • x ∈ carrier f_deg q
⊢ ∀ (m_1 m' : A), m_1 • x ∈ carrier f_deg q → m' • x ∈ carrier f_deg q → (m_1 + m') • x ∈ carrier f_deg q

Tactic:
simp_rw [add_smul]

Premises used: add_smul