awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 := ⋯ }
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 := ⋯ }
⊢ ∃ (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)
      (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 := sorry } :
    HomogeneousLocalization 𝒜 (Submonoid.powers x))
Tactic: use mk x0 ⊗ₜ mk y0
-- 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 := ⋯ }
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 := ⋯ }
⊢ 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))
have h : Eq (α := Localization (Submonoid.powers x))
  (val.{0, u_2, u_1} (ι := ℕ) (σ := σ) (𝒜 := 𝒜)
    (((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)
      (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 := sorry :
        NumDenSameDeg 𝒜 (Submonoid.powers x) }))
Tactic: ext
-- 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 := ⋯ }
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 := ⋯ }
⊢ 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) }))
have 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)))
        sorry *
      Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1) (x ^ (j * d)) sorry))
  (Localization.mk a
    (Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1) (x ^ j) sorry))
Tactic: simp only [Algebra.TensorProduct.lift_tmul, awayMapₐ_apply, val_mul,
    val_awayMap_mk, Localization.mk_mul, val_mk, x0, y0]
-- 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 := ⋯ }
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 := ⋯ }
⊢ 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) ⋯))
have 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) sorry).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))) sorry *
              Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1) (x ^ (j * d))
                sorry).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))) sorry *
                  Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1)
                    (x ^ (j * d)) sorry).2 :
          A) *
        (a, Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1) (x ^ j) sorry).1)
Tactic: rw [Localization.mk_eq_mk_iff, Localization.r_iff_exists]
-- 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 := ⋯ }
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 := ⋯ }
⊢ ∃ (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)
have h : (↑1 : A) *
    ((↑(a, Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1) (x ^ j) sorry).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))) sorry *
            Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1) (x ^ (j * d))
              sorry).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))) sorry *
                Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1)
                  (x ^ (j * d)) sorry).2 :
        A) *
      (a, Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1) (x ^ j) sorry).1)
Tactic: use 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
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 := ⋯ }
⊢ (↑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)
have 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
Tactic: simp only [OneMemClass.coe_one, one_mul, Submonoid.mk_mul_mk]
-- 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 := ⋯ }
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 := ⋯ }
⊢ 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
have 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
Tactic: cases d
Cleared hypotheses: d, hf, hd, this, x0, y0
-- 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 := ⋯ }
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
⊢ 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
have 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
Tactic: cases d
Cleared hypotheses: d, hf, hd, this, x0, y0
-- 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)
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 := ⋯ }
⊢ 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
have 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
Tactic: simp only [hx, add_tsub_cancel_right]
-- 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 𝒜
⊢ IsSeparated (X := Proj 𝒜) (toSpecZero 𝒜)
have refine : ∀
  (i :
    (Precoverage.ZeroHypercover.toPreZeroHypercover
        (Pullback.openCoverOfLeftRight (AffineOpenCover.openCover (affineOpenCover 𝒜))
          (AffineOpenCover.openCover (affineOpenCover 𝒜)) (toSpecZero 𝒜) (toSpecZero 𝒜))).1),
  IsClosedImmersion (X :=
    PreZeroHypercover.X (S := Proj 𝒜)
      (Precoverage.ZeroHypercover.toPreZeroHypercover
        (Precoverage.ZeroHypercover.pullback₁ (T := diagonalObj (X := Proj 𝒜) (toSpecZero 𝒜)) (diagonal (toSpecZero 𝒜))
          (Pullback.openCoverOfLeftRight (AffineOpenCover.openCover (affineOpenCover 𝒜))
            (AffineOpenCover.openCover (affineOpenCover 𝒜)) (toSpecZero 𝒜) (toSpecZero 𝒜))))
      i)
    (Cover.pullbackHom (P := IsOpenImmersion)
        (Pullback.openCoverOfLeftRight (AffineOpenCover.openCover (affineOpenCover 𝒜))
          (AffineOpenCover.openCover (affineOpenCover 𝒜)) (toSpecZero 𝒜) (toSpecZero 𝒜))
        (diagonal (toSpecZero 𝒜)) i :
      PreZeroHypercover.X (S := Proj 𝒜)
          (Precoverage.ZeroHypercover.toPreZeroHypercover
            (Precoverage.ZeroHypercover.pullback₁ (T := diagonalObj (X := Proj 𝒜) (toSpecZero 𝒜))
              (diagonal (toSpecZero 𝒜))
              (Pullback.openCoverOfLeftRight (AffineOpenCover.openCover (affineOpenCover 𝒜))
                (AffineOpenCover.openCover (affineOpenCover 𝒜)) (toSpecZero 𝒜) (toSpecZero 𝒜))))
          i ⟶
        PreZeroHypercover.X (S := diagonalObj (X := Proj 𝒜) (toSpecZero 𝒜))
          (Precoverage.ZeroHypercover.toPreZeroHypercover
            (Pullback.openCoverOfLeftRight (AffineOpenCover.openCover (affineOpenCover 𝒜))
              (AffineOpenCover.openCover (affineOpenCover 𝒜)) (toSpecZero 𝒜) (toSpecZero 𝒜)))
          i)
