awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper
Goal:
σ : Type u_1
A : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
d e : ℕ
f : A
hf : f ∈ 𝒜 d
g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
hd : 0 < d
n : ℕ
a : A
ha : a ∈ 𝒜 n
j : ℕ
hb' : (fun (x_1 : ℕ) ↦ x ^ x_1) j ∈ 𝒜 n
hfg : ¬(f * g) ^ j = 0
this : n = j * (d + e)
x0 : NumDenSameDeg 𝒜 (Submonoid.powers f) :=
  { deg := j * (d * (e + 1)),
    num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (j * (d * (e + 1)))) (a * g ^ (j * (d - 1))) ⋯,
    den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (j * (d * (e + 1)))) (f ^ (j * (e + 1))) ⋯, den_mem := ⋯ }
h : j * (d * e) = (j * e) • d
⊢ f ^ (j * e) ∈ 𝒜 (j * (d * e))

Tactic:
convert! SetLike.pow_mem_graded _ hf using 2

Premises used: SetLike.pow_mem_graded
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper
Goal:
σ : Type u_1
A : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
d e : ℕ
f : A
hf : f ∈ 𝒜 d
g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
hd : 0 < d
n : ℕ
a : A
ha : a ∈ 𝒜 n
j : ℕ
hb' : (fun (x_1 : ℕ) ↦ x ^ x_1) j ∈ 𝒜 n
hfg : ¬(f * g) ^ j = 0
this : n = j * (d + e)
x0 : NumDenSameDeg 𝒜 (Submonoid.powers f) :=
  { deg := j * (d * (e + 1)),
    num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (j * (d * (e + 1)))) (a * g ^ (j * (d - 1))) ⋯,
    den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (j * (d * (e + 1)))) (f ^ (j * (e + 1))) ⋯, den_mem := ⋯ }
⊢ j * (d * e) = (j * e) • d

Tactic:
ring
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper
Goal:
σ : Type u_1
A : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
d e : ℕ
f : A
hf : f ∈ 𝒜 d
g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
hd : 0 < d
n : ℕ
a : A
ha : a ∈ 𝒜 n
j : ℕ
hb' : (fun (x_1 : ℕ) ↦ x ^ x_1) j ∈ 𝒜 n
hfg : ¬(f * g) ^ j = 0
this : n = j * (d + e)
x0 : NumDenSameDeg 𝒜 (Submonoid.powers f) :=
  { deg := j * (d * (e + 1)),
    num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (j * (d * (e + 1)))) (a * g ^ (j * (d - 1))) ⋯,
    den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (j * (d * (e + 1)))) (f ^ (j * (e + 1))) ⋯, den_mem := ⋯ }
⊢ g ^ (j * d) ∈ 𝒜 ((j * d) • e)

Tactic:
SetLike.pow_mem_graded _ hg

Premises used: SetLike.pow_mem_graded
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper
Goal:
σ : Type u_1
A : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
d e : ℕ
f : A
hf : f ∈ 𝒜 d
g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
hd : 0 < d
n : ℕ
a : A
ha : a ∈ 𝒜 n
j : ℕ
hb' : (fun (x_1 : ℕ) ↦ x ^ x_1) j ∈ 𝒜 n
hfg : ¬(f * g) ^ j = 0
this : n = j * (d + e)
x0 : NumDenSameDeg 𝒜 (Submonoid.powers f) :=
  { deg := j * (d * (e + 1)),
    num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (j * (d * (e + 1)))) (a * g ^ (j * (d - 1))) ⋯,
    den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (j * (d * (e + 1)))) (f ^ (j * (e + 1))) ⋯, den_mem := ⋯ }
h : j * (d * e) = (j * d) • e
⊢ g ^ (j * d) ∈ 𝒜 (j * (d * e))

Tactic:
convert! SetLike.pow_mem_graded _ hg using 2

