awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
q : (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1)
a : A
i : ℕ
x : A⁰_ f
h : Membership.mem (γ := Set (A⁰_ f)) {s : A⁰_ f | s ∈ q.asIdeal} x
hx :
  Eq (α := Localization (Submonoid.powers f))
    ((algebraMap (A⁰_ f) (Localization.Away f) : (a : A⁰_ f) → Localization.Away f) x : Localization.Away f)
    (Localization.mk (HPow.hPow (α := A) ((proj 𝒜 i : (a : A) → A) a : A) m)
        (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers f) x) (f ^ i) ⋯) :
      Localization (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 := ⋯ } ∈
    q.asIdeal
have h₁ : x ∈ q.asIdeal
Tactic: change x ∈ q.asIdeal at h
Cleared hypotheses: h
-- 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 : A
i : ℕ
x : A⁰_ f
hx :
  Eq (α := Localization (Submonoid.powers f))
    ((algebraMap (A⁰_ f) (Localization.Away f) : (a : A⁰_ f) → Localization.Away f) x : Localization.Away f)
    (Localization.mk (HPow.hPow (α := A) ((proj 𝒜 i : (a : A) → A) a : A) m)
        (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers f) x) (f ^ i) ⋯) :
      Localization (Submonoid.powers f))
h : x ∈ 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) a : A) m) ⋯,
        den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i)) (f ^ i) ⋯, den_mem := ⋯ } ∈
    q.asIdeal
have h₁ : 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) sorry,
      den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i)) (f ^ i) sorry, den_mem := sorry } =
  x
Tactic: convert! h
-- 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 : A
i : ℕ
x : A⁰_ f
hx :
  Eq (α := Localization (Submonoid.powers f))
    ((algebraMap (A⁰_ f) (Localization.Away f) : (a : A⁰_ f) → Localization.Away f) x : Localization.Away f)
    (Localization.mk (HPow.hPow (α := A) ((proj 𝒜 i : (a : A) → A) a : A) m)
        (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers f) x) (f ^ i) ⋯) :
      Localization (Submonoid.powers f))
h : x ∈ 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) a : A) m) ⋯,
        den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i)) (f ^ i) ⋯, den_mem := ⋯ } =
    x
have h₁ : Localization.mk
    (↑(NumDenSameDeg.num
          { deg := m * i,
            num :=
              Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i)) (HPow.hPow (α := A) ((proj 𝒜 i : (a : A) → A) a : A) m) sorry,
            den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i)) (f ^ i) sorry, den_mem := sorry }) :
      A)
    (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers f) x)
      (↑(NumDenSameDeg.den
            { deg := m * i,
              num :=
                Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i)) (HPow.hPow (α := A) ((proj 𝒜 i : (a : A) → A) a : A) m) sorry,
              den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i)) (f ^ i) sorry, den_mem := sorry }) :
        A)
      sorry) =
  HomogeneousLocalization.val x
Tactic: rw [HomogeneousLocalization.ext_iff_val, HomogeneousLocalization.val_mk]
-- 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 : A
i : ℕ
x : A⁰_ f
hx :
  Eq (α := Localization (Submonoid.powers f))
    ((algebraMap (A⁰_ f) (Localization.Away f) : (a : A⁰_ f) → Localization.Away f) x : Localization.Away f)
    (Localization.mk (HPow.hPow (α := A) ((proj 𝒜 i : (a : A) → A) a : A) m)
        (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers f) x) (f ^ i) ⋯) :
      Localization (Submonoid.powers f))
h : x ∈ q.asIdeal
⊢ Localization.mk
      (↑(NumDenSameDeg.num
            { 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 := ⋯ }) :
        A)
      (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers f) x)
        (↑(NumDenSameDeg.den
              { 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 := ⋯ }) :
          A)
        ⋯) =
    HomogeneousLocalization.val x
have h₁ : Localization.mk (HPow.hPow (α := A) ((proj 𝒜 i : (a : A) → A) a : A) m)
    (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers f) x) (f ^ i) sorry) =
  HomogeneousLocalization.val x
Tactic: dsimp only [Subtype.coe_mk]
-- 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 : A
i : ℕ
x : A⁰_ f
hx :
  Eq (α := Localization (Submonoid.powers f))
    ((algebraMap (A⁰_ f) (Localization.Away f) : (a : A⁰_ f) → Localization.Away f) x : Localization.Away f)
    (Localization.mk (HPow.hPow (α := A) ((proj 𝒜 i : (a : A) → A) a : A) m)
        (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers f) x) (f ^ i) ⋯) :
      Localization (Submonoid.powers f))
h : x ∈ q.asIdeal
⊢ Localization.mk (HPow.hPow (α := A) ((proj 𝒜 i : (a : A) → A) a : A) m)
      (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers f) x) (f ^ i) ⋯) =
    HomogeneousLocalization.val x
