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
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
a : A
h₁ :
  Eq (α := Set ↥(pbo f))
    (Subtype.val (p := fun (x : ProjectiveSpectrum 𝒜) ↦
        Membership.mem (γ := Opens (ProjectiveSpectrum 𝒜)) (pbo f) x) ⁻¹'
      (↑(pbo a) : Set (ProjectiveSpectrum 𝒜)))
    (⋃ (i : ℕ),
      Subtype.val (p := fun (x : ProjectiveSpectrum 𝒜) ↦
          Membership.mem (γ := Opens (ProjectiveSpectrum 𝒜)) (pbo f) x) ⁻¹'
        (↑(pbo (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ℕ), ↥(𝒜 i)) a : ⨁ (i : ℕ), ↥(𝒜 i)) : (a : ℕ) → ↥(𝒜 a)) i) : A)) :
          Set (ProjectiveSpectrum 𝒜)))
e : (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1) ≃
  (↑(↑(Proj.restrict (U := Functor.obj (C := Opens (↑Proj.T : Type u_1)) (Opens.toTopCat Proj.T) (pbo f))
              ⋯).toPresheafedSpace :
        TopCat) :
    Type u_1) :=
  { toFun := FromSpec.toFun f_deg hm, invFun := ToSpec.toFun f, left_inv := ⋯, right_inv := ⋯ }
⊢ IsOpen (X := (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1))
    (Set.preimage (β :=
      (↑(↑(Proj.restrict (U := Functor.obj (C := Opens (↑Proj.T : Type u_1)) (Opens.toTopCat Proj.T) (pbo f))
                  ⋯).toPresheafedSpace :
            TopCat) :
        Type u_1))
      (⇑e :
        (a : (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1)) →
          (↑(↑(Proj.restrict ⋯).toPresheafedSpace : TopCat) : Type u_1))
      (Subtype.val (p := fun (x : ProjectiveSpectrum 𝒜) ↦
          Membership.mem (γ := Opens (ProjectiveSpectrum 𝒜)) (pbo f) x) ⁻¹'
        (fun (r : A) ↦ (↑(pbo r) : Set (ProjectiveSpectrum 𝒜))) a))
have rw : IsOpen.{u_1} (X := (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1))
  (⋃ (i : ℕ),
    Set.image (α :=
      (↑(↑(Proj.restrict (U := Functor.obj (C := Opens (↑Proj.T : Type u_1)) (Opens.toTopCat Proj.T) (pbo f))
                  sorry).toPresheafedSpace :
            TopCat) :
        Type u_1))
      (⇑e.symm :
        (a : (↑(↑(Proj.restrict sorry).toPresheafedSpace : TopCat) : Type u_1)) →
          (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1))
      (Subtype.val (p := fun (x : ProjectiveSpectrum 𝒜) ↦
          Membership.mem (γ := Opens (ProjectiveSpectrum 𝒜)) (pbo f) x) ⁻¹'
        (↑(pbo (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ℕ), ↥(𝒜 i)) a : ⨁ (i : ℕ), ↥(𝒜 i)) : (a : ℕ) → ↥(𝒜 a)) i) : A)) :
          Set (ProjectiveSpectrum 𝒜))))