Premises used: SetLike.pow_mem_graded
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper
Goal:
σ : Type u_1
A : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
d e : ℕ
f : A
hf : f ∈ 𝒜 d
g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
hd : 0 < d
n : ℕ
a : A
ha : a ∈ 𝒜 n
j : ℕ
hb' : (fun (x_1 : ℕ) ↦ x ^ x_1) j ∈ 𝒜 n
hfg : ¬(f * g) ^ j = 0
this : n = j * (d + e)
x0 : NumDenSameDeg 𝒜 (Submonoid.powers f) :=
  { deg := j * (d * (e + 1)),
    num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (j * (d * (e + 1)))) (a * g ^ (j * (d - 1))) ⋯,
    den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (j * (d * (e + 1)))) (f ^ (j * (e + 1))) ⋯, den_mem := ⋯ }
⊢ j * (d * e) = (j * d) • e

Tactic:
ring
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper
Goal:
σ : Type u_1
A : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
d e : ℕ
f : A
hf : f ∈ 𝒜 d
g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
hd : 0 < d
n : ℕ
a : A
ha : a ∈ 𝒜 n
j : ℕ
hb' : (fun (x_1 : ℕ) ↦ x ^ x_1) j ∈ 𝒜 n
hfg : ¬(f * g) ^ j = 0
this : n = j * (d + e)
x0 : NumDenSameDeg 𝒜 (Submonoid.powers f) :=
  { deg := j * (d * (e + 1)),
    num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (j * (d * (e + 1)))) (a * g ^ (j * (d - 1))) ⋯,
    den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (j * (d * (e + 1)))) (f ^ (j * (e + 1))) ⋯, den_mem := ⋯ }
y0 : NumDenSameDeg 𝒜 (Submonoid.powers g) :=
  { deg := j * (d * e), num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (j * (d * e))) (f ^ (j * e)) ⋯,
    den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (j * (d * e))) (g ^ (j * d)) ⋯, den_mem := ⋯ }
h :
  Eq (α := Away 𝒜 x)
    (((Algebra.TensorProduct.lift (awayMapₐ 𝒜 hg hx) (awayMapₐ 𝒜 hf ⋯) ⋯ :
            TensorProduct (↥(𝒜 0)) (Away 𝒜 f) (Away 𝒜 g) →ₐ[↥(𝒜 0)] Away 𝒜 x) :
          (a : TensorProduct (↥(𝒜 0)) (Away 𝒜 f) (Away 𝒜 g)) → Away 𝒜 x)
        (HomogeneousLocalization.mk x0 ⊗ₜ[↥(𝒜 0)] HomogeneousLocalization.mk y0) :
      Away 𝒜 x)
    (HomogeneousLocalization.mk
        { deg := n, num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 n) a ha,
          den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 n) ((fun (x_1 : ℕ) ↦ x ^ x_1) j) hb', den_mem := ⋯ } :
      HomogeneousLocalization 𝒜 (Submonoid.powers x))
⊢ ∃ (a_1 : TensorProduct (↥(𝒜 0)) (Away 𝒜 f) (Away 𝒜 g)),
    Eq (α := Away 𝒜 x)
      (((Algebra.TensorProduct.lift (awayMapₐ 𝒜 hg hx) (awayMapₐ 𝒜 hf ⋯) ⋯ :
              TensorProduct (↥(𝒜 0)) (Away 𝒜 f) (Away 𝒜 g) →ₐ[↥(𝒜 0)] Away 𝒜 x) :
            (a : TensorProduct (↥(𝒜 0)) (Away 𝒜 f) (Away 𝒜 g)) → Away 𝒜 x)
          a_1 :
        Away 𝒜 x)
      (HomogeneousLocalization.mk
          { deg := n, num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 n) a ha,
            den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 n) ((fun (x_1 : ℕ) ↦ x ^ x_1) j) hb', den_mem := ⋯ } :
        HomogeneousLocalization 𝒜 (Submonoid.powers x))

Tactic:
use mk x0 ⊗ₜ mk y0

