awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
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)
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 𝒜 ⋯))))
      (PrimeSpectrum.comap
        (CommRingCat.Hom.hom
          (Iso.inv (RingEquiv.toCommRingCatIso («Proj».stalkIso' 𝒜 (↑x : (↑Proj.T : Type u_1)))) ≫
            Iso.inv (Proj.restrictStalkIso ⋯ 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)))
⊢ 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))

Tactic:
rw [awayToΓ_ΓToStalk, CommRingCat.hom_comp, PrimeSpectrum.comap_comp]

Premises used: AlgebraicGeometry.ProjectiveSpectrum.Proj.awayToΓ_ΓToStalk, CommRingCat.hom_comp, PrimeSpectrum.comap_comp
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
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 (α := 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 𝒜 ⋯))))
      (PrimeSpectrum.comap
        (CommRingCat.Hom.hom
          (Iso.inv (RingEquiv.toCommRingCatIso («Proj».stalkIso' 𝒜 (↑x : (↑Proj.T : Type u_1)))) ≫
            Iso.inv (Proj.restrictStalkIso ⋯ 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)))

Tactic:
congr(PrimeSpectrum.comap _ $(@IsLocalRing.comap_closedPoint
    (HomogeneousLocalization.AtPrime 𝒜 x.1.asHomogeneousIdeal.toIdeal) _ _
    ((Proj| pbo f).presheaf.stalk x) _ _ _ (isLocalHom_of_isIso _)))

Premises used: Iff.mpr, CommRingCat.Hom.hom, congrArg, ProjectiveSpectrum.basicOpen, IsLocalRing.comap_closedPoint, RingEquiv.toCommRingCatIso, AlgebraicGeometry.Proj.toLocallyRingedSpace, CommRingCat.ofHom, id, AlgebraicGeometry.Proj.stalkIso', TopologicalSpace.Opens.isOpenEmbedding, AlgebraicGeometry.LocallyRingedSpace.restrictStalkIso, CategoryTheory.CategoryStruct.comp, HomogeneousLocalization.mapId, PrimeSpectrum.comap, Subtype.val, CategoryTheory.Iso.inv, Submonoid.powers_le, Subtype.property
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
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 (α := 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 𝒜 ⋯))))
      (PrimeSpectrum.comap
        (CommRingCat.Hom.hom
          (Iso.inv (RingEquiv.toCommRingCatIso («Proj».stalkIso' 𝒜 (↑x : (↑Proj.T : Type u_1)))) ≫
            Iso.inv (Proj.restrictStalkIso ⋯ 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)))

Tactic:
exact congr(PrimeSpectrum.comap _ $(@IsLocalRing.comap_closedPoint
    (HomogeneousLocalization.AtPrime 𝒜 x.1.asHomogeneousIdeal.toIdeal) _ _
    ((Proj| pbo f).presheaf.stalk x) _ _ _ (isLocalHom_of_isIso _)))
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
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)
obtain :
  ∀ (z : NumDenSameDeg 𝒜 (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)
              (HomogeneousLocalization.mk z) :
            HomogeneousLocalization 𝒜 (↑x : (↑Proj.T : Type u_1)).asHomogeneousIdeal.toIdeal.primeCompl) ↔
      HomogeneousLocalization.mk z ∈ ProjIsoSpecTopComponent.ToSpec.carrier x
⊢ ¬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

Tactic:
obtain ⟨z, rfl⟩ := z.mk_surjective

Premises used: HomogeneousLocalization.mk_surjective, rfl
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
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 : NumDenSameDeg 𝒜 (Submonoid.powers f)
rw :
  (↑(NumDenSameDeg.num
            { deg := z.deg,
              num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 z.deg) ((GradedRingHom.id 𝒜 : (a : A) → A) (↑z.num : A)) ⋯,
              den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 z.deg) ((GradedRingHom.id 𝒜 : (a : A) → A) (↑z.den : A)) ⋯,
              den_mem := ⋯ : NumDenSameDeg 𝒜 (↑x : (↑Proj.T : Type u_1)).asHomogeneousIdeal.toIdeal.primeCompl }) :
        A) ∉
      (↑x : (↑Proj.T : Type u_1)).asHomogeneousIdeal.toIdeal.primeCompl ↔
    (↑z.num : A) ∈ (↑x : (↑Proj.T : Type u_1)).asHomogeneousIdeal