Tactic: refine ⟨IsZariskiLocalAtTarget.of_openCover (Pullback.openCoverOfLeftRight
    (affineOpenCover 𝒜).openCover (affineOpenCover 𝒜).openCover _ _) ?_⟩
-- 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 𝒜
i j :
  PreZeroHypercover.I₀ (S := Proj 𝒜)
    (Precoverage.ZeroHypercover.toPreZeroHypercover (AffineOpenCover.openCover (affineOpenCover 𝒜)))
⊢ pullback (AffineCover.f (P := IsOpenImmersion) (affineOpenCover 𝒜) i ≫ toSpecZero 𝒜)
      (AffineCover.f (P := IsOpenImmersion) (affineOpenCover 𝒜) j ≫ toSpecZero 𝒜) ≅
    Spec
      (CommRingCat.of
        (Away 𝒜 (↑(i.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A) ⊗[↥(𝒜 0)]
          Away 𝒜 (↑(j.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A)))
have refine_1 : AffineCover.f (P := IsOpenImmersion) (affineOpenCover 𝒜) i ≫ toSpecZero 𝒜 =
  Spec.map (CommRingCat.ofHom (algebraMap (↥(𝒜 0)) (Away 𝒜 (↑(i.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A))))
Tactic: refine pullback.congrHom ?_ ?_ ≪≫ pullbackSpecIso (𝒜 0) (Away 𝒜 (i.2 : A)) (Away 𝒜 (j.2 : A))
-- 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 𝒜
i j :
  PreZeroHypercover.I₀ (S := Proj 𝒜)
    (Precoverage.ZeroHypercover.toPreZeroHypercover (AffineOpenCover.openCover (affineOpenCover 𝒜)))
refine_1 :
  AffineCover.f (P := IsOpenImmersion) (affineOpenCover 𝒜) i ≫ toSpecZero 𝒜 =
    Spec.map (CommRingCat.ofHom (algebraMap (↥(𝒜 0)) (Away 𝒜 (↑(i.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A))))
⊢ pullback (AffineCover.f (P := IsOpenImmersion) (affineOpenCover 𝒜) i ≫ toSpecZero 𝒜)
      (AffineCover.f (P := IsOpenImmersion) (affineOpenCover 𝒜) j ≫ toSpecZero 𝒜) ≅
    Spec
      (CommRingCat.of
        (Away 𝒜 (↑(i.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A) ⊗[↥(𝒜 0)]
          Away 𝒜 (↑(j.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A)))
have refine_2 : AffineCover.f (P := IsOpenImmersion) (affineOpenCover 𝒜) j ≫ toSpecZero 𝒜 =
  Spec.map (CommRingCat.ofHom (algebraMap (↥(𝒜 0)) (Away 𝒜 (↑(j.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A))))
Tactic: refine pullback.congrHom ?_ ?_ ≪≫ pullbackSpecIso (𝒜 0) (Away 𝒜 (i.2 : A)) (Away 𝒜 (j.2 : A))
-- 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 𝒜
i j :
  PreZeroHypercover.I₀ (S := Proj 𝒜)
    (Precoverage.ZeroHypercover.toPreZeroHypercover (AffineOpenCover.openCover (affineOpenCover 𝒜)))
⊢ AffineCover.f (P := IsOpenImmersion) (affineOpenCover 𝒜) i ≫ toSpecZero 𝒜 =
    Spec.map (CommRingCat.ofHom (algebraMap (↥(𝒜 0)) (Away 𝒜 (↑(i.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A))))
have refine_1 : Eq.{u_2 + 1} (α :=
  Spec (CommRingCat.of (Away 𝒜 (↑(i.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A))) ⟶ Spec (CommRingCat.of ↥(𝒜 0)))
  (Spec.map
    (CommRingCat.ofHom (fromZeroRingHom 𝒜 (Submonoid.powers (↑(i.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A)))))
  (Spec.map (CommRingCat.ofHom (algebraMap (↥(𝒜 0)) (Away 𝒜 (↑(i.snd (β := fun (i : ℕ+) ↦ ↥(𝒜 (↑i : ℕ)))) : A)))))
Tactic: simp [affineOpenCover, affineOpenCoverOfIrrelevantLESpan, awayι_toSpecZero]