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
q : (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1)
a : A
i : ℕ
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) ⋯,
        den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i)) (f ^ i) ⋯, den_mem := ⋯ } ∈
    q.asIdeal
⊢ ∃ (x : A⁰_ f),
    Membership.mem (γ := Set (A⁰_ f)) {s : A⁰_ f | s ∈ q.asIdeal} x ∧
      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))

Tactic:
refine ⟨_, h, 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
q : (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1)
a : A
i : ℕ
h :
  Membership.mem (γ := Set (Localization.Away f))
    (Set.image (α := A⁰_ f) (⇑(algebraMap (A⁰_ f) (Localization.Away f)) : (a : A⁰_ f) → Localization.Away f)
      {s : A⁰_ f | s ∈ 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) ⋯))
⊢ ∃ (x : A⁰_ f),
    Membership.mem (γ := Set (A⁰_ f)) {s : A⁰_ f | s ∈ q.asIdeal} x ∧
      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))

Tactic:
rw [Set.mem_image] at h

Premises used: Set.mem_image
-- 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 : A
i : ℕ
h :
  ∃ (x : A⁰_ f),
    Membership.mem (γ := Set (A⁰_ f)) {s : A⁰_ f | s ∈ q.asIdeal} x ∧
      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))
mpr :
  ∀ (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
⊢ 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

Tactic:
rcases h with ⟨x, h, hx⟩
-- 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 : 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))
⊢ x ∈ q.asIdeal

Tactic:
change x ∈ q.asIdeal at h

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
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
⊢ x ∈ q.asIdeal

Tactic:
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
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
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) ⋯,
        den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i)) (f ^ i) ⋯, den_mem := ⋯ } =
    x
⊢ 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

Tactic:
convert! 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
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
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) ⋯,
              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
⊢ 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

Tactic:
rw [HomogeneousLocalization.ext_iff_val, HomogeneousLocalization.val_mk]

Premises used: HomogeneousLocalization.val_mk, HomogeneousLocalization.ext_iff_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
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
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) ⋯) =
    HomogeneousLocalization.val x
⊢ 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

Tactic:
dsimp only [Subtype.coe_mk]

Premises used: Subtype.coe_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
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
h₁ : (algebraMap (A⁰_ f) (Localization.Away f) : (a : A⁰_ f) → Localization.Away f) x = HomogeneousLocalization.val x
⊢ 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

Tactic:
rw [← hx]
-- 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 : 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
⊢ (algebraMap (A⁰_ f) (Localization.Away f) : (a : A⁰_ f) → Localization.Away f) x = HomogeneousLocalization.val x

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)
a : A
n : ℕ
hn : a ∈ 𝒜 n
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
⊢ 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
rw : HPow.hPow (α := A) ((proj 𝒜 n : (a : A) → A) a : A) m ∈ 𝒜 (m • n)
⊢ HPow.hPow (α := A) ((proj 𝒜 n : (a : A) → A) a : A) m ∈ 𝒜 (m * n)

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
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)

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
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
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) ⋯,
          den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * n)) (f ^ n) ⋯, den_mem := ⋯ } ∈
      q.asIdeal ↔
    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
⊢ 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

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

Premises used: HMul.hMul, Subtype.mk, HPow.hPow, HomogeneousLocalization.NumDenSameDeg.mk, GradedRing.proj, Exists.intro, HomogeneousLocalization.mk, DFunLike.coe, PrimeSpectrum.asIdeal, 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)
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

Tactic:
⟨fun h ↦ h n, fun h i ↦ if hi : i = n then hi ▸ h else ?_⟩

Premises used: Eq.rec, dite, Iff.intro, Eq.symm, Eq
-- 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
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) ⋯,
            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
⊢ 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

Tactic:
refine ⟨fun h ↦ h n, fun h i ↦ if hi : i = n then hi ▸ h else ?_⟩
-- 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
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
⊢ 0 ∈ q.asIdeal

Tactic:
zero_mem q.asIdeal

Premises used: ZeroMemClass.zero_mem, 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)
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
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) ⋯,
        den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i)) (f ^ i) ⋯, den_mem := ⋯ })
    0
⊢ 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

Tactic:
convert! zero_mem q.asIdeal

Premises used: ZeroMemClass.zero_mem, 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)
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
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) ⋯,
          den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i)) (f ^ i) ⋯, den_mem := ⋯ :
          NumDenSameDeg 𝒜 (Submonoid.powers f) }))
    (HomogeneousLocalization.val.{0, u_1, u_2} (ι := ℕ) (σ := σ) (𝒜 := 𝒜) 0)
⊢ 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

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
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 (α := 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) ⋯,
          den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i)) (f ^ i) ⋯, den_mem := ⋯ :
          NumDenSameDeg 𝒜 (Submonoid.powers f) }))
    (HomogeneousLocalization.val.{0, u_1, u_2} (ι := ℕ) (σ := σ) (𝒜 := 𝒜) 0)

Tactic:
simp only [proj_apply, decompose_of_mem_ne _ hn (Ne.symm hi), zero_pow hm.ne',
      HomogeneousLocalization.val_mk, Localization.mk_zero, HomogeneousLocalization.val_zero]

Premises used: HomogeneousLocalization.val_zero, HomogeneousLocalization.val_mk, Ne.symm, LT.lt.ne', DirectSum.decompose_of_mem_ne, Localization.mk_zero, zero_pow, 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)
a : A
n : ℕ
hn : a ∈ 𝒜 n
⊢ 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 ↔
    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

Tactic:
simp only [proj_apply, decompose_of_mem_same _ hn]

Premises used: DirectSum.decompose_of_mem_same, GradedRing.proj_apply