awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme (goal)
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
f : A
x : ↥(pbo f)
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
this : Algebra (A⁰_ f) (AtPrime 𝒜 (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal) :=
  RingHom.toAlgebra (mapId 𝒜 ⋯)
y z : NumDenSameDeg 𝒜 (Submonoid.powers f)
e_1 :
  Eq (α := AtPrime 𝒜 (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal)
    ((algebraMap (A⁰_ f) (AtPrime 𝒜 (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal) :
          (a : A⁰_ f) → AtPrime 𝒜 (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal)
        (HomogeneousLocalization.mk y) :
      AtPrime 𝒜 (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal)
    ((algebraMap (A⁰_ f) (AtPrime 𝒜 (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal) :
          (a : A⁰_ f) → AtPrime 𝒜 (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal)
        (HomogeneousLocalization.mk z) :
      AtPrime 𝒜 (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal)
i : ℕ
c : A
hc : c ∈ 𝒜 i
hc' : c ∉ (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal
e : c * ((↑z.den : A) * (↑y.num : A)) = c * ((↑y.den : A) * (↑z.num : A))
⊢ (↑z.den : A) * (c ^ m * (↑y.num : A)) = (↑y.den : A) * (c ^ m * (↑z.num : A))
have toIsLocalizationMap : c ^ m * ((↑z.den : A) * (↑y.num : A)) = (↑y.den : A) * (c ^ m * (↑z.num : A))
Tactic: rw [mul_left_comm, mul_left_comm y.den.1, ← tsub_add_cancel_of_le (show 1 ≤ m from hm),
      pow_succ, mul_assoc, mul_assoc, e]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme (goal)
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
f : A
x : ↥(pbo f)
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
this : Algebra (A⁰_ f) (AtPrime 𝒜 (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal) :=
  RingHom.toAlgebra (mapId 𝒜 ⋯)
y z : NumDenSameDeg 𝒜 (Submonoid.powers f)
e_1 :
  Eq (α := AtPrime 𝒜 (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal)
    ((algebraMap (A⁰_ f) (AtPrime 𝒜 (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal) :
          (a : A⁰_ f) → AtPrime 𝒜 (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal)
        (HomogeneousLocalization.mk y) :
      AtPrime 𝒜 (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal)
    ((algebraMap (A⁰_ f) (AtPrime 𝒜 (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal) :
          (a : A⁰_ f) → AtPrime 𝒜 (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal)
        (HomogeneousLocalization.mk z) :
      AtPrime 𝒜 (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal)
i : ℕ
c : A
hc : c ∈ 𝒜 i
hc' : c ∉ (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal
e : c * ((↑z.den : A) * (↑y.num : A)) = c * ((↑y.den : A) * (↑z.num : A))
toIsLocalizationMap : c ^ m * ((↑z.den : A) * (↑y.num : A)) = (↑y.den : A) * (c ^ m * (↑z.num : A))
⊢ (↑z.den : A) * (c ^ m * (↑y.num : A)) = (↑y.den : A) * (c ^ m * (↑z.num : A))
have toIsLocalizationMap₁ : c ^ m * ((↑z.den : A) * (↑y.num : A)) = c ^ m * ((↑y.den : A) * (↑z.num : A))
Tactic: rw [mul_left_comm, mul_left_comm y.den.1, ← tsub_add_cancel_of_le (show 1 ≤ m from hm),
      pow_succ, mul_assoc, mul_assoc, e]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme (goal)
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
f : A
x : ↥(pbo f)
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
this : Algebra (A⁰_ f) (AtPrime 𝒜 (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal) :=
  RingHom.toAlgebra (mapId 𝒜 ⋯)
y z : NumDenSameDeg 𝒜 (Submonoid.powers f)
e_1 :
  Eq (α := AtPrime 𝒜 (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal)
    ((algebraMap (A⁰_ f) (AtPrime 𝒜 (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal) :
          (a : A⁰_ f) → AtPrime 𝒜 (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal)
        (HomogeneousLocalization.mk y) :
      AtPrime 𝒜 (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal)
    ((algebraMap (A⁰_ f) (AtPrime 𝒜 (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal) :
          (a : A⁰_ f) → AtPrime 𝒜 (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal)
        (HomogeneousLocalization.mk z) :
      AtPrime 𝒜 (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal)
i : ℕ
c : A
hc : c ∈ 𝒜 i
hc' : c ∉ (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal
e : c * ((↑z.den : A) * (↑y.num : A)) = c * ((↑y.den : A) * (↑z.num : A))
toIsLocalizationMap : c ^ m * ((↑z.den : A) * (↑y.num : A)) = (↑y.den : A) * (c ^ m * (↑z.num : A))
toIsLocalizationMap₁ : c ^ m * ((↑z.den : A) * (↑y.num : A)) = c ^ m * ((↑y.den : A) * (↑z.num : A))
⊢ (↑z.den : A) * (c ^ m * (↑y.num : A)) = (↑y.den : A) * (c ^ m * (↑z.num : A))
have toIsLocalizationMap₂ : c ^ (m - 1 + 1) * ((↑z.den : A) * (↑y.num : A)) = c ^ (m - 1 + 1) * ((↑y.den : A) * (↑z.num : A))
Tactic: rw [mul_left_comm, mul_left_comm y.den.1, ← tsub_add_cancel_of_le (show 1 ≤ m from hm),
      pow_succ, mul_assoc, mul_assoc, e]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme (goal)
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
f : A
x : ↥(pbo f)
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
this : Algebra (A⁰_ f) (AtPrime 𝒜 (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal) :=
  RingHom.toAlgebra (mapId 𝒜 ⋯)
y z : NumDenSameDeg 𝒜 (Submonoid.powers f)
e_1 :
  Eq (α := AtPrime 𝒜 (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal)
    ((algebraMap (A⁰_ f) (AtPrime 𝒜 (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal) :
          (a : A⁰_ f) → AtPrime 𝒜 (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal)
        (HomogeneousLocalization.mk y) :
      AtPrime 𝒜 (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal)
    ((algebraMap (A⁰_ f) (AtPrime 𝒜 (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal) :
          (a : A⁰_ f) → AtPrime 𝒜 (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal)
        (HomogeneousLocalization.mk z) :
      AtPrime 𝒜 (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal)
i : ℕ
c : A
hc : c ∈ 𝒜 i
hc' : c ∉ (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal
e : c * ((↑z.den : A) * (↑y.num : A)) = c * ((↑y.den : A) * (↑z.num : A))
toIsLocalizationMap : c ^ m * ((↑z.den : A) * (↑y.num : A)) = (↑y.den : A) * (c ^ m * (↑z.num : A))
toIsLocalizationMap₁ : c ^ m * ((↑z.den : A) * (↑y.num : A)) = c ^ m * ((↑y.den : A) * (↑z.num : A))
toIsLocalizationMap₂ : c ^ (m - 1 + 1) * ((↑z.den : A) * (↑y.num : A)) = c ^ (m - 1 + 1) * ((↑y.den : A) * (↑z.num : A))
⊢ (↑z.den : A) * (c ^ m * (↑y.num : A)) = (↑y.den : A) * (c ^ m * (↑z.num : A))
have toIsLocalizationMap₃ : c ^ (m - 1) * c * ((↑z.den : A) * (↑y.num : A)) = c ^ (m - 1) * c * ((↑y.den : A) * (↑z.num : A))
Tactic: rw [mul_left_comm, mul_left_comm y.den.1, ← tsub_add_cancel_of_le (show 1 ≤ m from hm),
      pow_succ, mul_assoc, mul_assoc, e]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme (goal)
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
f : A
x : ↥(pbo f)
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
this : Algebra (A⁰_ f) (AtPrime 𝒜 (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal) :=
  RingHom.toAlgebra (mapId 𝒜 ⋯)
y z : NumDenSameDeg 𝒜 (Submonoid.powers f)
e_1 :
  Eq (α := AtPrime 𝒜 (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal)
    ((algebraMap (A⁰_ f) (AtPrime 𝒜 (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal) :
          (a : A⁰_ f) → AtPrime 𝒜 (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal)
        (HomogeneousLocalization.mk y) :
      AtPrime 𝒜 (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal)
    ((algebraMap (A⁰_ f) (AtPrime 𝒜 (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal) :
          (a : A⁰_ f) → AtPrime 𝒜 (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal)
        (HomogeneousLocalization.mk z) :
      AtPrime 𝒜 (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal)
i : ℕ
c : A
hc : c ∈ 𝒜 i
hc' : c ∉ (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal
e : c * ((↑z.den : A) * (↑y.num : A)) = c * ((↑y.den : A) * (↑z.num : A))
toIsLocalizationMap : c ^ m * ((↑z.den : A) * (↑y.num : A)) = (↑y.den : A) * (c ^ m * (↑z.num : A))
toIsLocalizationMap₁ : c ^ m * ((↑z.den : A) * (↑y.num : A)) = c ^ m * ((↑y.den : A) * (↑z.num : A))
toIsLocalizationMap₂ : c ^ (m - 1 + 1) * ((↑z.den : A) * (↑y.num : A)) = c ^ (m - 1 + 1) * ((↑y.den : A) * (↑z.num : A))
toIsLocalizationMap₃ : c ^ (m - 1) * c * ((↑z.den : A) * (↑y.num : A)) = c ^ (m - 1) * c * ((↑y.den : A) * (↑z.num : A))
⊢ (↑z.den : A) * (c ^ m * (↑y.num : A)) = (↑y.den : A) * (c ^ m * (↑z.num : A))
have toIsLocalizationMap₄ : c ^ (m - 1) * (c * ((↑z.den : A) * (↑y.num : A))) = c ^ (m - 1) * c * ((↑y.den : A) * (↑z.num : A))
Tactic: rw [mul_left_comm, mul_left_comm y.den.1, ← tsub_add_cancel_of_le (show 1 ≤ m from hm),
      pow_succ, mul_assoc, mul_assoc, e]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme (goal)
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
f : A
x : ↥(pbo f)
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
this : Algebra (A⁰_ f) (AtPrime 𝒜 (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal) :=
  RingHom.toAlgebra (mapId 𝒜 ⋯)
y z : NumDenSameDeg 𝒜 (Submonoid.powers f)
e_1 :
  Eq (α := AtPrime 𝒜 (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal)
    ((algebraMap (A⁰_ f) (AtPrime 𝒜 (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal) :
          (a : A⁰_ f) → AtPrime 𝒜 (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal)
        (HomogeneousLocalization.mk y) :
      AtPrime 𝒜 (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal)
    ((algebraMap (A⁰_ f) (AtPrime 𝒜 (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal) :
          (a : A⁰_ f) → AtPrime 𝒜 (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal)
        (HomogeneousLocalization.mk z) :
      AtPrime 𝒜 (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal)
i : ℕ
c : A
hc : c ∈ 𝒜 i
hc' : c ∉ (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal
e : c * ((↑z.den : A) * (↑y.num : A)) = c * ((↑y.den : A) * (↑z.num : A))
toIsLocalizationMap : c ^ m * ((↑z.den : A) * (↑y.num : A)) = (↑y.den : A) * (c ^ m * (↑z.num : A))
toIsLocalizationMap₁ : c ^ m * ((↑z.den : A) * (↑y.num : A)) = c ^ m * ((↑y.den : A) * (↑z.num : A))
toIsLocalizationMap₂ : c ^ (m - 1 + 1) * ((↑z.den : A) * (↑y.num : A)) = c ^ (m - 1 + 1) * ((↑y.den : A) * (↑z.num : A))
toIsLocalizationMap₃ : c ^ (m - 1) * c * ((↑z.den : A) * (↑y.num : A)) = c ^ (m - 1) * c * ((↑y.den : A) * (↑z.num : A))
toIsLocalizationMap₄ :
  c ^ (m - 1) * (c * ((↑z.den : A) * (↑y.num : A))) = c ^ (m - 1) * c * ((↑y.den : A) * (↑z.num : A))
⊢ (↑z.den : A) * (c ^ m * (↑y.num : A)) = (↑y.den : A) * (c ^ m * (↑z.num : A))
have toIsLocalizationMap₅ : c ^ (m - 1) * (c * ((↑z.den : A) * (↑y.num : A))) = c ^ (m - 1) * (c * ((↑y.den : A) * (↑z.num : A)))
Tactic: rw [mul_left_comm, mul_left_comm y.den.1, ← tsub_add_cancel_of_le (show 1 ≤ m from hm),
      pow_succ, mul_assoc, mul_assoc, e]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme (goal)
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
f : A
x : ↥(pbo f)
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
this : Algebra (A⁰_ f) (AtPrime 𝒜 (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal) :=
  RingHom.toAlgebra (mapId 𝒜 ⋯)
y z : NumDenSameDeg 𝒜 (Submonoid.powers f)
e_1 :
  Eq (α := AtPrime 𝒜 (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal)
    ((algebraMap (A⁰_ f) (AtPrime 𝒜 (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal) :
          (a : A⁰_ f) → AtPrime 𝒜 (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal)
        (HomogeneousLocalization.mk y) :
      AtPrime 𝒜 (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal)
    ((algebraMap (A⁰_ f) (AtPrime 𝒜 (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal) :
          (a : A⁰_ f) → AtPrime 𝒜 (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal)
        (HomogeneousLocalization.mk z) :
      AtPrime 𝒜 (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal)
i : ℕ
c : A
hc : c ∈ 𝒜 i
hc' : c ∉ (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal
e : c * ((↑z.den : A) * (↑y.num : A)) = c * ((↑y.den : A) * (↑z.num : A))
toIsLocalizationMap : c ^ m * ((↑z.den : A) * (↑y.num : A)) = (↑y.den : A) * (c ^ m * (↑z.num : A))
toIsLocalizationMap₁ : c ^ m * ((↑z.den : A) * (↑y.num : A)) = c ^ m * ((↑y.den : A) * (↑z.num : A))
toIsLocalizationMap₂ : c ^ (m - 1 + 1) * ((↑z.den : A) * (↑y.num : A)) = c ^ (m - 1 + 1) * ((↑y.den : A) * (↑z.num : A))
toIsLocalizationMap₃ : c ^ (m - 1) * c * ((↑z.den : A) * (↑y.num : A)) = c ^ (m - 1) * c * ((↑y.den : A) * (↑z.num : A))
toIsLocalizationMap₄ :
  c ^ (m - 1) * (c * ((↑z.den : A) * (↑y.num : A))) = c ^ (m - 1) * c * ((↑y.den : A) * (↑z.num : A))
toIsLocalizationMap₅ :
  c ^ (m - 1) * (c * ((↑z.den : A) * (↑y.num : A))) = c ^ (m - 1) * (c * ((↑y.den : A) * (↑z.num : A)))
⊢ (↑z.den : A) * (c ^ m * (↑y.num : A)) = (↑y.den : A) * (c ^ m * (↑z.num : A))
have toIsLocalizationMap₆ : c ^ (m - 1) * (c * ((↑y.den : A) * (↑z.num : A))) = c ^ (m - 1) * (c * ((↑y.den : A) * (↑z.num : A)))
Tactic: rw [mul_left_comm, mul_left_comm y.den.1, ← tsub_add_cancel_of_le (show 1 ≤ m from hm),
      pow_succ, mul_assoc, mul_assoc, e]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme (hypothesis)
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
⊢ IsIso (X := Proj.restrict (U := Functor.obj (C := Opens (↑Proj.T : Type u_1)) (Opens.toTopCat Proj.T) (pbo f)) ⋯)
    (toSpec 𝒜 f)
have this : IsIso (X :=
  (↑(Proj.restrict (U := Functor.obj (C := Opens (↑Proj.T : Type u_1)) (Opens.toTopCat Proj.T) (pbo f))
          sorry).toPresheafedSpace :
    TopCat))
  (PresheafedSpace.Hom.base (LocallyRingedSpace.Hom.toHom (toSpec 𝒜 f)))
Tactic: haveI : IsIso (toSpec 𝒜 f).base := toSpec_base_isIso 𝒜 f_deg hm
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme (goal)
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
this :
  IsIso (X :=
    (↑(Proj.restrict (U := Functor.obj (C := Opens (↑Proj.T : Type u_1)) (Opens.toTopCat Proj.T) (pbo f))
            ⋯).toPresheafedSpace :
      TopCat))
    (PresheafedSpace.Hom.base (LocallyRingedSpace.Hom.toHom (toSpec 𝒜 f)))
x :
  (↑(Proj.restrict (U := Functor.obj (C := Opens (↑Proj.T : Type u_1)) (Opens.toTopCat Proj.T) (pbo f)) ⋯).toTopCat :
    Type u_1)
⊢ IsIso (X :=
    (Spec A⁰_ f).presheaf.stalk
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC := carrier)
            (X :=
            (↑(Proj.restrict (U := Functor.obj (C := Opens (↑Proj.T : Type u_1)) (Opens.toTopCat Proj.T) (pbo f))
                    ⋯).toPresheafedSpace :
              TopCat))
            (PresheafedSpace.Hom.base (LocallyRingedSpace.Hom.toHom (toSpec 𝒜 f))) :
          (a : (↑(↑(Proj.restrict ⋯).toPresheafedSpace : TopCat) : Type u_1)) →
            (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1))
        x))
    (LocallyRingedSpace.Hom.stalkMap (toSpec 𝒜 f) x)
have rw : IsIso (X :=
  (Spec A⁰_ f).presheaf.stalk
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC := carrier) (X :=
          (↑(Proj.restrict (U := Functor.obj (C := Opens (↑Proj.T : Type u_1)) (Opens.toTopCat Proj.T) (pbo f))
                  sorry).toPresheafedSpace :
            TopCat))
          (PresheafedSpace.Hom.base (LocallyRingedSpace.Hom.toHom (toSpec 𝒜 f))) :
        (a : (↑(↑(Proj.restrict sorry).toPresheafedSpace : TopCat) : Type u_1)) →
          (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1))
      x))
  (Y :=
  (Proj.restrict (U := Functor.obj (C := Opens (↑Proj.T : Type u_1)) (Opens.toTopCat Proj.T) (pbo f)) sorry).presheaf.stalk
    x)
  (Iso.hom (specStalkEquiv 𝒜 f x f_deg hm) ≫
    Iso.inv (RingEquiv.toCommRingCatIso («Proj».stalkIso' 𝒜 (↑x : ProjectiveSpectrum 𝒜))) ≫
      Iso.inv (Proj.restrictStalkIso sorry x))
Tactic: rw [stalkMap_toSpec 𝒜 f x f_deg hm]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme (hypothesis)
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
this :
  IsIso (X :=
    (↑(Proj.restrict (U := Functor.obj (C := Opens (↑Proj.T : Type u_1)) (Opens.toTopCat Proj.T) (pbo f))
            ⋯).toPresheafedSpace :
      TopCat))
    (PresheafedSpace.Hom.base (LocallyRingedSpace.Hom.toHom (toSpec 𝒜 f)))
⊢ IsIso (X := Proj.restrict (U := Functor.obj (C := Opens (↑Proj.T : Type u_1)) (Opens.toTopCat Proj.T) (pbo f)) ⋯)
    (toSpec 𝒜 f)
have x : ∀
  (x :
    (↑(Proj.restrict (U := Functor.obj (C := Opens (↑Proj.T : Type u_1)) (Opens.toTopCat Proj.T) (pbo f)) sorry).toTopCat :
      Type u_1)),
  IsIso (X :=
    (Spec A⁰_ f).presheaf.stalk
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC := carrier)
            (X :=
            (↑(Proj.restrict (U := Functor.obj (C := Opens (↑Proj.T : Type u_1)) (Opens.toTopCat Proj.T) (pbo f))
                    sorry).toPresheafedSpace :
              TopCat))
            (PresheafedSpace.Hom.base (LocallyRingedSpace.Hom.toHom (toSpec 𝒜 f))) :
          (a : (↑(↑(Proj.restrict sorry).toPresheafedSpace : TopCat) : Type u_1)) →
            (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1))
        x))
    (LocallyRingedSpace.Hom.stalkMap (toSpec 𝒜 f) x)
Tactic: haveI _ (x) : IsIso ((toSpec 𝒜 f).stalkMap x) := by
    rw [stalkMap_toSpec 𝒜 f x f_deg hm]; infer_instance
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme (hypothesis)
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
this :
  IsIso (X :=
    (↑(Proj.restrict (U := Functor.obj (C := Opens (↑Proj.T : Type u_1)) (Opens.toTopCat Proj.T) (pbo f))
            ⋯).toPresheafedSpace :
      TopCat))
    (PresheafedSpace.Hom.base (LocallyRingedSpace.Hom.toHom (toSpec 𝒜 f)))
h :
  ∀
    (x :
      (↑(Proj.restrict (U := Functor.obj (C := Opens (↑Proj.T : Type u_1)) (Opens.toTopCat Proj.T) (pbo f))
              ⋯).toTopCat :
        Type u_1)),
    IsIso (X :=
      (Spec A⁰_ f).presheaf.stalk
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC := carrier)
              (X :=
              (↑(Proj.restrict (U := Functor.obj (C := Opens (↑Proj.T : Type u_1)) (Opens.toTopCat Proj.T) (pbo f))
                      ⋯).toPresheafedSpace :
                TopCat))
              (PresheafedSpace.Hom.base (LocallyRingedSpace.Hom.toHom (toSpec 𝒜 f))) :
            (a : (↑(↑(Proj.restrict ⋯).toPresheafedSpace : TopCat) : Type u_1)) →
              (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1))
          x))
      (LocallyRingedSpace.Hom.stalkMap (toSpec 𝒜 f) x)
⊢ IsIso (X := Proj.restrict (U := Functor.obj (C := Opens (↑Proj.T : Type u_1)) (Opens.toTopCat Proj.T) (pbo f)) ⋯)
    (toSpec 𝒜 f)
have this₁ : LocallyRingedSpace.IsOpenImmersion (X :=
  Proj.restrict (U := Functor.obj (C := Opens (↑Proj.T : Type u_1)) (Opens.toTopCat Proj.T) (pbo f)) sorry) (toSpec 𝒜 f)
Tactic: haveI : LocallyRingedSpace.IsOpenImmersion (toSpec 𝒜 f) :=
    LocallyRingedSpace.IsOpenImmersion.of_stalk_iso (toSpec 𝒜 f)
      (TopCat.homeoOfIso (asIso <| (toSpec 𝒜 f).base)).isOpenEmbedding
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme (goal)
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
x : (↑Proj.T : Type u_1)
⊢ ∃ (f : A) (m : ℕ) (_ : f ∈ 𝒜 m) (_ : 0 < m), f ∉ x.asHomogeneousIdeal
have by_contra! : ∀ (this : ∀ (f : A) (m : ℕ), f ∈ 𝒜 m → 0 < m → f ∈ x.asHomogeneousIdeal), False
Tactic: by_contra!
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme (goal)
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
x : (↑Proj.T : Type u_1)
this : ∀ (f : A) (m : ℕ), f ∈ 𝒜 m → 0 < m → f ∈ x.asHomogeneousIdeal
⊢ False
have refine : ∀ (z : A) (hz : Membership.mem (γ := HomogeneousIdeal 𝒜) (HomogeneousIdeal.irrelevant 𝒜) z), z ∈ x.asHomogeneousIdeal
Tactic: refine x.not_irrelevant_le fun z hz ↦ ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme (goal)
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
x : (↑Proj.T : Type u_1)
this : ∀ (f : A) (m : ℕ), f ∈ 𝒜 m → 0 < m → f ∈ x.asHomogeneousIdeal
z : A
hz : Membership.mem (γ := HomogeneousIdeal 𝒜) (HomogeneousIdeal.irrelevant 𝒜) z
⊢ z ∈ x.asHomogeneousIdeal
have rw : ∑ i ∈ DFinsupp.support (β := fun (i : ℕ) ↦ ↥(𝒜 i)) ((decompose 𝒜 : (a : A) → ⨁ (i : ℕ), ↥(𝒜 i)) z),
    (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ℕ), ↥(𝒜 i)) z : ⨁ (i : ℕ), ↥(𝒜 i)) : (a : ℕ) → ↥(𝒜 a)) i) : A) ∈
  x.asHomogeneousIdeal
Tactic: rw [← DirectSum.sum_support_decompose 𝒜 z]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme (goal)
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
x : (↑Proj.T : Type u_1)
⊢ ∃ (U : OpenNhds x) (R : CommRingCat.{u_1}),
    Nonempty.{u_1 + 1} (Proj.restrict ⋯ ≅ «Spec».toLocallyRingedSpace.obj (op R))
have obtain : ∀ (f : A) (m : ℕ) (f_deg : f ∈ 𝒜 m) (hm : 0 < m) (hx : f ∉ x.asHomogeneousIdeal),
  ∃ (U : OpenNhds x) (R : CommRingCat.{u_1}),
    Nonempty.{u_1 + 1} (Proj.restrict sorry ≅ «Spec».toLocallyRingedSpace.obj (op R))
Tactic: obtain ⟨f, m, f_deg, hm, hx⟩ : ∃ (f : A) (m : ℕ) (_ : f ∈ 𝒜 m) (_ : 0 < m), f ∉ x.1 := by
      by_contra!
      refine x.not_irrelevant_le fun z hz ↦ ?_
      rw [← DirectSum.sum_support_decompose 𝒜 z]
      exact x.1.toIdeal.sum_mem fun k hk ↦ this _ k (SetLike.coe_mem _) <| by_contra <| by aesop
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme (goal)
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
x : (↑Proj.T : Type u_1)
⊢ ∃ (U : OpenNhds x) (R : CommRingCat.{u_1}),
    Nonempty.{u_1 + 1} (Proj.restrict ⋯ ≅ «Spec».toLocallyRingedSpace.obj (op R))
have obtain : ∃ (f : A) (m : ℕ) (_ : f ∈ 𝒜 m) (_ : 0 < m), f ∉ x.asHomogeneousIdeal
Tactic: classical
    obtain ⟨f, m, f_deg, hm, hx⟩ : ∃ (f : A) (m : ℕ) (_ : f ∈ 𝒜 m) (_ : 0 < m), f ∉ x.1 := by
      by_contra!
      refine x.not_irrelevant_le fun z hz ↦ ?_
      rw [← DirectSum.sum_support_decompose 𝒜 z]
      exact x.1.toIdeal.sum_mem fun k hk ↦ this _ k (SetLike.coe_mem _) <| by_contra <| by aesop
    exact ⟨⟨pbo f, hx⟩, .of (A⁰_ f), ⟨projIsoSpec 𝒜 f f_deg hm⟩⟩