⊢ ¬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)
            (HomogeneousLocalization.mk z) :
          HomogeneousLocalization 𝒜 (↑x : (↑Proj.T : Type u_1)).asHomogeneousIdeal.toIdeal.primeCompl) ↔
    HomogeneousLocalization.mk z ∈ ProjIsoSpecTopComponent.ToSpec.carrier x

Tactic:
rw [← HomogeneousLocalization.isUnit_iff_isUnit_val,
    ProjIsoSpecTopComponent.ToSpec.mk_mem_carrier, HomogeneousLocalization.map_mk,
    HomogeneousLocalization.val_mk, Localization.mk_eq_mk',
    IsLocalization.AtPrime.isUnit_mk'_iff]

Premises used: HomogeneousLocalization.map_mk, Localization.mk_eq_mk', HomogeneousLocalization.val_mk, AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.mk_mem_carrier, HomogeneousLocalization.isUnit_iff_isUnit_val, IsLocalization.AtPrime.isUnit_mk'_iff
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
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 : NumDenSameDeg 𝒜 (Submonoid.powers f)
⊢ (↑(NumDenSameDeg.num
            { deg := z.deg,
              num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 z.deg) ((GradedRingHom.id 𝒜 : (a : A) → A) (↑z.num : A)) ⋯,
              den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 z.deg) ((GradedRingHom.id 𝒜 : (a : A) → A) (↑z.den : A)) ⋯,
              den_mem := ⋯ : NumDenSameDeg 𝒜 (↑x : (↑Proj.T : Type u_1)).asHomogeneousIdeal.toIdeal.primeCompl }) :
        A) ∉
      (↑x : (↑Proj.T : Type u_1)).asHomogeneousIdeal.toIdeal.primeCompl ↔
    (↑z.num : A) ∈ (↑x : (↑Proj.T : Type u_1)).asHomogeneousIdeal

Tactic:
not_not

Premises used: Classical.not_not, Set.Mem, setOf, Not
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
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 : NumDenSameDeg 𝒜 (Submonoid.powers f)
⊢ (↑(NumDenSameDeg.num
            { deg := z.deg,
              num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 z.deg) ((GradedRingHom.id 𝒜 : (a : A) → A) (↑z.num : A)) ⋯,
              den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 z.deg) ((GradedRingHom.id 𝒜 : (a : A) → A) (↑z.den : A)) ⋯,
              den_mem := ⋯ : NumDenSameDeg 𝒜 (↑x : (↑Proj.T : Type u_1)).asHomogeneousIdeal.toIdeal.primeCompl }) :
        A) ∉
      (↑x : (↑Proj.T : Type u_1)).asHomogeneousIdeal.toIdeal.primeCompl ↔
    (↑z.num : A) ∈ (↑x : (↑Proj.T : Type u_1)).asHomogeneousIdeal

Tactic:
exact not_not

Premises used: Classical.not_not
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
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))
            ⋯).toPresheafedSpace :
      TopCat))
    (Iso.hom (projIsoSpecTopComponent f_deg hm))

Tactic:
(projIsoSpecTopComponent f_deg hm).isIso_hom

Premises used: AlgebraicGeometry.projIsoSpecTopComponent, CategoryTheory.Iso.isIso_hom
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
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
h :
  Eq (α :=
    (↑(Proj.restrict (U := Functor.obj (C := Opens (↑Proj.T : Type u_1)) (Opens.toTopCat Proj.T) (pbo f))
              ⋯).toPresheafedSpace :
        TopCat) ⟶
      (↑(Spec A⁰_ f).toPresheafedSpace : TopCat))
    (PresheafedSpace.Hom.base (LocallyRingedSpace.Hom.toHom (toSpec 𝒜 f))) (Iso.hom (projIsoSpecTopComponent f_deg hm))
⊢ 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)))

Tactic:
convert! (projIsoSpecTopComponent f_deg hm).isIso_hom