Tactic: rw [← Equiv.image_symm_eq_preimage, h₁, Set.image_iUnion]
-- 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 : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)
hx : Membership.mem (γ := Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) (pbo f) x
⊢ Eq (α := CommRingCat.of (A⁰_ f) ⟶ Presheaf.stalk (Sheaf.presheaf (structureSheaf 𝒜)) x)
    (awayToSection 𝒜 f ≫ Presheaf.germ (Sheaf.presheaf (structureSheaf 𝒜)) (pbo f) x hx :
      CommRingCat.of (A⁰_ f) ⟶ Presheaf.stalk (Sheaf.presheaf (structureSheaf 𝒜)) x)
    (CategoryStruct.comp (Y := CommRingCat.of (HomogeneousLocalization 𝒜 x.asHomogeneousIdeal.toIdeal.primeCompl))
        (CommRingCat.ofHom (HomogeneousLocalization.mapId 𝒜 ⋯))
        (Iso.inv (RingEquiv.toCommRingCatIso («Proj».stalkIso' 𝒜 x))) :
      CommRingCat.of (HomogeneousLocalization 𝒜 (Submonoid.powers f)) ⟶
        CommRingCat.of (↑(Presheaf.stalk (Sheaf.presheaf (structureSheaf 𝒜)) x) : Type u_1))
have hf : ∀ (z : (↑(CommRingCat.of (A⁰_ f)) : Type u_1)),
  Eq (α := (↑(Presheaf.stalk (Sheaf.presheaf (structureSheaf 𝒜)) x) : Type u_1))
    (((CommRingCat.Hom.hom (awayToSection 𝒜 f ≫ Presheaf.germ (Sheaf.presheaf (structureSheaf 𝒜)) (pbo f) x hx) :
            (↑(CommRingCat.of (A⁰_ f)) : Type u_1) →+*
              (↑(Presheaf.stalk (Sheaf.presheaf (structureSheaf 𝒜)) x) : Type u_1)) :
          (a : (↑(CommRingCat.of (A⁰_ f)) : Type u_1)) → (↑((structureSheaf 𝒜).presheaf.stalk x) : Type u_1))
        z :
      (↑(Presheaf.stalk (Sheaf.presheaf (structureSheaf 𝒜)) x) : Type u_1))
    ((CommRingCat.Hom.hom
            (CategoryStruct.comp (Y :=
              CommRingCat.of (HomogeneousLocalization 𝒜 x.asHomogeneousIdeal.toIdeal.primeCompl))
              (CommRingCat.ofHom (HomogeneousLocalization.mapId 𝒜 sorry))
              (Iso.inv (RingEquiv.toCommRingCatIso («Proj».stalkIso' 𝒜 x)))) :
          (a : (↑(CommRingCat.of (A⁰_ f)) : Type u_1)) → (↑((structureSheaf 𝒜).presheaf.stalk x) : Type u_1))
        z :
      (↑(Presheaf.stalk (Sheaf.presheaf (structureSheaf 𝒜)) x) : Type u_1))
Tactic: ext 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 𝒜
f : A
x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)
hx : Membership.mem (γ := Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) (pbo f) x
z : (↑(CommRingCat.of (A⁰_ f)) : Type u_1)
⊢ Eq (α := (↑(Presheaf.stalk (Sheaf.presheaf (structureSheaf 𝒜)) x) : Type u_1))
    (((CommRingCat.Hom.hom (awayToSection 𝒜 f ≫ Presheaf.germ (Sheaf.presheaf (structureSheaf 𝒜)) (pbo f) x hx) :
            (↑(CommRingCat.of (A⁰_ f)) : Type u_1) →+*
              (↑(Presheaf.stalk (Sheaf.presheaf (structureSheaf 𝒜)) x) : Type u_1)) :
          (a : (↑(CommRingCat.of (A⁰_ f)) : Type u_1)) → (↑((structureSheaf 𝒜).presheaf.stalk x) : Type u_1))
        z :
      (↑(Presheaf.stalk (Sheaf.presheaf (structureSheaf 𝒜)) x) : Type u_1))
    ((CommRingCat.Hom.hom
            (CategoryStruct.comp (Y :=
              CommRingCat.of (HomogeneousLocalization 𝒜 x.asHomogeneousIdeal.toIdeal.primeCompl))
              (CommRingCat.ofHom (HomogeneousLocalization.mapId 𝒜 ⋯))
              (Iso.inv (RingEquiv.toCommRingCatIso («Proj».stalkIso' 𝒜 x)))) :
          (a : (↑(CommRingCat.of (A⁰_ f)) : Type u_1)) → (↑((structureSheaf 𝒜).presheaf.stalk x) : Type u_1))
        z :
      (↑(Presheaf.stalk (Sheaf.presheaf (structureSheaf 𝒜)) x) : Type u_1))
have hf : Eq (α := HomogeneousLocalization.AtPrime 𝒜 x.asHomogeneousIdeal.toIdeal)
  ((«Proj».stalkIso' 𝒜 x :
        (a : (↑((structureSheaf 𝒜).presheaf.stalk x) : Type u_1)) →
          HomogeneousLocalization.AtPrime 𝒜 x.asHomogeneousIdeal.toIdeal)
      (((CommRingCat.Hom.hom (awayToSection 𝒜 f ≫ Presheaf.germ (Sheaf.presheaf (structureSheaf 𝒜)) (pbo f) x hx) :
            (↑(CommRingCat.of (A⁰_ f)) : Type u_1) →+*
              (↑(Presheaf.stalk (Sheaf.presheaf (structureSheaf 𝒜)) x) : Type u_1)) :
          (a : (↑(CommRingCat.of (A⁰_ f)) : Type u_1)) → (↑((structureSheaf 𝒜).presheaf.stalk x) : Type u_1))
        z) :
    HomogeneousLocalization.AtPrime 𝒜 x.asHomogeneousIdeal.toIdeal)
  ((CommRingCat.Hom.hom' (CommRingCat.ofHom (HomogeneousLocalization.mapId 𝒜 sorry)) :
        (a : (↑(CommRingCat.of (HomogeneousLocalization 𝒜 (Submonoid.powers f))) : Type u_1)) →
          (↑(CommRingCat.of (HomogeneousLocalization 𝒜 x.asHomogeneousIdeal.toIdeal.primeCompl)) : Type u_1))
      z :
    (↑(CommRingCat.of (HomogeneousLocalization 𝒜 x.asHomogeneousIdeal.toIdeal.primeCompl)) : Type u_1))
Tactic: apply (Proj.stalkIso' 𝒜 x).eq_symm_apply.mpr
-- 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 : (↑(CommRingCat.of (A⁰_ f)) : Type u_1)
p : ↥(unop (op (pbo f)))
⊢ Eq (α := Localization (M := A) (↑p : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)).asHomogeneousIdeal.toIdeal.primeCompl)
    (HomogeneousLocalization.val.{0, u_1, u_2} (ι := ℕ) (σ := σ) (𝒜 := 𝒜)
      ((↑((CommRingCat.Hom.hom' (awayToSection 𝒜 f) :
                (a : (↑(CommRingCat.of (A⁰_ f)) : Type u_1)) → (↑((structureSheaf 𝒜).obj.obj (op (pbo f))) : Type u_1))
              x) :
          (x : ↥(unop (op (pbo f)))) →
            (fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦
                HomogeneousLocalization.AtPrime 𝒜 x.asHomogeneousIdeal.toIdeal)
              (↑x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)))
        p))
    ((IsLocalization.map (M := Submonoid.powers f) (T :=
          (↑p : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)).asHomogeneousIdeal.toIdeal.primeCompl)
          (Localization (M := A) (↑p : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)).asHomogeneousIdeal.toIdeal.primeCompl)
          (RingHom.id A) ⋯ :
        (a : Localization (Submonoid.powers f)) →
          Localization (↑p : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)).asHomogeneousIdeal.toIdeal.primeCompl)
      (HomogeneousLocalization.val x))
have obtain : ∀ (x : HomogeneousLocalization.NumDenSameDeg 𝒜 (Submonoid.powers f)),
  Eq (α := Localization (M := A) (↑p : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)).asHomogeneousIdeal.toIdeal.primeCompl)
    (HomogeneousLocalization.val.{0, u_1, u_2} (ι := ℕ) (σ := σ) (𝒜 := 𝒜)
      ((↑((CommRingCat.Hom.hom' (awayToSection 𝒜 f) :
                (a : (↑(CommRingCat.of (A⁰_ f)) : Type u_1)) → (↑((structureSheaf 𝒜).obj.obj (op (pbo f))) : Type u_1))
              (HomogeneousLocalization.mk x)) :
          (x : ↥(unop (op (pbo f)))) →
            (fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦
                HomogeneousLocalization.AtPrime 𝒜 x.asHomogeneousIdeal.toIdeal)
              (↑x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)))
        p))
    ((IsLocalization.map (M := Submonoid.powers f) (T :=
          (↑p : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)).asHomogeneousIdeal.toIdeal.primeCompl)
          (Localization (M := A) (↑p : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)).asHomogeneousIdeal.toIdeal.primeCompl)
          (RingHom.id A) sorry :
        (a : Localization (Submonoid.powers f)) →
          Localization (↑p : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)).asHomogeneousIdeal.toIdeal.primeCompl)
      (HomogeneousLocalization.mk x).val)
Tactic: obtain ⟨x, rfl⟩ := HomogeneousLocalization.mk_surjective x
Cleared hypotheses: x
-- 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
p : ↥(unop (op (pbo f)))
x : HomogeneousLocalization.NumDenSameDeg 𝒜 (Submonoid.powers f)
⊢ Eq (α := Localization (M := A) (↑p : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)).asHomogeneousIdeal.toIdeal.primeCompl)
    (HomogeneousLocalization.val.{0, u_1, u_2} (ι := ℕ) (σ := σ) (𝒜 := 𝒜)
      ((↑((CommRingCat.Hom.hom' (awayToSection 𝒜 f) :
                (a : (↑(CommRingCat.of (A⁰_ f)) : Type u_1)) → (↑((structureSheaf 𝒜).obj.obj (op (pbo f))) : Type u_1))
              (HomogeneousLocalization.mk x)) :
          (x : ↥(unop (op (pbo f)))) →
            (fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦
                HomogeneousLocalization.AtPrime 𝒜 x.asHomogeneousIdeal.toIdeal)
              (↑x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)))
        p))
    ((IsLocalization.map (M := Submonoid.powers f) (T :=
          (↑p : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)).asHomogeneousIdeal.toIdeal.primeCompl)
          (Localization (M := A) (↑p : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)).asHomogeneousIdeal.toIdeal.primeCompl)
          (RingHom.id A) ⋯ :
        (a : Localization (Submonoid.powers f)) →
          Localization (↑p : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)).asHomogeneousIdeal.toIdeal.primeCompl)
      (HomogeneousLocalization.mk x).val)
