awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor (goal)
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 (ℬ₊))
⊢ Eq (α := Proj 𝒞 ⟶ Proj 𝒜) (map (g.comp f) ⋯) (CategoryStruct.comp (Y := Proj ℬ) (map g hg) (map f hf))
have refine : ∀
  (s :
    PreZeroHypercover.I₀ (S := Proj 𝒞)
      (Precoverage.ZeroHypercover.toPreZeroHypercover
        (Scheme.AffineOpenCover.openCover (mapAffineOpenCover (g.comp f) sorry)))),
  Eq (α :=
    PreZeroHypercover.X
        (Precoverage.ZeroHypercover.toPreZeroHypercover
          (Scheme.AffineOpenCover.openCover (mapAffineOpenCover (g.comp f) sorry)))
        s ⟶
      Proj 𝒜)
    (PreZeroHypercover.f
        (Precoverage.ZeroHypercover.toPreZeroHypercover
          (Scheme.AffineOpenCover.openCover (mapAffineOpenCover (g.comp f) sorry)))
        s ≫
      map (g.comp f) sorry)
    (PreZeroHypercover.f
        (Precoverage.ZeroHypercover.toPreZeroHypercover
          (Scheme.AffineOpenCover.openCover (mapAffineOpenCover (g.comp f) sorry)))
        s ≫
      CategoryStruct.comp (Y := Proj ℬ) (map g hg) (map f hf))
Tactic: refine (mapAffineOpenCover _ <| irrelevant_le_map_comp hf hg).openCover.hom_ext _ _ fun s ↦ ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor (goal)
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 (ℬ₊))
s :
  PreZeroHypercover.I₀ (S := Proj 𝒞)
    (Precoverage.ZeroHypercover.toPreZeroHypercover
      (Scheme.AffineOpenCover.openCover (mapAffineOpenCover (g.comp f) ⋯)))
⊢ Eq (α :=
    PreZeroHypercover.X
        (Precoverage.ZeroHypercover.toPreZeroHypercover
          (Scheme.AffineOpenCover.openCover (mapAffineOpenCover (g.comp f) ⋯)))
        s ⟶
      Proj 𝒜)
    (PreZeroHypercover.f
        (Precoverage.ZeroHypercover.toPreZeroHypercover
          (Scheme.AffineOpenCover.openCover (mapAffineOpenCover (g.comp f) ⋯)))
        s ≫
      map (g.comp f) ⋯)
    (PreZeroHypercover.f
        (Precoverage.ZeroHypercover.toPreZeroHypercover
          (Scheme.AffineOpenCover.openCover (mapAffineOpenCover (g.comp f) ⋯)))
        s ≫
      CategoryStruct.comp (Y := Proj ℬ) (map g hg) (map f hf))
have simp : Eq (α := Spec (Scheme.AffineCover.X (P := IsOpenImmersion) (mapAffineOpenCover (g.comp f) sorry) s) ⟶ Proj 𝒜)
  (Spec.map (CommRingCat.ofHom (Away.map (g.comp f) (↑(s.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A))) ≫
    awayι 𝒜 (↑(s.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A) sorry sorry)
  (awayι 𝒞 ((g.comp f : (a : A) → C) (↑(s.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A)) sorry sorry ≫
    CategoryStruct.comp (Y := Proj ℬ) (map g hg) (map f hf))
Tactic: simp only [Scheme.AffineOpenCover.openCover_X, Scheme.AffineOpenCover.openCover_f,
    mapAffineOpenCover_f, awayι_comp_map (g.comp f) _ s.1.2 _ s.2.2]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor (goal)
Goal:
A σ : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
⊢ map (GradedRingHom.id 𝒜) ⋯ = 𝟙 (Proj 𝒜)
have 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 𝒜) sorry =
    PreZeroHypercover.f
        (Precoverage.ZeroHypercover.toPreZeroHypercover (Scheme.AffineOpenCover.openCover (affineOpenCover 𝒜))) s ≫
      𝟙 (Proj 𝒜)
Tactic: refine (affineOpenCover _).openCover.hom_ext _ _ fun s ↦ ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor (goal)
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 𝒜)))
⊢ PreZeroHypercover.f
        (Precoverage.ZeroHypercover.toPreZeroHypercover (Scheme.AffineOpenCover.openCover (affineOpenCover 𝒜))) s ≫
      map (GradedRingHom.id 𝒜) ⋯ =
    PreZeroHypercover.f
        (Precoverage.ZeroHypercover.toPreZeroHypercover (Scheme.AffineOpenCover.openCover (affineOpenCover 𝒜))) s ≫
      𝟙 (Proj 𝒜)