Premises used: HomogeneousLocalization.mk
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper
Goal:
σ : Type u_1
A : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
d e : ℕ
f : A
hf : f ∈ 𝒜 d
g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
hd : 0 < d
n : ℕ
a : A
ha : a ∈ 𝒜 n
j : ℕ
hb' : (fun (x_1 : ℕ) ↦ x ^ x_1) j ∈ 𝒜 n
hfg : ¬(f * g) ^ j = 0
this : n = j * (d + e)
x0 : NumDenSameDeg 𝒜 (Submonoid.powers f) :=
  { deg := j * (d * (e + 1)),
    num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (j * (d * (e + 1)))) (a * g ^ (j * (d - 1))) ⋯,
    den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (j * (d * (e + 1)))) (f ^ (j * (e + 1))) ⋯, den_mem := ⋯ }
y0 : NumDenSameDeg 𝒜 (Submonoid.powers g) :=
  { deg := j * (d * e), num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (j * (d * e))) (f ^ (j * e)) ⋯,
    den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (j * (d * e))) (g ^ (j * d)) ⋯, den_mem := ⋯ }
h :
  Eq (α := Localization (Submonoid.powers x))
    (val.{0, u_2, u_1} (ι := ℕ) (σ := σ) (𝒜 := 𝒜)
      (((Algebra.TensorProduct.lift (awayMapₐ 𝒜 hg hx) (awayMapₐ 𝒜 hf ⋯) ⋯ :
            TensorProduct (↥(𝒜 0)) (Away 𝒜 f) (Away 𝒜 g) →ₐ[↥(𝒜 0)] Away 𝒜 x) :
          (a : TensorProduct (↥(𝒜 0)) (Away 𝒜 f) (Away 𝒜 g)) → Away 𝒜 x)
        (HomogeneousLocalization.mk x0 ⊗ₜ[↥(𝒜 0)] HomogeneousLocalization.mk y0)))
    (val
      (HomogeneousLocalization.mk
        { deg := n, num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 n) a ha,
          den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 n) ((fun (x_1 : ℕ) ↦ x ^ x_1) j) hb', den_mem := ⋯ :
          NumDenSameDeg 𝒜 (Submonoid.powers x) }))
⊢ Eq (α := Away 𝒜 x)
    (((Algebra.TensorProduct.lift (awayMapₐ 𝒜 hg hx) (awayMapₐ 𝒜 hf ⋯) ⋯ :
            TensorProduct (↥(𝒜 0)) (Away 𝒜 f) (Away 𝒜 g) →ₐ[↥(𝒜 0)] Away 𝒜 x) :
          (a : TensorProduct (↥(𝒜 0)) (Away 𝒜 f) (Away 𝒜 g)) → Away 𝒜 x)
        (HomogeneousLocalization.mk x0 ⊗ₜ[↥(𝒜 0)] HomogeneousLocalization.mk y0) :
      Away 𝒜 x)
    (HomogeneousLocalization.mk
        { deg := n, num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 n) a ha,
          den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 n) ((fun (x_1 : ℕ) ↦ x ^ x_1) j) hb', den_mem := ⋯ } :
      HomogeneousLocalization 𝒜 (Submonoid.powers x))

Tactic:
ext
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper
Goal:
σ : Type u_1
A : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
d e : ℕ
f : A
hf : f ∈ 𝒜 d
g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
hd : 0 < d
n : ℕ
a : A
ha : a ∈ 𝒜 n
j : ℕ
hb' : (fun (x_1 : ℕ) ↦ x ^ x_1) j ∈ 𝒜 n
hfg : ¬(f * g) ^ j = 0
this : n = j * (d + e)
x0 : NumDenSameDeg 𝒜 (Submonoid.powers f) :=
  { deg := j * (d * (e + 1)),
    num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (j * (d * (e + 1)))) (a * g ^ (j * (d - 1))) ⋯,
    den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (j * (d * (e + 1)))) (f ^ (j * (e + 1))) ⋯, den_mem := ⋯ }
y0 : NumDenSameDeg 𝒜 (Submonoid.powers g) :=
  { deg := j * (d * e), num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (j * (d * e))) (f ^ (j * e)) ⋯,
    den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (j * (d * e))) (g ^ (j * d)) ⋯, den_mem := ⋯ }
h :
  Eq (α := Localization (Submonoid.powers x))
    (Localization.mk (a * g ^ (j * (d - 1)) * g ^ (j * (e + 1)) * (f ^ (j * e) * f ^ (j * d)))
      (Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1) (x ^ (j * (e + 1)))
          ⋯ *
        Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1) (x ^ (j * d)) ⋯))
    (Localization.mk a
      (Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1) (x ^ j) ⋯))