have change : Eq (α := Localization (M := A) (↑p : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)).asHomogeneousIdeal.toIdeal.primeCompl)
  (HomogeneousLocalization.val.{0, u_1, u_2} (ι := ℕ) (σ := σ) (𝒜 := 𝒜)
    (((HomogeneousLocalization.mapId 𝒜 sorry :
          HomogeneousLocalization 𝒜 (Submonoid.powers f) →+*
            HomogeneousLocalization 𝒜
              (↑p : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)).asHomogeneousIdeal.toIdeal.primeCompl) :
        (a : HomogeneousLocalization 𝒜 (Submonoid.powers f)) →
          HomogeneousLocalization 𝒜
            (↑p : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)).asHomogeneousIdeal.toIdeal.primeCompl)
      (HomogeneousLocalization.mk x)))
  ((IsLocalization.map (M := Submonoid.powers f) (T :=
        (↑p : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)).asHomogeneousIdeal.toIdeal.primeCompl)
        (Localization (M := A) (↑p : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)).asHomogeneousIdeal.toIdeal.primeCompl)
        (RingHom.id A) sorry :
      (a : Localization (Submonoid.powers f)) →
        Localization (↑p : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)).asHomogeneousIdeal.toIdeal.primeCompl)
    (HomogeneousLocalization.mk x).val)