Premises used: AlgebraicGeometry.projIsoSpecTopComponent, CategoryTheory.Iso.isIso_hom
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
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
⊢ Eq (α :=
    (↑(Proj.restrict (U := Functor.obj (C := Opens (↑Proj.T : Type u_1)) (Opens.toTopCat Proj.T) (pbo f))
              ⋯).toPresheafedSpace :
        TopCat) ⟶
      (↑(Spec A⁰_ f).toPresheafedSpace : TopCat))
    (PresheafedSpace.Hom.base (LocallyRingedSpace.Hom.toHom (toSpec 𝒜 f))) (Iso.hom (projIsoSpecTopComponent f_deg hm))

Tactic:
ConcreteCategory.hom_ext _ _ <| toSpec_base_apply_eq 𝒜

Premises used: AlgebraicGeometry.ProjectiveSpectrum.Proj.toSpec_base_apply_eq, CategoryTheory.ConcreteCategory.hom_ext
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
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
⊢ Eq (α :=
    (↑(Proj.restrict (U := Functor.obj (C := Opens (↑Proj.T : Type u_1)) (Opens.toTopCat Proj.T) (pbo f))
              ⋯).toPresheafedSpace :
        TopCat) ⟶
      (↑(Spec A⁰_ f).toPresheafedSpace : TopCat))
    (PresheafedSpace.Hom.base (LocallyRingedSpace.Hom.toHom (toSpec 𝒜 f))) (Iso.hom (projIsoSpecTopComponent f_deg hm))

Tactic:
exact ConcreteCategory.hom_ext _ _ <| toSpec_base_apply_eq 𝒜