have 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) sorry sorry
Tactic: convert! awayι_comp_map (.id 𝒜) _ _ _ s.2.2 using 1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper (goal)
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
⊢ ∃ (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
have 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 sorry) sorry :
              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 := sorry } :
        HomogeneousLocalization 𝒜 (Submonoid.powers x))
Tactic: obtain ⟨⟨n, ⟨a, ha⟩, ⟨b, hb'⟩, ⟨j, (rfl : _ = b)⟩⟩, rfl⟩ := mk_surjective z
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper (goal)
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
⊢ ∃ (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))
have 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 sorry) sorry :
              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 := sorry } :
        HomogeneousLocalization 𝒜 (Submonoid.powers x))
Tactic: by_cases hfg : (f * g) ^ j = 0
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper (goal)
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))
⊢ ∃ (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))
have 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 sorry) sorry :
              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 := sorry } :
        HomogeneousLocalization 𝒜 (Submonoid.powers x))
Tactic: by_cases hfg : (f * g) ^ j = 0
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper (goal)
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
⊢ ∃ (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))
have h : Eq (α := Away 𝒜 x)
  (((Algebra.TensorProduct.lift (awayMapₐ 𝒜 hg hx) (awayMapₐ 𝒜 hf sorry) sorry :
        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 := sorry })
Tactic: use 0
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper (hypothesis)
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
⊢ 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 := ⋯ })
have this : Subsingleton.{max (u_2 + 1) 1} (HomogeneousLocalization 𝒜 (Submonoid.powers x))
Tactic: have := HomogeneousLocalization.subsingleton 𝒜 (x := Submonoid.powers x) ⟨j, hx ▸ hfg⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper (goal)
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)
have hxj : (fun (x_1 : ℕ) ↦ x ^ x_1) j ∈ 𝒜 (j * (d + e))
Tactic: apply DirectSum.degree_eq_of_mem_mem 𝒜 hb'
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper (goal)
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))
⊢ n = j * (d + e)
have hx₁ : Ne.{u_2 + 1} (α := A) ((fun (x_1 : ℕ) ↦ x ^ x_1) j) 0
Tactic: apply DirectSum.degree_eq_of_mem_mem 𝒜 hb'
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper (goal)
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
⊢ (fun (x_1 : ℕ) ↦ x ^ x_1) j ∈ 𝒜 (j * (d + e))
have hxj : SetLike.GradedMonoid 𝒜
Tactic: convert! SetLike.pow_mem_graded _ _ using 2
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper (goal)
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 𝒜
⊢ (fun (x_1 : ℕ) ↦ x ^ x_1) j ∈ 𝒜 (j * (d + e))
have hxj₁ : x ∈ 𝒜 (d + e)
Tactic: convert! SetLike.pow_mem_graded _ _ using 2
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper (hypothesis)
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
⊢ ∃ (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))
have this : 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
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper (goal)
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)) ∈ 𝒜 (j * (d * (e + 1)))
have h : j * (d * (e + 1)) = n + (j * (d - 1)) • e
Tactic: convert! SetLike.mul_mem_graded ha (SetLike.pow_mem_graded _ hg) using 2
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper (goal)
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)) = n + (j * (d - 1)) • e
have h : j * (d * (e + 1)) = j * (d + e) + (j * (d - 1)) • e
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper (goal)
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 * (d + e) + (j * (d - 1)) • e
have 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
Tactic: cases d
Cleared hypotheses: d, hf, hd, this
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper (goal)
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
⊢ j * (d * (e + 1)) = j * (d + e) + (j * (d - 1)) • e
have 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
Tactic: cases d
Cleared hypotheses: d, hf, hd, this
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper (goal)
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 + 1 - 1)) • e
have h : j * ((n_1 + 1) * (e + 1)) = j * (n_1 + 1 + e) + j * n_1 * e
Tactic: simp
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper (goal)
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 * (d * (e + 1)))
have h : j * (d * (e + 1)) = (j * (e + 1)) • d
Tactic: convert! SetLike.pow_mem_graded _ hf using 2
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper (goal)
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 * (d * e))
have h : j * (d * e) = (j * e) • d
Tactic: convert! SetLike.pow_mem_graded _ hf using 2
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper (goal)
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))
have h : j * (d * e) = (j * d) • e
Tactic: convert! SetLike.pow_mem_graded _ hg using 2