⊢ Eq (α := Localization (Submonoid.powers x))
    (val.{0, u_2, u_1} (ι := ℕ) (σ := σ) (𝒜 := 𝒜)
      (((Algebra.TensorProduct.lift (awayMapₐ 𝒜 hg hx) (awayMapₐ 𝒜 hf ⋯) ⋯ :
            TensorProduct (↥(𝒜 0)) (Away 𝒜 f) (Away 𝒜 g) →ₐ[↥(𝒜 0)] Away 𝒜 x) :
          (a : TensorProduct (↥(𝒜 0)) (Away 𝒜 f) (Away 𝒜 g)) → Away 𝒜 x)
        (HomogeneousLocalization.mk x0 ⊗ₜ[↥(𝒜 0)] HomogeneousLocalization.mk y0)))
    (val
      (HomogeneousLocalization.mk
        { deg := n, num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 n) a ha,
          den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 n) ((fun (x_1 : ℕ) ↦ x ^ x_1) j) hb', den_mem := ⋯ :
          NumDenSameDeg 𝒜 (Submonoid.powers x) }))

Tactic:
simp only [Algebra.TensorProduct.lift_tmul, awayMapₐ_apply, val_mul,
    val_awayMap_mk, Localization.mk_mul, val_mk, x0, y0]

Premises used: HomogeneousLocalization.awayMapₐ_apply, HomogeneousLocalization.val_mk, HomogeneousLocalization.val_mul, HomogeneousLocalization.val_awayMap_mk, Algebra.TensorProduct.lift_tmul, Localization.mk_mul
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper
Goal:
σ : Type u_1
A : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
d e : ℕ
f : A
hf : f ∈ 𝒜 d
g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
hd : 0 < d
n : ℕ
a : A
ha : a ∈ 𝒜 n
j : ℕ
hb' : (fun (x_1 : ℕ) ↦ x ^ x_1) j ∈ 𝒜 n
hfg : ¬(f * g) ^ j = 0
this : n = j * (d + e)
x0 : NumDenSameDeg 𝒜 (Submonoid.powers f) :=
  { deg := j * (d * (e + 1)),
    num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (j * (d * (e + 1)))) (a * g ^ (j * (d - 1))) ⋯,
    den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (j * (d * (e + 1)))) (f ^ (j * (e + 1))) ⋯, den_mem := ⋯ }
y0 : NumDenSameDeg 𝒜 (Submonoid.powers g) :=
  { deg := j * (d * e), num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (j * (d * e))) (f ^ (j * e)) ⋯,
    den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (j * (d * e))) (g ^ (j * d)) ⋯, den_mem := ⋯ }
h :
  ∃ (c : ↥(Submonoid.powers x)),
    (↑c : A) *
        ((↑(a,
                  Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1) (x ^ j)
                    ⋯).2 :
            A) *
          (a * g ^ (j * (d - 1)) * g ^ (j * (e + 1)) * (f ^ (j * e) * f ^ (j * d)),
              Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1)
                  (x ^ (j * (e + 1))) ⋯ *
                Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1)
                  (x ^ (j * d)) ⋯).1) =
      (↑c : A) *
        ((↑(a * g ^ (j * (d - 1)) * g ^ (j * (e + 1)) * (f ^ (j * e) * f ^ (j * d)),
                  Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1)
                      (x ^ (j * (e + 1))) ⋯ *
                    Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1)
                      (x ^ (j * d)) ⋯).2 :
            A) *
          (a, Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1) (x ^ j) ⋯).1)
⊢ Eq (α := Localization (Submonoid.powers x))
    (Localization.mk (a * g ^ (j * (d - 1)) * g ^ (j * (e + 1)) * (f ^ (j * e) * f ^ (j * d)))
      (Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1) (x ^ (j * (e + 1)))
          ⋯ *
        Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1) (x ^ (j * d)) ⋯))
    (Localization.mk a
      (Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1) (x ^ j) ⋯))

Tactic:
rw [Localization.mk_eq_mk_iff, Localization.r_iff_exists]