have h₁ : (algebraMap (A⁰_ f) (Localization.Away f) : (a : A⁰_ f) → Localization.Away f) x = HomogeneousLocalization.val x
Tactic: rw [← hx]
-- 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)
a : A
n : ℕ
hn : a ∈ 𝒜 n
⊢ f ^ n ∈ 𝒜 (m * n)
have rw : f ^ n ∈ 𝒜 (n * 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
hm : 0 < m
q : (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1)
a : A
n : ℕ
hn : a ∈ 𝒜 n
⊢ HPow.hPow (α := A) ((proj 𝒜 n : (a : A) → A) a : A) m ∈ 𝒜 (m * n)
have rw : HPow.hPow (α := A) ((proj 𝒜 n : (a : A) → A) a : A) m ∈ 𝒜 (m • n)
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
hm : 0 < m
q : (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1)
a : A
n : ℕ
hn : a ∈ 𝒜 n
⊢ a ∈ carrier f_deg q ↔
    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 := ⋯ } ∈
      q.asIdeal
have trans : a ∈ carrier f_deg q ↔
  HomogeneousLocalization.mk
      { deg := m * n,
        num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * n)) (HPow.hPow (α := A) ((proj 𝒜 n : (a : A) → A) a : A) m) sorry,
        den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * n)) (f ^ n) sorry, den_mem := sorry } ∈
    q.asIdeal
Tactic: trans (HomogeneousLocalization.mk ⟨m * n, ⟨proj 𝒜 n a ^ m, by rw [← smul_eq_mul]; mem_tac⟩,
    ⟨f ^ n, by rw [mul_comm]; mem_tac⟩, ⟨_, rfl⟩⟩ : A⁰_ f) ∈ q.asIdeal
-- 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)
a : A
n : ℕ
hn : a ∈ 𝒜 n
trans :
  a ∈ carrier f_deg q ↔
    HomogeneousLocalization.mk
        { deg := m * n,
          num :=
            Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * n)) (HPow.hPow (α := A) ((proj 𝒜 n : (a : A) → A) a : A) m) ⋯,
          den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * n)) (f ^ n) ⋯, 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 ^ m) ⋯,
          den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * n)) (f ^ n) ⋯, den_mem := ⋯ } ∈
      q.asIdeal
have trans₁ : HomogeneousLocalization.mk
      { deg := m * n,
        num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * n)) (HPow.hPow (α := A) ((proj 𝒜 n : (a : A) → A) a : A) m) sorry,
        den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * n)) (f ^ n) sorry, den_mem := sorry } ∈
    q.asIdeal ↔
  HomogeneousLocalization.mk
      { deg := m * n, num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * n)) (a ^ m) sorry,
        den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * n)) (f ^ n) sorry, den_mem := sorry } ∈
    q.asIdeal
Tactic: trans (HomogeneousLocalization.mk ⟨m * n, ⟨proj 𝒜 n a ^ m, by rw [← smul_eq_mul]; mem_tac⟩,
    ⟨f ^ n, by rw [mul_comm]; mem_tac⟩, ⟨_, rfl⟩⟩ : A⁰_ f) ∈ q.asIdeal
-- 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)
a : A
n : ℕ
hn : a ∈ 𝒜 n
⊢ a ∈ carrier f_deg q ↔
    HomogeneousLocalization.mk
        { deg := m * n,
          num :=
            Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * n)) (HPow.hPow (α := A) ((proj 𝒜 n : (a : A) → A) a : A) m) ⋯,
          den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * n)) (f ^ n) ⋯, den_mem := ⋯ } ∈
      q.asIdeal
have refine : ∀
  (h :
    HomogeneousLocalization.mk
        { deg := m * n,
          num :=
            Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * n)) (HPow.hPow (α := A) ((proj 𝒜 n : (a : A) → A) a : A) m) sorry,
          den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * n)) (f ^ n) sorry, den_mem := sorry } ∈
      q.asIdeal)
  (i : ℕ) (hi : ¬i = n),
  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) sorry,
        den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i)) (f ^ i) sorry, den_mem := sorry } ∈
    q.asIdeal
Tactic: refine ⟨fun h ↦ h n, fun h i ↦ if hi : i = n then hi ▸ h else ?_⟩
-- 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)
a : A
n : ℕ
hn : a ∈ 𝒜 n
h :
  HomogeneousLocalization.mk
      { deg := m * n,
        num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * n)) (HPow.hPow (α := A) ((proj 𝒜 n : (a : A) → A) a : A) m) ⋯,
        den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * n)) (f ^ n) ⋯, den_mem := ⋯ } ∈
    q.asIdeal
i : ℕ
hi : ¬i = n
⊢ 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 := ⋯ } ∈
    q.asIdeal
