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
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 := ⋯ }
⊢ (↑z.num : A) ∈ carrier f_deg q ↔ HomogeneousLocalization.mk z ∈ q.asIdeal
have convert! : (↑z.num : A) ∈ 𝒜 (n * m)
Tactic: convert! mem_carrier_iff_of_mem_mul f_deg hm q z.num.1 (n := n) ?_ using 2
-- 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
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 =
    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 := ⋯ }
have 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) sorry,
        den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * n)) (f ^ n) sorry, den_mem := sorry :
        NumDenSameDeg 𝒜 (Submonoid.powers f) })
Tactic: apply HomogeneousLocalization.val_injective
-- 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
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) ∈ 𝒜 (n * m)
have this₁ : n • m = z.deg
Tactic: have := degree_eq_of_mem_mem 𝒜 (SetLike.pow_mem_graded n f_deg) (hn.symm ▸ z.den.2) this
-- 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
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) ∈ 𝒜 (n * m)
have rw : (↑z.num : A) ∈ 𝒜 z.deg
Tactic: rw [← smul_eq_mul, this]
-- 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
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
have 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)
              sorry,
          den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i)) (f ^ i) sorry, den_mem := sorry :
          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)
              sorry,
          den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i)) (f ^ i) sorry, den_mem := sorry :
          NumDenSameDeg 𝒜 (Submonoid.powers f) }) ∈
    q.asIdeal
Tactic: refine fun i => (q.2.mem_or_mem ?_).elim id id
-- 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
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 : ℕ
⊢ 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
have 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)))
            sorry :
          ↥(𝒜 (m * i + m * i))),
      den := (Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i + m * i)) (f ^ (i + i)) sorry : ↥(𝒜 (m * i + m * i))),
      den_mem := sorry } ∈
  q.asIdeal
Tactic: simp_rw [← pow_add, map_add, add_pow, mul_comm, ← nsmul_eq_mul]
-- 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
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 ∈ 𝒜 (m * i)
have rw : f ^ i ∈ 𝒜 (i * m)
Tactic: rw [mul_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
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)
have rw : HPow.hPow (α := A) ((proj 𝒜 i : (a : A) → A) b : A) m ∈ 𝒜 (m • i)
Tactic: rw [← smul_eq_mul]
-- 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
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)
have rw : HPow.hPow (α := A) ((proj 𝒜 i : (a : A) → A) a : A) m ∈ 𝒜 (m • i)
Tactic: rw [← smul_eq_mul]
-- 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
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 ∈ 𝒜 (m * i)
have rw : f ^ i ∈ 𝒜 (i * m)
Tactic: rw [mul_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
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 : ℕ
refine_3 :
  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))
              (∑ 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
have refine_1 : ∀ (j : ℕ) (h2 : ¬m + m < j) (h1 : j ≤ m),
  HPow.hPow (α := A) ((proj 𝒜 i : (a : A) → A) a : A) j * HPow.hPow (α := A) ((proj 𝒜 i : (a : A) → A) b : A) (m - j) ∈
    𝒜 (m * i)
Tactic: let g : ℕ → A⁰_ f := fun j => (m + m).choose j •
      if h2 : m + m < j then (0 : A⁰_ f)
      else
        if h1 : j ≤ m then
          (HomogeneousLocalization.mk
            ⟨m * i, ⟨proj 𝒜 i a ^ j * proj 𝒜 i b ^ (m - j), ?_⟩,
              ⟨_, by rw [mul_comm]; mem_tac⟩, ⟨i, rfl⟩⟩ : A⁰_ f) *
          (HomogeneousLocalization.mk
            ⟨m * i, ⟨proj 𝒜 i b ^ m, by rw [← smul_eq_mul]; mem_tac⟩,
              ⟨_, by rw [mul_comm]; mem_tac⟩, ⟨i, rfl⟩⟩ : A⁰_ f)
        else
          (HomogeneousLocalization.mk
            ⟨m * i, ⟨proj 𝒜 i a ^ m, by rw [← smul_eq_mul]; mem_tac⟩,
              ⟨_, by rw [mul_comm]; mem_tac⟩, ⟨i, rfl⟩⟩ : A⁰_ f) *
          (HomogeneousLocalization.mk
            ⟨m * i, ⟨proj 𝒜 i a ^ (j - m) * proj 𝒜 i b ^ (m + m - j), ?_⟩,
              ⟨_, by rw [mul_comm]; mem_tac⟩, ⟨i, rfl⟩⟩ : A⁰_ f)
-- 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
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 : ℕ
refine_3 :
  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
refine_1 :
  ∀ (j : ℕ) (h2 : ¬m + m < j) (h1 : j ≤ m),
    HPow.hPow (α := A) ((proj 𝒜 i : (a : A) → A) a : A) j *
        HPow.hPow (α := A) ((proj 𝒜 i : (a : A) → A) b : A) (m - j) ∈
      𝒜 (m * i)
⊢ 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
have refine_2 : ∀ (j : ℕ) (h2 : ¬m + m < j) (h1 : ¬j ≤ m),
  HPow.hPow (α := A) ((proj 𝒜 i : (a : A) → A) a : A) (j - m) *
      HPow.hPow (α := A) ((proj 𝒜 i : (a : A) → A) b : A) (m + m - j) ∈
    𝒜 (m * i)
Tactic: let g : ℕ → A⁰_ f := fun j => (m + m).choose j •
      if h2 : m + m < j then (0 : A⁰_ f)
      else
        if h1 : j ≤ m then
          (HomogeneousLocalization.mk
            ⟨m * i, ⟨proj 𝒜 i a ^ j * proj 𝒜 i b ^ (m - j), ?_⟩,
              ⟨_, by rw [mul_comm]; mem_tac⟩, ⟨i, rfl⟩⟩ : A⁰_ f) *
          (HomogeneousLocalization.mk
            ⟨m * i, ⟨proj 𝒜 i b ^ m, by rw [← smul_eq_mul]; mem_tac⟩,
              ⟨_, by rw [mul_comm]; mem_tac⟩, ⟨i, rfl⟩⟩ : A⁰_ f)
        else
          (HomogeneousLocalization.mk
            ⟨m * i, ⟨proj 𝒜 i a ^ m, by rw [← smul_eq_mul]; mem_tac⟩,
              ⟨_, by rw [mul_comm]; mem_tac⟩, ⟨i, rfl⟩⟩ : A⁰_ f) *
          (HomogeneousLocalization.mk
            ⟨m * i, ⟨proj 𝒜 i a ^ (j - m) * proj 𝒜 i b ^ (m + m - j), ?_⟩,
              ⟨_, by rw [mul_comm]; mem_tac⟩, ⟨i, rfl⟩⟩ : A⁰_ f)
-- 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
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) j * HPow.hPow (α := A) ((proj 𝒜 i : (a : A) → A) b : A) (m - j) ∈
    𝒜 (m * i)