Premises used: Localization.r_iff_exists, Localization.mk_eq_mk_iff
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper
Goal:
σ : Type u_1
A : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
d e : ℕ
f : A
hf : f ∈ 𝒜 d
g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
hd : 0 < d
n : ℕ
a : A
ha : a ∈ 𝒜 n
j : ℕ
hb' : (fun (x_1 : ℕ) ↦ x ^ x_1) j ∈ 𝒜 n
hfg : ¬(f * g) ^ j = 0
this : n = j * (d + e)
x0 : NumDenSameDeg 𝒜 (Submonoid.powers f) :=
  { deg := j * (d * (e + 1)),
    num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (j * (d * (e + 1)))) (a * g ^ (j * (d - 1))) ⋯,
    den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (j * (d * (e + 1)))) (f ^ (j * (e + 1))) ⋯, den_mem := ⋯ }
y0 : NumDenSameDeg 𝒜 (Submonoid.powers g) :=
  { deg := j * (d * e), num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (j * (d * e))) (f ^ (j * e)) ⋯,
    den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (j * (d * e))) (g ^ (j * d)) ⋯, den_mem := ⋯ }
h :
  (↑1 : A) *
      ((↑(a, Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1) (x ^ j) ⋯).2 :
          A) *
        (a * g ^ (j * (d - 1)) * g ^ (j * (e + 1)) * (f ^ (j * e) * f ^ (j * d)),
            Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1)
                (x ^ (j * (e + 1))) ⋯ *
              Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1) (x ^ (j * d))
                ⋯).1) =
    (↑1 : A) *
      ((↑(a * g ^ (j * (d - 1)) * g ^ (j * (e + 1)) * (f ^ (j * e) * f ^ (j * d)),
                Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1)
                    (x ^ (j * (e + 1))) ⋯ *
                  Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1)
                    (x ^ (j * d)) ⋯).2 :
          A) *
        (a, Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1) (x ^ j) ⋯).1)
⊢ ∃ (c : ↥(Submonoid.powers x)),
    (↑c : A) *
        ((↑(a,
                  Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1) (x ^ j)
                    ⋯).2 :
            A) *
          (a * g ^ (j * (d - 1)) * g ^ (j * (e + 1)) * (f ^ (j * e) * f ^ (j * d)),
              Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1)
                  (x ^ (j * (e + 1))) ⋯ *
                Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1)
                  (x ^ (j * d)) ⋯).1) =
      (↑c : A) *
        ((↑(a * g ^ (j * (d - 1)) * g ^ (j * (e + 1)) * (f ^ (j * e) * f ^ (j * d)),
                  Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1)
                      (x ^ (j * (e + 1))) ⋯ *
                    Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1)
                      (x ^ (j * d)) ⋯).2 :
            A) *
          (a, Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1) (x ^ j) ⋯).1)

Tactic:
use 1
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper
Goal:
σ : Type u_1
A : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
d e : ℕ
f : A
hf : f ∈ 𝒜 d
g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
hd : 0 < d
n : ℕ
a : A
ha : a ∈ 𝒜 n
j : ℕ
hb' : (fun (x_1 : ℕ) ↦ x ^ x_1) j ∈ 𝒜 n
hfg : ¬(f * g) ^ j = 0
this : n = j * (d + e)
x0 : NumDenSameDeg 𝒜 (Submonoid.powers f) :=
  { deg := j * (d * (e + 1)),
    num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (j * (d * (e + 1)))) (a * g ^ (j * (d - 1))) ⋯,
    den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (j * (d * (e + 1)))) (f ^ (j * (e + 1))) ⋯, den_mem := ⋯ }
y0 : NumDenSameDeg 𝒜 (Submonoid.powers g) :=
  { deg := j * (d * e), num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (j * (d * e))) (f ^ (j * e)) ⋯,
    den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (j * (d * e))) (g ^ (j * d)) ⋯, den_mem := ⋯ }
h :
  x ^ j * (a * g ^ (j * (d - 1)) * g ^ (j * (e + 1)) * (f ^ (j * e) * f ^ (j * d))) =
    x ^ (j * (e + 1)) * x ^ (j * d) * a