Premises used: AlgebraicGeometry.ProjectiveSpectrum.Proj.toSpec_base_apply_eq, CategoryTheory.ConcreteCategory.hom_ext
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
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 : NumDenSameDeg 𝒜 (Submonoid.powers f)
⊢ Membership.mem (γ := Ideal (↑(CommRingCat.of (A⁰_ f)) : Type u_1))
      (PrimeSpectrum.asIdeal
        ((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))
      (HomogeneousLocalization.mk z) ↔
    (↑z.num : A) ∈ (↑x : (↑Proj.T : Type u_1)).asHomogeneousIdeal

Tactic:
(toSpec_base_apply_eq 𝒜 x).symm ▸ ProjIsoSpecTopComponent.ToSpec.mk_mem_carrier _ _

Premises used: Eq.rec, AlgebraicGeometry.ProjectiveSpectrum.Proj.toSpec_base_apply_eq, AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.mk_mem_carrier, Eq.symm
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
f : A
t : NumDenSameDeg 𝒜 (Submonoid.powers f)
⊢ ProjIsoSpecTopComponent.ToSpec.toFun f ⁻¹' (↑(sbo HomogeneousLocalization.mk t) : Set (PrimeSpectrum (A⁰_ f))) =
    Subtype.val (p := fun (x : (↑Proj.T : Type u_1)) ↦ Membership.mem (γ := Opens (↑Proj.T : Type u_1)) (pbo f) x) ⁻¹'
      (↑(pbo (↑t.num : A)) : Set (ProjectiveSpectrum 𝒜))

Tactic:
(ProjIsoSpecTopComponent.ToSpec.preimage_basicOpen f t)

Premises used: AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.preimage_basicOpen
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
f : A
t : NumDenSameDeg 𝒜 (Submonoid.powers f)
h :
  Eq (α :=
    (↑(↑(Proj.restrict (U := Functor.obj (C := Opens (↑Proj.T : Type u_1)) (Opens.toTopCat Proj.T) (pbo f))
                  ⋯).toPresheafedSpace :
            TopCat) :
        Type u_1) →
      (↑(↑(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))
    (ProjIsoSpecTopComponent.ToSpec.toFun f)
⊢ (⇑(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)) ⁻¹'
      (↑(sbo HomogeneousLocalization.mk t) : Set (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1)) =
    (↑((Opens.comap
                {
                  toFun :=
                    Subtype.val (p := fun (x : (↑Proj.T : Type u_1)) ↦
                      Membership.mem (γ := Opens (↑Proj.T : Type u_1)) (pbo f) x),
                  continuous_toFun := ⋯ : C(↥(pbo f), ProjectiveSpectrum 𝒜) } :
              (a : Opens (ProjectiveSpectrum 𝒜)) → Opens ↥(pbo f))
            (pbo (↑t.num : A)) :
          Opens ↥(pbo f)) :
      Set (↑(↑(Proj.restrict ⋯).toPresheafedSpace : TopCat) : Type u_1))

Tactic:
convert! (ProjIsoSpecTopComponent.ToSpec.preimage_basicOpen f t)

Premises used: AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.preimage_basicOpen
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
f : A
t : NumDenSameDeg 𝒜 (Submonoid.powers f)
⊢ Eq (α :=
    (↑(↑(Proj.restrict (U := Functor.obj (C := Opens (↑Proj.T : Type u_1)) (Opens.toTopCat Proj.T) (pbo f))
                  ⋯).toPresheafedSpace :
            TopCat) :
        Type u_1) →
      (↑(↑(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))
    (ProjIsoSpecTopComponent.ToSpec.toFun f)

Tactic:
funext fun _ => toSpec_base_apply_eq _ _

Premises used: AlgebraicGeometry.ProjectiveSpectrum.Proj.toSpec_base_apply_eq, funext
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
f : A
t : NumDenSameDeg 𝒜 (Submonoid.powers f)
⊢ Eq (α :=
    (↑(↑(Proj.restrict (U := Functor.obj (C := Opens (↑Proj.T : Type u_1)) (Opens.toTopCat Proj.T) (pbo f))
                  ⋯).toPresheafedSpace :
            TopCat) :
        Type u_1) →
      (↑(↑(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))
    (ProjIsoSpecTopComponent.ToSpec.toFun f)

Tactic:
exact funext fun _ => toSpec_base_apply_eq _ _

Premises used: AlgebraicGeometry.ProjectiveSpectrum.Proj.toSpec_base_apply_eq, funext
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
f : A
U : (Opens (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1))ᵒᵖ
⊢ Eq (α :=
    CommRingCat.of (A⁰_ f) ⟶
      (Functor.obj
            (Presheaf.pushforward CommRingCat (PresheafedSpace.Hom.base (LocallyRingedSpace.Hom.toHom (toSpec 𝒜 f))))
            (Proj.restrict (U := Functor.obj (C := Opens (↑Proj.T : Type u_1)) (Opens.toTopCat Proj.T) (pbo f))
                ⋯).presheaf).obj
        U)
    (Iso.inv (Scheme.ΓSpecIso (CommRingCat.of (A⁰_ f))) ≫
      (Spec A⁰_ f).presheaf.map (Quiver.Hom.op (homOfLE ⋯)) ≫
        NatTrans.app (PresheafedSpace.Hom.c (LocallyRingedSpace.Hom.toHom (toSpec 𝒜 f))) U)
    (CommRingCat.ofHom
        (algebraMap (A⁰_ f)
          (Functor.obj
            (ObjectProperty.FullSubcategory.obj (P :=
              CategoryTheory.Presheaf.IsSheaf
                (Opens.grothendieckTopology
                  (↑(PrimeSpectrum.Top (↑(unop (op (CommRingCat.of (A⁰_ f)))) : Type u_1)) : Type u_1)))
              (structureSheafInType (↑(unop (op (CommRingCat.of (A⁰_ f)))) : Type u_1)
                (↑(unop (op (CommRingCat.of (A⁰_ f)))) : Type u_1)))
            U)) ≫
      NatTrans.app
        (PresheafedSpace.Hom.c
          (LocallyRingedSpace.Hom.toHom
            ((ΓSpec.locallyRingedSpaceAdjunction.homEquiv
                  (Proj.restrict (U := Functor.obj (C := Opens (↑Proj.T : Type u_1)) (Opens.toTopCat Proj.T) (pbo f)) ⋯)
                  (op (CommRingCat.of (A⁰_ f))) :
                (a : LocallyRingedSpace.Γ.rightOp.obj (Proj.restrict ⋯) ⟶ op (CommRingCat.of (A⁰_ f))) →
                  Proj.restrict ⋯ ⟶ «Spec».toLocallyRingedSpace.obj (op (CommRingCat.of (A⁰_ f))))
              (Quiver.Hom.op (awayToΓ 𝒜 f)))))
        U)

Tactic:
rfl