have refine_1 : HPow.hPow (α := A) ((proj 𝒜 i : (a : A) → A) a : A) j * HPow.hPow (α := A) ((proj 𝒜 i : (a : A) → A) b : A) (m - j) ∈
  𝒜 (j • i + (m - j) • i)
Tactic: rw [(_ : m * i = _)]
-- 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
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
refine_1 :
  HPow.hPow (α := A) ((proj 𝒜 i : (a : A) → A) a : A) j * HPow.hPow (α := A) ((proj 𝒜 i : (a : A) → A) b : A) (m - j) ∈
    𝒜 (j • i + (m - j) • i)
⊢ HPow.hPow (α := A) ((proj 𝒜 i : (a : A) → A) a : A) j * HPow.hPow (α := A) ((proj 𝒜 i : (a : A) → A) b : A) (m - j) ∈
    𝒜 (m * i)
have rw : m * i = j • i + (m - j) • i
Tactic: rw [(_ : m * i = _)]
-- 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
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) j * HPow.hPow (α := A) ((proj 𝒜 i : (a : A) → A) b : A) (m - j) ∈
    𝒜 (j • i + (m - j) • i)
have refine_1 : HPow.hPow (α := A) ((proj 𝒜 i : (a : A) → A) a : A) j ∈ 𝒜 (j • i)
Tactic: apply GradedMonoid.toGradedMul.mul_mem
-- 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
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
refine_1 : HPow.hPow (α := A) ((proj 𝒜 i : (a : A) → A) a : A) j ∈ 𝒜 (j • i)
⊢ HPow.hPow (α := A) ((proj 𝒜 i : (a : A) → A) a : A) j * HPow.hPow (α := A) ((proj 𝒜 i : (a : A) → A) b : A) (m - j) ∈
    𝒜 (j • i + (m - j) • i)
have refine_1₁ : HPow.hPow (α := A) ((proj 𝒜 i : (a : A) → A) b : A) (m - j) ∈ 𝒜 ((m - j) • i)
Tactic: apply GradedMonoid.toGradedMul.mul_mem
-- 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
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
⊢ m * i = j • i + (m - j) • i
have rw : m * i = m • i
Tactic: rw [← add_smul, Nat.add_sub_of_le h1]
-- 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
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) (j - m) *
      HPow.hPow (α := A) ((proj 𝒜 i : (a : A) → A) b : A) (m + m - j) ∈
    𝒜 (m * i)
have refine_2 : HPow.hPow (α := A) ((proj 𝒜 i : (a : A) → A) a : A) (j - m) *
    HPow.hPow (α := A) ((proj 𝒜 i : (a : A) → A) b : A) (m + m - j) ∈
  𝒜 ((j - m) • i + (m + m - j) • i)
