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 : (↑(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)
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 𝒜 ⋯)) :
          (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))
⊢ 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))

Tactic:
apply (Proj.stalkIso' 𝒜 x).eq_symm_apply.mpr

Premises used: Iff.mpr, AlgebraicGeometry.Proj.stalkIso', RingEquiv.eq_symm_apply
-- 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 : (↑(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 (α := 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 𝒜 ⋯)) :
          (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'_germ

Premises used: AlgebraicGeometry.Proj.stalkIso'_germ
-- 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 : (↑(CommRingCat.of (A⁰_ f)) : Type u_1)
p : ↥(unop (op (pbo f)))
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) ⋯ :
          (a : Localization (Submonoid.powers f)) →
            Localization (↑p : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)).asHomogeneousIdeal.toIdeal.primeCompl)
        (HomogeneousLocalization.mk x).val)
⊢ 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))

Tactic:
obtain ⟨x, rfl⟩ := HomogeneousLocalization.mk_surjective x

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
p : ↥(unop (op (pbo f)))
x : HomogeneousLocalization.NumDenSameDeg 𝒜 (Submonoid.powers f)
change :
  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)
⊢ 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)

Tactic:
change (HomogeneousLocalization.mapId 𝒜 _ _).val = _

Premises used: HomogeneousLocalization.mapId, DFunLike.coe, HomogeneousLocalization.val
-- 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
p : ↥(unop (op (pbo f)))
x : HomogeneousLocalization.NumDenSameDeg 𝒜 (Submonoid.powers f)
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) ⋯))
    ((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) ⋯)))
⊢ 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)

Tactic:
dsimp [HomogeneousLocalization.mapId, HomogeneousLocalization.map]

Premises used: HomogeneousLocalization.map, HomogeneousLocalization.mapId
-- 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
p : ↥(unop (op (pbo f)))
x : HomogeneousLocalization.NumDenSameDeg 𝒜 (Submonoid.powers f)
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) ⋯))
    (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)
                  ⋯) :
              A))
          ⋯ :
        ↥(↑p : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)).asHomogeneousIdeal.toIdeal.primeCompl))
⊢ 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) ⋯)))

Tactic:
rw [Localization.mk_eq_mk', Localization.mk_eq_mk', IsLocalization.map_mk']

Premises used: IsLocalization.map_mk', Localization.mk_eq_mk'
-- 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
p : ↥(unop (op (pbo f)))
x : HomogeneousLocalization.NumDenSameDeg 𝒜 (Submonoid.powers f)
⊢ 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) ⋯))
    (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)
                  ⋯) :
              A))
          ⋯ :
        ↥(↑p : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)).asHomogeneousIdeal.toIdeal.primeCompl))

Tactic:
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))
              ⋯).toPresheafedSpace :
        TopCat) :
    Type u_1)
⊢ Eq (α :=
    CommRingCat.of (A⁰_ f) ⟶
      CommRingCat.of (↑(Presheaf.stalk (Sheaf.presheaf (structureSheaf 𝒜)) (↑x : ProjectiveSpectrum 𝒜)) : Type u_1))
    (CategoryStruct.comp (Y :=
      CommRingCat.of
        (HomogeneousLocalization 𝒜
          (Ideal.primeCompl
            (HomogeneousIdeal.toIdeal.{0, u_2, u_1} (σ := σ) (𝒜 := 𝒜)
              (ProjectiveSpectrum.asHomogeneousIdeal
                ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
                      carrier) (X :=
                      Functor.obj (C := Opens (ProjectiveSpectrum 𝒜))
                        (Opens.toTopCat (TopCat.of (ProjectiveSpectrum 𝒜))) (pbo f))
                      (Opens.inclusion' (pbo f)) :
                    (a : (↑((Opens.toTopCat (TopCat.of (ProjectiveSpectrum 𝒜))).obj (pbo f)) : Type u_1)) →
                      (↑{ carrier := TopCat.of (ProjectiveSpectrum 𝒜), presheaf := (structureSheaf 𝒜).obj, IsSheaf := ⋯,
                              isLocalRing := ⋯ }.toTopCat :
                        Type u_1))
                  x))))))
      (CommRingCat.ofHom (HomogeneousLocalization.mapId 𝒜 ⋯))
      (Iso.inv
        (RingEquiv.toCommRingCatIso
          («Proj».stalkIso' 𝒜
            ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC :=
                  carrier) (X :=
                  Functor.obj (C := Opens (ProjectiveSpectrum 𝒜)) (Opens.toTopCat (TopCat.of (ProjectiveSpectrum 𝒜)))
                    (pbo f))
                  (Opens.inclusion' (pbo f)) :
                (a : (↑((Opens.toTopCat (TopCat.of (ProjectiveSpectrum 𝒜))).obj (pbo f)) : Type u_1)) →
                  (↑{ carrier := TopCat.of (ProjectiveSpectrum 𝒜), presheaf := (structureSheaf 𝒜).obj, IsSheaf := ⋯,
                          isLocalRing := ⋯ }.toTopCat :
                    Type u_1))
              x)))))
    (CategoryStruct.comp (Y :=
      CommRingCat.of (HomogeneousLocalization 𝒜 (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl))
      (CommRingCat.ofHom (HomogeneousLocalization.mapId 𝒜 ⋯))
      (Iso.inv (RingEquiv.toCommRingCatIso («Proj».stalkIso' 𝒜 (↑x : ProjectiveSpectrum 𝒜)))))

Tactic:
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)
change :
  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))
⊢ 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)))

Tactic:
change PrimeSpectrum.comap (awayToΓ 𝒜 f ≫ (Proj| pbo f).presheaf.Γgerm x).hom
        (IsLocalRing.closedPoint ((Proj| pbo f).presheaf.stalk x)) = _

Premises used: CommRingCat.Hom.hom, CommRingCat.carrier, ProjectiveSpectrum.basicOpen, AlgebraicGeometry.Proj.toLocallyRingedSpace, TopologicalSpace.Opens.isOpenEmbedding, TopCat.Presheaf.stalk, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, TopCat.Presheaf.Γgerm, AlgebraicGeometry.LocallyRingedSpace.restrict, IsLocalRing.closedPoint, CategoryTheory.CategoryStruct.comp, AlgebraicGeometry.ProjectiveSpectrum.Proj.awayToΓ, AlgebraicGeometry.PresheafedSpace.presheaf, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, PrimeSpectrum.comap