⊢ (↑1 : A) *
      ((↑(a, Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1) (x ^ j) ⋯).2 :
          A) *
        (a * g ^ (j * (d - 1)) * g ^ (j * (e + 1)) * (f ^ (j * e) * f ^ (j * d)),
            Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1)
                (x ^ (j * (e + 1))) ⋯ *
              Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1) (x ^ (j * d))
                ⋯).1) =
    (↑1 : A) *
      ((↑(a * g ^ (j * (d - 1)) * g ^ (j * (e + 1)) * (f ^ (j * e) * f ^ (j * d)),
                Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1)
                    (x ^ (j * (e + 1))) ⋯ *
                  Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1)
                    (x ^ (j * d)) ⋯).2 :
          A) *
        (a, Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1) (x ^ j) ⋯).1)

Tactic:
simp only [OneMemClass.coe_one, one_mul, Submonoid.mk_mul_mk]

Premises used: OneMemClass.coe_one, Submonoid.mk_mul_mk, one_mul
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper
Goal:
σ : Type u_1
A : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
d e : ℕ
f : A
hf : f ∈ 𝒜 d
g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
hd : 0 < d
n : ℕ
a : A
ha : a ∈ 𝒜 n
j : ℕ
hb' : (fun (x_1 : ℕ) ↦ x ^ x_1) j ∈ 𝒜 n
hfg : ¬(f * g) ^ j = 0
this : n = j * (d + e)
x0 : NumDenSameDeg 𝒜 (Submonoid.powers f) :=
  { deg := j * (d * (e + 1)),
    num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (j * (d * (e + 1)))) (a * g ^ (j * (d - 1))) ⋯,
    den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (j * (d * (e + 1)))) (f ^ (j * (e + 1))) ⋯, den_mem := ⋯ }
y0 : NumDenSameDeg 𝒜 (Submonoid.powers g) :=
  { deg := j * (d * e), num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (j * (d * e))) (f ^ (j * e)) ⋯,
    den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (j * (d * e))) (g ^ (j * d)) ⋯, den_mem := ⋯ }
h :
  ∀ (hf : f ∈ 𝒜 0) (hd : LT.lt (α := ℕ) 0 0) (this : n = j * (0 + e)),
    x ^ j * (a * g ^ (j * HSub.hSub (α := ℕ) 0 1) * g ^ (j * (e + 1)) * (f ^ (j * e) * f ^ (j * 0))) =
      x ^ (j * (e + 1)) * x ^ (j * 0) * a
h₁ :
  ∀ (n_1 : ℕ) (hf : f ∈ 𝒜 (n_1 + 1)) (hd : 0 < n_1 + 1) (this : n = j * (n_1 + 1 + e)),
    x ^ j * (a * g ^ (j * (n_1 + 1 - 1)) * g ^ (j * (e + 1)) * (f ^ (j * e) * f ^ (j * (n_1 + 1)))) =
      x ^ (j * (e + 1)) * x ^ (j * (n_1 + 1)) * a
⊢ x ^ j * (a * g ^ (j * (d - 1)) * g ^ (j * (e + 1)) * (f ^ (j * e) * f ^ (j * d))) =
    x ^ (j * (e + 1)) * x ^ (j * d) * a

Tactic:
cases d
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper
Goal:
σ : Type u_1
A : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
e : ℕ
f g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
n : ℕ
a : A
ha : a ∈ 𝒜 n
j : ℕ
hb' : (fun (x_1 : ℕ) ↦ x ^ x_1) j ∈ 𝒜 n
hfg : ¬(f * g) ^ j = 0
hf : f ∈ 𝒜 0
hd : LT.lt (α := ℕ) 0 0
this : n = j * (0 + e)
x0 : NumDenSameDeg 𝒜 (Submonoid.powers f) :=
  { deg := j * (0 * (e + 1)),
    num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (j * (0 * (e + 1)))) (a * g ^ (j * HSub.hSub (α := ℕ) 0 1)) ⋯,
    den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (j * (0 * (e + 1)))) (f ^ (j * (e + 1))) ⋯, den_mem := ⋯ }