have h₁ : Eq (α := 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) sorry,
      den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i)) (f ^ i) sorry, den_mem := sorry })
  0
Tactic: convert! zero_mem q.asIdeal
-- 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)
a : A
n : ℕ
hn : a ∈ 𝒜 n
h :
  HomogeneousLocalization.mk
      { deg := m * n,
        num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * n)) (HPow.hPow (α := A) ((proj 𝒜 n : (a : A) → A) a : A) m) ⋯,
        den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * n)) (f ^ n) ⋯, den_mem := ⋯ } ∈
    q.asIdeal
i : ℕ
hi : ¬i = n
⊢ Eq (α := 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 := ⋯ })
    0
have h₁ : Eq (α := Localization (Submonoid.powers f))
  (HomogeneousLocalization.val
    (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) sorry,
        den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i)) (f ^ i) sorry, den_mem := sorry :
        NumDenSameDeg 𝒜 (Submonoid.powers f) }))
  (HomogeneousLocalization.val.{0, u_1, u_2} (ι := ℕ) (σ := σ) (𝒜 := 𝒜) 0)
Tactic: apply HomogeneousLocalization.val_injective
-- 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)
a : A
n : ℕ
hn : a ∈ 𝒜 (n * m)
⊢ f ^ n ∈ 𝒜 (m * n)
have rw : f ^ n ∈ 𝒜 (n * 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
hm : 0 < m
q : (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1)
a : A
n : ℕ
hn : a ∈ 𝒜 (n * m)
⊢ 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
have rw : (HPow.hPow (α := A⁰_ f)
      (HomogeneousLocalization.mk
        { deg := m * n, num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * n)) a sorry,
          den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * n)) (f ^ n) sorry, den_mem := sorry :
          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) sorry,
        den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * (n * m))) (f ^ (n * m)) sorry, den_mem := sorry } ∈
    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]
-- 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)
a : A
n : ℕ
hn : a ∈ 𝒜 (n * m)
⊢ (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)
have e_a : HPow.hPow (α := A⁰_ f)
    (HomogeneousLocalization.mk
      { deg := m * n, num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * n)) a sorry,
        den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * n)) (f ^ n) sorry, den_mem := sorry :
        NumDenSameDeg 𝒜 (Submonoid.powers f) })
    m =
  HomogeneousLocalization.mk
    { deg := m * (n * m), num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * (n * m))) (a ^ m) sorry,
      den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * (n * m))) (f ^ (n * m)) sorry, den_mem := sorry }
Tactic: congr 1
-- 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)
a : A
n : ℕ
hn : a ∈ 𝒜 (n * m)
⊢ 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 := ⋯ }
have e_a : HomogeneousLocalization.val
    (HPow.hPow (α := A⁰_ f)
      (HomogeneousLocalization.mk
        { deg := m * n, num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * n)) a sorry,
          den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * n)) (f ^ n) sorry, den_mem := sorry :
          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) sorry,
        den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * (n * m))) (f ^ (n * m)) sorry, den_mem := sorry :
        NumDenSameDeg 𝒜 (Submonoid.powers f) })
Tactic: apply HomogeneousLocalization.val_injective
-- 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)
a : A
n : ℕ
hn : a ∈ 𝒜 (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) })
have 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) sorry) m))
  (Localization.mk (a ^ m)
    (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers f) x) ((f ^ n) ^ m) sorry))
Tactic: simp only [HomogeneousLocalization.val_mk, HomogeneousLocalization.val_pow,
    Localization.mk_pow, pow_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
hm : 0 < m
q : (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1)
z : NumDenSameDeg 𝒜 (Submonoid.powers f)
⊢ (↑z.num : A) ∈ carrier f_deg q ↔ HomogeneousLocalization.mk z ∈ q.asIdeal
have obtain : ∀ (n : ℕ) (hn : f ^ n = (↑z.den : A)), (↑z.num : A) ∈ carrier f_deg q ↔ HomogeneousLocalization.mk z ∈ q.asIdeal
Tactic: obtain ⟨n, hn : f ^ n = _⟩ := z.den_mem
-- 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)
e : f ^ n = 0
⊢ False
have this : Subsingleton.{max (u_1 + 1) 1} (HomogeneousLocalization 𝒜 (Submonoid.powers f))
Tactic: have := HomogeneousLocalization.subsingleton 𝒜 (x := .powers f) ⟨n, 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
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)
⊢ (↑z.num : A) ∈ carrier f_deg q ↔ HomogeneousLocalization.mk z ∈ q.asIdeal
have this : 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
-- 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
⊢ (↑z.num : A) ∈ carrier f_deg q ↔ HomogeneousLocalization.mk z ∈ q.asIdeal
have h : HomogeneousLocalization.mk z =
  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 }
Tactic: convert! mem_carrier_iff_of_mem_mul f_deg hm q z.num.1 (n := n) ?_ using 2