Tactic: change (HomogeneousLocalization.mapId 𝒜 _ _).val = _
-- 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
p : ↥(unop (op (pbo f)))
x : HomogeneousLocalization.NumDenSameDeg 𝒜 (Submonoid.powers f)
⊢ Eq (α := Localization (M := A) (↑p : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)).asHomogeneousIdeal.toIdeal.primeCompl)
    (HomogeneousLocalization.val.{0, u_1, u_2} (ι := ℕ) (σ := σ) (𝒜 := 𝒜)
      (((HomogeneousLocalization.mapId 𝒜 ⋯ :
            HomogeneousLocalization 𝒜 (Submonoid.powers f) →+*
              HomogeneousLocalization 𝒜
                (↑p : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)).asHomogeneousIdeal.toIdeal.primeCompl) :
          (a : HomogeneousLocalization 𝒜 (Submonoid.powers f)) →
            HomogeneousLocalization 𝒜
              (↑p : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)).asHomogeneousIdeal.toIdeal.primeCompl)
        (HomogeneousLocalization.mk x)))
    ((IsLocalization.map (M := Submonoid.powers f) (T :=
          (↑p : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)).asHomogeneousIdeal.toIdeal.primeCompl)
          (Localization (M := A) (↑p : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)).asHomogeneousIdeal.toIdeal.primeCompl)
          (RingHom.id A) ⋯ :
        (a : Localization (Submonoid.powers f)) →
          Localization (↑p : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)).asHomogeneousIdeal.toIdeal.primeCompl)
      (HomogeneousLocalization.mk x).val)