Tactic: rw [(_ : m * i = _)]
-- 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
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
refine_2 :
  HPow.hPow (α := A) ((proj 𝒜 i : (a : A) → A) a : A) (j - m) *
      HPow.hPow (α := A) ((proj 𝒜 i : (a : A) → A) b : A) (m + m - j) ∈
    𝒜 ((j - m) • i + (m + m - j) • i)
⊢ HPow.hPow (α := A) ((proj 𝒜 i : (a : A) → A) a : A) (j - m) *
      HPow.hPow (α := A) ((proj 𝒜 i : (a : A) → A) b : A) (m + m - j) ∈
    𝒜 (m * i)
have rw : m * i = (j - m) • i + (m + m - j) • i
Tactic: rw [(_ : m * i = _)]
-- 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
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) (j - m) *
      HPow.hPow (α := A) ((proj 𝒜 i : (a : A) → A) b : A) (m + m - j) ∈
    𝒜 ((j - m) • i + (m + m - j) • i)
have refine_2 : HPow.hPow (α := A) ((proj 𝒜 i : (a : A) → A) a : A) (j - m) ∈ 𝒜 ((j - m) • i)
Tactic: apply GradedMonoid.toGradedMul.mul_mem (i := (j - m) • i) (j := (m + m - j) • i)
-- 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
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
refine_2 : HPow.hPow (α := A) ((proj 𝒜 i : (a : A) → A) a : A) (j - m) ∈ 𝒜 ((j - m) • i)
⊢ HPow.hPow (α := A) ((proj 𝒜 i : (a : A) → A) a : A) (j - m) *
      HPow.hPow (α := A) ((proj 𝒜 i : (a : A) → A) b : A) (m + m - j) ∈
    𝒜 ((j - m) • i + (m + m - j) • i)
have refine_2₁ : HPow.hPow (α := A) ((proj 𝒜 i : (a : A) → A) b : A) (m + m - j) ∈ 𝒜 ((m + m - j) • i)
Tactic: apply GradedMonoid.toGradedMul.mul_mem (i := (j - m) • i) (j := (m + m - j) • i)
-- 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
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
⊢ m * i = (j - m) • i + (m + m - j) • i
have rw : m * i = (j - m + (m + m - j)) • i
Tactic: rw [← add_smul]
-- 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
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
⊢ m * i = (j - m + (m + m - j)) • i
have e_a : m = j - m + (m + m - j)
Tactic: congr
-- 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
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 : ℕ
g : ℕ → A⁰_ f :=
  fun (j : ℕ) ↦
    HSMul.hSMul (β := A⁰_ f) ((m + m).choose j)
      (if h2 : m + m < j then 0
      else
        if h1 : j ≤ m then
          HMul.hMul (α := HomogeneousLocalization 𝒜 (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 : A) j *
                      HPow.hPow (α := A) ((proj 𝒜 i : (a : A) → A) b : A) (m - j))
                    ⋯,
                den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i)) (f ^ i) ⋯, den_mem := ⋯ })
            (HomogeneousLocalization.mk
              { deg := m * i,
                num :=
                  Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i)) (HPow.hPow (α := A) ((proj 𝒜 i : (a : A) → A) b : A) m)
                    ⋯,
                den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i)) (f ^ i) ⋯, den_mem := ⋯ })
        else
          HMul.hMul (α := HomogeneousLocalization 𝒜 (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 : A) m)
                    ⋯,
                den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i)) (f ^ i) ⋯, den_mem := ⋯ })
            (HomogeneousLocalization.mk
              { deg := m * i,
                num :=
                  Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i))
                    (HPow.hPow (α := A) ((proj 𝒜 i : (a : A) → A) a : A) (j - m) *
                      HPow.hPow (α := A) ((proj 𝒜 i : (a : A) → A) b : A) (m + m - j))
                    ⋯,
                den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i)) (f ^ i) ⋯, den_mem := ⋯ }))
j : ℕ
hj : j ∈ range (m + m + 1)
⊢ Eq (α := Localization.Away f)
    (Localization.mk
      ((m + m).choose j •
        (HPow.hPow (α := A) ((proj 𝒜 i : (a : A) → A) a : A) j *
          HPow.hPow (α := A) ((proj 𝒜 i : (a : A) → A) b : A) (m + m - j)))
      (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers f) x) (f ^ (i + i)) ⋯))
    ((algebraMap (A⁰_ f) (Localization.Away f) : (a : A⁰_ f) → Localization.Away f) (g j))
have change : Localization.mk
    ((m + m).choose j •
      (HPow.hPow (α := A) ((proj 𝒜 i : (a : A) → A) a : A) j *
        HPow.hPow (α := A) ((proj 𝒜 i : (a : A) → A) b : A) (m + m - j)))
    (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers f) x) (f ^ (i + i)) sorry) =
  HomogeneousLocalization.val (g j)
Tactic: change _ = HomogeneousLocalization.val _