y0 : NumDenSameDeg 𝒜 (Submonoid.powers g) :=
  { deg := j * (0 * e), num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (j * (0 * e))) (f ^ (j * e)) ⋯,
    den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (j * (0 * e))) (g ^ (j * 0)) ⋯, den_mem := ⋯ }
⊢ x ^ j * (a * g ^ (j * HSub.hSub (α := ℕ) 0 1) * g ^ (j * (e + 1)) * (f ^ (j * e) * f ^ (j * 0))) =
    x ^ (j * (e + 1)) * x ^ (j * 0) * a

Tactic:
contradiction
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper
Goal:
σ : Type u_1
A : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
e : ℕ
f g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
n : ℕ
a : A
ha : a ∈ 𝒜 n
j : ℕ
hb' : (fun (x_1 : ℕ) ↦ x ^ x_1) j ∈ 𝒜 n
hfg : ¬(f * g) ^ j = 0
n_1 : ℕ
hf : f ∈ 𝒜 (n_1 + 1)
hd : 0 < n_1 + 1
this : n = j * (n_1 + 1 + e)
x0 : NumDenSameDeg 𝒜 (Submonoid.powers f) :=
  { deg := j * ((n_1 + 1) * (e + 1)),
    num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (j * ((n_1 + 1) * (e + 1)))) (a * g ^ (j * (n_1 + 1 - 1))) ⋯,
    den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (j * ((n_1 + 1) * (e + 1)))) (f ^ (j * (e + 1))) ⋯, den_mem := ⋯ }
y0 : NumDenSameDeg 𝒜 (Submonoid.powers g) :=
  { deg := j * ((n_1 + 1) * e), num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (j * ((n_1 + 1) * e))) (f ^ (j * e)) ⋯,
    den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (j * ((n_1 + 1) * e))) (g ^ (j * (n_1 + 1))) ⋯, den_mem := ⋯ }
h :
  (f * g) ^ j * (a * g ^ (j * n_1) * g ^ (j * (e + 1)) * (f ^ (j * e) * f ^ (j * (n_1 + 1)))) =
    (f * g) ^ (j * (e + 1)) * (f * g) ^ (j * (n_1 + 1)) * a
⊢ x ^ j * (a * g ^ (j * (n_1 + 1 - 1)) * g ^ (j * (e + 1)) * (f ^ (j * e) * f ^ (j * (n_1 + 1)))) =
    x ^ (j * (e + 1)) * x ^ (j * (n_1 + 1)) * a

Tactic:
simp only [hx, add_tsub_cancel_right]

Premises used: add_tsub_cancel_right
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper
Goal:
σ : Type u_1
A : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
e : ℕ
f g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
n : ℕ
a : A
ha : a ∈ 𝒜 n
j : ℕ
hb' : (fun (x_1 : ℕ) ↦ x ^ x_1) j ∈ 𝒜 n
hfg : ¬(f * g) ^ j = 0
n_1 : ℕ
hf : f ∈ 𝒜 (n_1 + 1)
hd : 0 < n_1 + 1
this : n = j * (n_1 + 1 + e)
x0 : NumDenSameDeg 𝒜 (Submonoid.powers f) :=
  { deg := j * ((n_1 + 1) * (e + 1)),
    num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (j * ((n_1 + 1) * (e + 1)))) (a * g ^ (j * (n_1 + 1 - 1))) ⋯,
    den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (j * ((n_1 + 1) * (e + 1)))) (f ^ (j * (e + 1))) ⋯, den_mem := ⋯ }
y0 : NumDenSameDeg 𝒜 (Submonoid.powers g) :=
  { deg := j * ((n_1 + 1) * e), num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (j * ((n_1 + 1) * e))) (f ^ (j * e)) ⋯,
    den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (j * ((n_1 + 1) * e))) (g ^ (j * (n_1 + 1))) ⋯, den_mem := ⋯ }
⊢ (f * g) ^ j * (a * g ^ (j * n_1) * g ^ (j * (e + 1)) * (f ^ (j * e) * f ^ (j * (n_1 + 1)))) =
    (f * g) ^ (j * (e + 1)) * (f * g) ^ (j * (n_1 + 1)) * a

Tactic:
ring