have dsimp : Eq (α := Localization (M := A) (↑p : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)).asHomogeneousIdeal.toIdeal.primeCompl)
  (Localization.mk (↑x.num : A)
    (Subtype.mk (p := fun (x : A) ↦
      x ∈ (↑p : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)).asHomogeneousIdeal.toIdeal.primeCompl) (↑x.den : A) sorry))
  ((IsLocalization.map (M := Submonoid.powers f) (T :=
        (↑p : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)).asHomogeneousIdeal.toIdeal.primeCompl)
        (Localization (M := A) (↑p : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)).asHomogeneousIdeal.toIdeal.primeCompl)
        (RingHom.id A) sorry :
      (a : Localization (Submonoid.powers f)) →
        Localization (↑p : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)).asHomogeneousIdeal.toIdeal.primeCompl)
    (Localization.mk (↑x.num : A)
      (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers f) x) (↑x.den : A) sorry)))
Tactic: dsimp [HomogeneousLocalization.mapId, HomogeneousLocalization.map]
-- 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
p : ↥(unop (op (pbo f)))
x : HomogeneousLocalization.NumDenSameDeg 𝒜 (Submonoid.powers f)
⊢ Eq (α := Localization (M := A) (↑p : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)).asHomogeneousIdeal.toIdeal.primeCompl)
    (Localization.mk (↑x.num : A)
      (Subtype.mk (p := fun (x : A) ↦
        x ∈ (↑p : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)).asHomogeneousIdeal.toIdeal.primeCompl) (↑x.den : A) ⋯))
    ((IsLocalization.map (M := Submonoid.powers f) (T :=
          (↑p : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)).asHomogeneousIdeal.toIdeal.primeCompl)
          (Localization (M := A) (↑p : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)).asHomogeneousIdeal.toIdeal.primeCompl)
          (RingHom.id A) ⋯ :
        (a : Localization (Submonoid.powers f)) →
          Localization (↑p : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)).asHomogeneousIdeal.toIdeal.primeCompl)
      (Localization.mk (↑x.num : A)
        (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers f) x) (↑x.den : A) ⋯)))
have rw : Eq (α := Localization (M := A) (↑p : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)).asHomogeneousIdeal.toIdeal.primeCompl)
  (IsLocalization.mk' (M := (↑p : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)).asHomogeneousIdeal.toIdeal.primeCompl)
    (Localization (M := A) (↑p : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)).asHomogeneousIdeal.toIdeal.primeCompl)
    (↑x.num : A)
    (Subtype.mk (p := fun (x : A) ↦
      x ∈ (↑p : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)).asHomogeneousIdeal.toIdeal.primeCompl) (↑x.den : A) sorry))
  (IsLocalization.mk' (R := A) (M :=
    (↑p : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)).asHomogeneousIdeal.toIdeal.primeCompl)
    (Localization (M := A) (↑p : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)).asHomogeneousIdeal.toIdeal.primeCompl)
    ((RingHom.id A : (a : A) → A) (↑x.num : A) : A)
    (Subtype.mk (p := fun (x : A) ↦
        x ∈ (↑p : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)).asHomogeneousIdeal.toIdeal.primeCompl)
        ((RingHom.id A : (a : A) → A)
          (↑(Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers f) x) (↑x.den : A) sorry) :
            A))
        sorry :
      ↥(↑p : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)).asHomogeneousIdeal.toIdeal.primeCompl))
