awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor
Goal:
A B C σ τ ψ : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
inst_3 : CommRing B
inst_4 : SetLike τ B
inst_5 : AddSubgroupClass τ B
inst_6 : CommRing C
inst_7 : SetLike ψ C
inst_8 : AddSubgroupClass ψ C
𝒜 : ℕ → σ
ℬ : ℕ → τ
𝒞 : ℕ → ψ
inst_9 : GradedRing 𝒜
inst_10 : GradedRing ℬ
inst_11 : GradedRing 𝒞
f : 𝒜 →+*ᵍ ℬ
g : ℬ →+*ᵍ 𝒞
hf : LE.le (α := HomogeneousIdeal ℬ) (ℬ₊) (HomogeneousIdeal.map f (𝒜₊))
hg : LE.le (α := HomogeneousIdeal 𝒞) (𝒞₊) (HomogeneousIdeal.map g (ℬ₊))
⊢ LE.le (α := HomogeneousIdeal 𝒜) (𝒜₊) (HomogeneousIdeal.map (GradedRingHom.id 𝒜) (𝒜₊))

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor
Goal:
A σ : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
⊢ map (GradedRingHom.id 𝒜) ⋯ = 𝟙 (Proj 𝒜)

Tactic:
(affineOpenCover _).openCover.hom_ext _ _ fun s ↦ ?_

Premises used: AlgebraicGeometry.Proj.affineOpenCover, AlgebraicGeometry.Scheme.AffineOpenCover.openCover, AlgebraicGeometry.Scheme.Cover.hom_ext
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor
Goal:
A σ : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
refine :
  ∀
    (s :
      PreZeroHypercover.I₀ (S := Proj 𝒜)
        (Precoverage.ZeroHypercover.toPreZeroHypercover (Scheme.AffineOpenCover.openCover (affineOpenCover 𝒜)))),
    PreZeroHypercover.f
          (Precoverage.ZeroHypercover.toPreZeroHypercover (Scheme.AffineOpenCover.openCover (affineOpenCover 𝒜))) s ≫
        map (GradedRingHom.id 𝒜) ⋯ =
      PreZeroHypercover.f
          (Precoverage.ZeroHypercover.toPreZeroHypercover (Scheme.AffineOpenCover.openCover (affineOpenCover 𝒜))) s ≫
        𝟙 (Proj 𝒜)
⊢ map (GradedRingHom.id 𝒜) ⋯ = 𝟙 (Proj 𝒜)

Tactic:
refine (affineOpenCover _).openCover.hom_ext _ _ fun s ↦ ?_

Premises used: AlgebraicGeometry.Proj.affineOpenCover, AlgebraicGeometry.Scheme.AffineOpenCover.openCover, AlgebraicGeometry.Scheme.Cover.hom_ext
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor
Goal:
A σ : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
s :
  PreZeroHypercover.I₀ (S := Proj 𝒜)
    (Precoverage.ZeroHypercover.toPreZeroHypercover (Scheme.AffineOpenCover.openCover (affineOpenCover 𝒜)))