Tactic: rw [Localization.mk_eq_mk', Localization.mk_eq_mk', IsLocalization.map_mk']
-- 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 :
  (↑(Proj.restrict (U := Functor.obj (C := Opens (↑Proj.T : Type u_1)) (Opens.toTopCat Proj.T) (pbo f)) ⋯).toTopCat :
    Type u_1)
⊢ Eq (α := (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1))
    ((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 :
      (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1))
    (PrimeSpectrum.comap (S :=
        HomogeneousLocalization 𝒜 (↑x : (↑Proj.T : Type u_1)).asHomogeneousIdeal.toIdeal.primeCompl) (mapId 𝒜 ⋯)
        (closedPoint (AtPrime 𝒜 (↑x : (↑Proj.T : Type u_1)).asHomogeneousIdeal.toIdeal)) :
      PrimeSpectrum (HomogeneousLocalization 𝒜 (Submonoid.powers f)))
have change : PrimeSpectrum.comap (S :=
    (↑((Proj.restrict (U := Functor.obj (C := Opens (↑Proj.T : Type u_1)) (Opens.toTopCat Proj.T) (pbo f))
                sorry).presheaf.stalk
          x) :
      Type u_1))
    (CommRingCat.Hom.hom
      (awayToΓ 𝒜 f ≫
        (Proj.restrict (U := Functor.obj (C := Opens (↑Proj.T : Type u_1)) (Opens.toTopCat Proj.T) (pbo f))
                sorry).presheaf.Γgerm
          x))
    (closedPoint
      (↑((Proj.restrict (U := Functor.obj (C := Opens (↑Proj.T : Type u_1)) (Opens.toTopCat Proj.T) (pbo f))
                  sorry).presheaf.stalk
            x) :
        Type u_1)) =
  PrimeSpectrum.comap (S := HomogeneousLocalization 𝒜 (↑x : (↑Proj.T : Type u_1)).asHomogeneousIdeal.toIdeal.primeCompl)
    (mapId 𝒜 sorry) (closedPoint (AtPrime 𝒜 (↑x : (↑Proj.T : Type u_1)).asHomogeneousIdeal.toIdeal))
Tactic: change PrimeSpectrum.comap (awayToΓ 𝒜 f ≫ (Proj| pbo f).presheaf.Γgerm x).hom
        (IsLocalRing.closedPoint ((Proj| pbo f).presheaf.stalk x)) = _
-- 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 :
  (↑(Proj.restrict (U := Functor.obj (C := Opens (↑Proj.T : Type u_1)) (Opens.toTopCat Proj.T) (pbo f)) ⋯).toTopCat :
    Type u_1)
⊢ PrimeSpectrum.comap (S :=
      (↑((Proj.restrict (U := Functor.obj (C := Opens (↑Proj.T : Type u_1)) (Opens.toTopCat Proj.T) (pbo f))
                  ⋯).presheaf.stalk
            x) :
        Type u_1))
      (CommRingCat.Hom.hom
        (awayToΓ 𝒜 f ≫
          (Proj.restrict (U := Functor.obj (C := Opens (↑Proj.T : Type u_1)) (Opens.toTopCat Proj.T) (pbo f))
                  ⋯).presheaf.Γgerm
            x))
      (closedPoint
        (↑((Proj.restrict (U := Functor.obj (C := Opens (↑Proj.T : Type u_1)) (Opens.toTopCat Proj.T) (pbo f))
                    ⋯).presheaf.stalk
              x) :
          Type u_1)) =
    PrimeSpectrum.comap (S :=
      HomogeneousLocalization 𝒜 (↑x : (↑Proj.T : Type u_1)).asHomogeneousIdeal.toIdeal.primeCompl) (mapId 𝒜 ⋯)
      (closedPoint (AtPrime 𝒜 (↑x : (↑Proj.T : Type u_1)).asHomogeneousIdeal.toIdeal))
have rw : Eq (α := PrimeSpectrum (↑(CommRingCat.of (A⁰_ f)) : Type u_1))
  (Function.comp (β :=
    PrimeSpectrum
      (↑(CommRingCat.of (HomogeneousLocalization 𝒜 (↑x : (↑Proj.T : Type u_1)).asHomogeneousIdeal.toIdeal.primeCompl)) :
        Type u_1))
    (PrimeSpectrum.comap (CommRingCat.Hom.hom (CommRingCat.ofHom (mapId 𝒜 sorry))))
    (PrimeSpectrum.comap
      (CommRingCat.Hom.hom
        (Iso.inv (RingEquiv.toCommRingCatIso («Proj».stalkIso' 𝒜 (↑x : (↑Proj.T : Type u_1)))) ≫
          Iso.inv (Proj.restrictStalkIso sorry x))))
    (closedPoint
      (↑((Proj.restrict (U := Functor.obj (C := Opens (↑Proj.T : Type u_1)) (Opens.toTopCat Proj.T) (pbo f))
                  sorry).presheaf.stalk
            x) :
        Type u_1)))
  (PrimeSpectrum.comap (S :=
    HomogeneousLocalization 𝒜 (↑x : (↑Proj.T : Type u_1)).asHomogeneousIdeal.toIdeal.primeCompl) (mapId 𝒜 sorry)
    (closedPoint (AtPrime 𝒜 (↑x : (↑Proj.T : Type u_1)).asHomogeneousIdeal.toIdeal)))
Tactic: rw [awayToΓ_ΓToStalk, CommRingCat.hom_comp, PrimeSpectrum.comap_comp]
-- 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 :
  (↑(Proj.restrict (U := Functor.obj (C := Opens (↑Proj.T : Type u_1)) (Opens.toTopCat Proj.T) (pbo f)) ⋯).toTopCat :
    Type u_1)
z : HomogeneousLocalization 𝒜 (Submonoid.powers f)
⊢ ¬IsUnit (M := AtPrime 𝒜 (↑x : (↑Proj.T : Type u_1)).asHomogeneousIdeal.toIdeal)
        ((mapId 𝒜 ⋯ :
              (a : HomogeneousLocalization 𝒜 (Submonoid.powers f)) →
                HomogeneousLocalization 𝒜 (↑x : (↑Proj.T : Type u_1)).asHomogeneousIdeal.toIdeal.primeCompl)
            z :
          HomogeneousLocalization 𝒜 (↑x : (↑Proj.T : Type u_1)).asHomogeneousIdeal.toIdeal.primeCompl) ↔
    z ∈ ProjIsoSpecTopComponent.ToSpec.carrier x
have obtain : ∀ (z : NumDenSameDeg 𝒜 (Submonoid.powers f)),
  ¬IsUnit (M := AtPrime 𝒜 (↑x : (↑Proj.T : Type u_1)).asHomogeneousIdeal.toIdeal)
        ((mapId 𝒜 sorry :
              (a : HomogeneousLocalization 𝒜 (Submonoid.powers f)) →
                HomogeneousLocalization 𝒜 (↑x : (↑Proj.T : Type u_1)).asHomogeneousIdeal.toIdeal.primeCompl)
            (HomogeneousLocalization.mk z) :
          HomogeneousLocalization 𝒜 (↑x : (↑Proj.T : Type u_1)).asHomogeneousIdeal.toIdeal.primeCompl) ↔
    HomogeneousLocalization.mk z ∈ ProjIsoSpecTopComponent.ToSpec.carrier x
Tactic: obtain ⟨z, rfl⟩ := z.mk_surjective
Cleared hypotheses: z