⊢ Eq (α :=
    Spec
        (CommRingCat.of
          (Away (A := A) 𝒜
            ((GradedRingHom.id 𝒜 : (a : A) → A) (↑(s.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A) : A))) ⟶
      Proj 𝒜)
    (awayι 𝒜 ((GradedRingHom.id 𝒜 : (a : A) → A) (↑(s.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A)) ⋯ ⋯ ≫
      map (GradedRingHom.id 𝒜) ⋯)
    (Spec.map (CommRingCat.ofHom (Away.map (GradedRingHom.id 𝒜) (↑(s.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A))) ≫
      awayι 𝒜 (↑(s.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A) ⋯ ⋯)

Tactic:
awayι_comp_map (.id 𝒜) _ _ _ s.2.2

Premises used: Sigma.snd, GradedRingHom.id, AlgebraicGeometry.Proj.awayι_comp_map, Subtype.property
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor
Goal:
A σ : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
s :
  PreZeroHypercover.I₀ (S := Proj 𝒜)
    (Precoverage.ZeroHypercover.toPreZeroHypercover (Scheme.AffineOpenCover.openCover (affineOpenCover 𝒜)))
h :
  (PreZeroHypercover.X
          (Precoverage.ZeroHypercover.toPreZeroHypercover (Scheme.AffineOpenCover.openCover (affineOpenCover 𝒜))) s ⟶
        Proj 𝒜) =
      (Spec
          (CommRingCat.of
            (Away (A := A) 𝒜
              ((GradedRingHom.id 𝒜 : (a : A) → A) (↑(s.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A) : A))) ⟶
        Proj 𝒜) →
    PreZeroHypercover.f
          (Precoverage.ZeroHypercover.toPreZeroHypercover (Scheme.AffineOpenCover.openCover (affineOpenCover 𝒜))) s ≫
        𝟙 (Proj 𝒜) =
      Spec.map (CommRingCat.ofHom (Away.map (GradedRingHom.id 𝒜) (↑(s.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A))) ≫
        awayι 𝒜 (↑(s.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A) ⋯ ⋯
⊢ PreZeroHypercover.f
        (Precoverage.ZeroHypercover.toPreZeroHypercover (Scheme.AffineOpenCover.openCover (affineOpenCover 𝒜))) s ≫
      map (GradedRingHom.id 𝒜) ⋯ =
    PreZeroHypercover.f
        (Precoverage.ZeroHypercover.toPreZeroHypercover (Scheme.AffineOpenCover.openCover (affineOpenCover 𝒜))) s ≫
      𝟙 (Proj 𝒜)

Tactic:
convert! awayι_comp_map (.id 𝒜) _ _ _ s.2.2 using 1

Premises used: Sigma.snd, GradedRingHom.id, AlgebraicGeometry.Proj.awayι_comp_map, Subtype.property
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor
Goal:
A σ : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
s :
  PreZeroHypercover.I₀ (S := Proj 𝒜)
    (Precoverage.ZeroHypercover.toPreZeroHypercover (Scheme.AffineOpenCover.openCover (affineOpenCover 𝒜)))
e_1 :
  (PreZeroHypercover.X
        (Precoverage.ZeroHypercover.toPreZeroHypercover (Scheme.AffineOpenCover.openCover (affineOpenCover 𝒜))) s ⟶
      Proj 𝒜) =
    (Spec
        (CommRingCat.of
          (Away (A := A) 𝒜
            ((GradedRingHom.id 𝒜 : (a : A) → A) (↑(s.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A) : A))) ⟶
      Proj 𝒜)
⊢ PreZeroHypercover.f
        (Precoverage.ZeroHypercover.toPreZeroHypercover (Scheme.AffineOpenCover.openCover (affineOpenCover 𝒜))) s ≫
      𝟙 (Proj 𝒜) =
    Spec.map (CommRingCat.ofHom (Away.map (GradedRingHom.id 𝒜) (↑(s.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A))) ≫
      awayι 𝒜 (↑(s.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A) ⋯ ⋯

Tactic:
simp
-- 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
z : Away 𝒜 x
obtain :
  ∀ (n : ℕ) (a : A) (ha : a ∈ 𝒜 n) (j : ℕ) (hb' : (fun (x_1 : ℕ) ↦ x ^ x_1) j ∈ 𝒜 n),
    ∃ (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))
⊢ ∃ (a : TensorProduct (↥(𝒜 0)) (Away 𝒜 f) (Away 𝒜 g)),
    ((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 =
      z

Tactic:
obtain ⟨⟨n, ⟨a, ha⟩, ⟨b, hb'⟩, ⟨j, (rfl : _ = b)⟩⟩, rfl⟩ := mk_surjective z

Premises used: HomogeneousLocalization.mk_surjective, rfl
-- 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
pos :
  ∀ (hfg : (f * g) ^ j = 0),
    ∃ (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))
neg :
  ∀ (hfg : ¬(f * g) ^ j = 0),
    ∃ (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))
⊢ ∃ (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:
by_cases hfg : (f * g) ^ j = 0

Premises used: HMul.hMul
-- 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
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)
      0)
    (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 := ⋯ })
⊢ ∃ (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 0
-- 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
⊢ Subsingleton.{max (u_2 + 1) 1} (HomogeneousLocalization 𝒜 (Submonoid.powers x))

Tactic:
have := HomogeneousLocalization.subsingleton 𝒜 (x := Submonoid.powers x) ⟨j, hx ▸ hfg⟩
-- 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 : Subsingleton.{max (u_2 + 1) 1} (HomogeneousLocalization 𝒜 (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)
      0)
    (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 := ⋯ })

Tactic:
this.elim _ _

Premises used: Subsingleton.elim
-- 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 : Subsingleton.{max (u_2 + 1) 1} (HomogeneousLocalization 𝒜 (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)
      0)
    (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 := ⋯ })

Tactic:
exact this.elim _ _

Premises used: Subsingleton.elim
-- 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
hxj : (fun (x_1 : ℕ) ↦ x ^ x_1) j ∈ 𝒜 (j * (d + e))
hx₁ : Ne.{u_2 + 1} (α := A) ((fun (x_1 : ℕ) ↦ x ^ x_1) j) 0
⊢ n = j * (d + e)

Tactic:
apply DirectSum.degree_eq_of_mem_mem 𝒜 hb'

Premises used: DirectSum.degree_eq_of_mem_mem
-- 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
⊢ x ^ j ∈ 𝒜 (j • (d + e))

Tactic:
SetLike.pow_mem_graded _ _

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
hxj : SetLike.GradedMonoid 𝒜
hxj₁ : x ∈ 𝒜 (d + e)
⊢ (fun (x_1 : ℕ) ↦ x ^ x_1) j ∈ 𝒜 (j * (d + e))

Tactic:
convert! SetLike.pow_mem_graded _ _ 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
⊢ SetLike.GradedMonoid 𝒜

Tactic:
infer_instance
-- 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
⊢ x ∈ 𝒜 (d + e)

Tactic:
hx ▸ SetLike.mul_mem_graded hf hg

Premises used: SetLike.mul_mem_graded, Eq.rec, Eq.symm
-- 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
⊢ x ∈ 𝒜 (d + e)

Tactic:
exact hx ▸ SetLike.mul_mem_graded hf hg
-- 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
⊢ Ne.{u_2 + 1} (α := A) ((fun (x_1 : ℕ) ↦ x ^ x_1) j) 0

Tactic:
hx ▸ hfg

Premises used: Eq.rec, Eq.symm
-- 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
⊢ Ne.{u_2 + 1} (α := A) ((fun (x_1 : ℕ) ↦ x ^ x_1) j) 0

Tactic:
exact hx ▸ hfg
-- 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
⊢ n = j * (d + e)

Tactic:
have : n = j * (d + e) := by
    apply DirectSum.degree_eq_of_mem_mem 𝒜 hb'
    · convert! SetLike.pow_mem_graded _ _ using 2
      · infer_instance
      · exact hx ▸ SetLike.mul_mem_graded hf hg
    · exact hx ▸ hfg
-- 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)
⊢ a * g ^ (j * (d - 1)) ∈ 𝒜 (n + (j * (d - 1)) • e)

Tactic:
SetLike.mul_mem_graded ha (SetLike.pow_mem_graded _ hg)

Premises used: SetLike.mul_mem_graded, 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)
h : j * (d * (e + 1)) = n + (j * (d - 1)) • e
⊢ a * g ^ (j * (d - 1)) ∈ 𝒜 (j * (d * (e + 1)))

Tactic:
convert! SetLike.mul_mem_graded ha (SetLike.pow_mem_graded _ hg) using 2

Premises used: SetLike.mul_mem_graded, 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)
h : j * (d * (e + 1)) = j * (d + e) + (j * (d - 1)) • e
⊢ j * (d * (e + 1)) = n + (j * (d - 1)) • e

Tactic:
rw [this]
-- 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)
h :
  ∀ (hf : f ∈ 𝒜 0) (hd : LT.lt (α := ℕ) 0 0) (this : n = j * (0 + e)),
    j * (0 * (e + 1)) = j * (0 + e) + (j * HSub.hSub (α := ℕ) 0 1) • e
h₁ :
  ∀ (n_1 : ℕ) (hf : f ∈ 𝒜 (n_1 + 1)) (hd : 0 < n_1 + 1) (this : n = j * (n_1 + 1 + e)),
    j * ((n_1 + 1) * (e + 1)) = j * (n_1 + 1 + e) + (j * (n_1 + 1 - 1)) • e
⊢ j * (d * (e + 1)) = j * (d + e) + (j * (d - 1)) • e

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)
⊢ j * (0 * (e + 1)) = j * (0 + e) + (j * HSub.hSub (α := ℕ) 0 1) • e

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)
h : j * ((n_1 + 1) * (e + 1)) = j * (n_1 + 1 + e) + j * n_1 * e
⊢ j * ((n_1 + 1) * (e + 1)) = j * (n_1 + 1 + e) + (j * (n_1 + 1 - 1)) • e

Tactic:
simp
-- 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)
⊢ j * ((n_1 + 1) * (e + 1)) = j * (n_1 + 1 + e) + j * n_1 * 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)
⊢ f ^ (j * (e + 1)) ∈ 𝒜 ((j * (e + 1)) • d)

Tactic:
SetLike.pow_mem_graded _ hf

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)
h : j * (d * (e + 1)) = (j * (e + 1)) • d
⊢ f ^ (j * (e + 1)) ∈ 𝒜 (j * (d * (e + 1)))

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)
⊢ j * (d * (e + 1)) = (j * (e + 1)) • 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 := ⋯ }
⊢ f ^ (j * e) ∈ 𝒜 ((j * e) • d)

Tactic:
SetLike.pow_mem_graded _ hf

Premises used: SetLike.pow_mem_graded