awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
Goal:
σ : Type u_1
A : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
X : Scheme
f : A →+* (↑Γ(X, ⊤) : Type u)
hf : Eq (α := Ideal (↑Γ(X, ⊤) : Type u)) (Ideal.map f (HomogeneousIdeal.toIdeal (HomogeneousIdeal.irrelevant 𝒜))) ⊤
⊢ Eq (α := X ⟶ Spec (CommRingCat.of ↥(𝒜 0))) (fromOfGlobalSections 𝒜 f hf ≫ toSpecZero 𝒜)
    (X.toSpecΓ ≫ Spec.map (CommRingCat.ofHom (f.comp (algebraMap (↥(𝒜 0)) A))))

Tactic:
(openCoverOfMapIrrelevantEqTop 𝒜 f hf).hom_ext _ _ fun x ↦ ?_

Premises used: AlgebraicGeometry.Scheme.Cover.hom_ext, AlgebraicGeometry.Proj.openCoverOfMapIrrelevantEqTop
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
Goal:
σ : Type u_1
A : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
X : Scheme
f : A →+* (↑Γ(X, ⊤) : Type u)
hf : Eq (α := Ideal (↑Γ(X, ⊤) : Type u)) (Ideal.map f (HomogeneousIdeal.toIdeal (HomogeneousIdeal.irrelevant 𝒜))) ⊤
refine :
  ∀ (x : (openCoverOfMapIrrelevantEqTop 𝒜 f hf).I₀),
    Eq (α := (openCoverOfMapIrrelevantEqTop 𝒜 f hf).X x ⟶ Spec (CommRingCat.of ↥(𝒜 0)))
      ((openCoverOfMapIrrelevantEqTop 𝒜 f hf).f x ≫ fromOfGlobalSections 𝒜 f hf ≫ toSpecZero 𝒜)
      ((openCoverOfMapIrrelevantEqTop 𝒜 f hf).f x ≫
        X.toSpecΓ ≫ Spec.map (CommRingCat.ofHom (f.comp (algebraMap (↥(𝒜 0)) A))))
⊢ Eq (α := X ⟶ Spec (CommRingCat.of ↥(𝒜 0))) (fromOfGlobalSections 𝒜 f hf ≫ toSpecZero 𝒜)
    (X.toSpecΓ ≫ Spec.map (CommRingCat.ofHom (f.comp (algebraMap (↥(𝒜 0)) A))))

Tactic:
refine (openCoverOfMapIrrelevantEqTop 𝒜 f hf).hom_ext _ _ fun x ↦ ?_

Premises used: AlgebraicGeometry.Scheme.Cover.hom_ext, AlgebraicGeometry.Proj.openCoverOfMapIrrelevantEqTop
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
σ : Type u_4
τ : Type u_5
ψ : Type u_6
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
inst_3 : CommRing B
inst_4 : SetLike τ B
inst_5 : AddSubgroupClass τ B
inst_6 : CommRing C
inst_7 : SetLike ψ C
inst_8 : AddSubgroupClass ψ C
𝒜 : ℕ → σ
ℬ : ℕ → τ
𝒞 : ℕ → ψ
inst_9 : GradedRing 𝒜
inst_10 : GradedRing ℬ
inst_11 : GradedRing 𝒞
f : 𝒜 →+*ᵍ ℬ
g : ℬ →+*ᵍ 𝒞
hf : LE.le (α := HomogeneousIdeal ℬ) (ℬ₊) (HomogeneousIdeal.map f (𝒜₊))
hg : LE.le (α := HomogeneousIdeal 𝒞) (𝒞₊) (HomogeneousIdeal.map g (ℬ₊))
simp_rw :
  ∀ (a : Set A),
    ∃ (s : Set B),
      Eq (α := Set (ProjectiveSpectrum ℬ))
        (Set.preimage (β := ProjectiveSpectrum 𝒜) (comapFun f hf : (p : ProjectiveSpectrum ℬ) → ProjectiveSpectrum 𝒜)
            (zeroLocus 𝒜 a : Set (ProjectiveSpectrum 𝒜)) :
          Set (ProjectiveSpectrum ℬ))
        (zeroLocus ℬ s : Set (ProjectiveSpectrum ℬ))
⊢ Continuous (X := ProjectiveSpectrum ℬ) (Y := ProjectiveSpectrum 𝒜)
    (comapFun f hf : (p : ProjectiveSpectrum ℬ) → ProjectiveSpectrum 𝒜)

Tactic:
simp_rw [continuous_iff_isClosed, isClosed_iff_zeroLocus, exists_imp, forall_eq_apply_imp_iff]

Premises used: continuous_iff_isClosed, ProjectiveSpectrum.isClosed_iff_zeroLocus, forall_eq_apply_imp_iff, exists_imp
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
σ : Type u_4
τ : Type u_5
ψ : Type u_6
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
inst_3 : CommRing B
inst_4 : SetLike τ B
inst_5 : AddSubgroupClass τ B
inst_6 : CommRing C
inst_7 : SetLike ψ C
inst_8 : AddSubgroupClass ψ C
𝒜 : ℕ → σ
ℬ : ℕ → τ
𝒞 : ℕ → ψ
inst_9 : GradedRing 𝒜
inst_10 : GradedRing ℬ
inst_11 : GradedRing 𝒞
f : 𝒜 →+*ᵍ ℬ
g : ℬ →+*ᵍ 𝒞
hf : LE.le (α := HomogeneousIdeal ℬ) (ℬ₊) (HomogeneousIdeal.map f (𝒜₊))
hg : LE.le (α := HomogeneousIdeal 𝒞) (𝒞₊) (HomogeneousIdeal.map g (ℬ₊))
s : Set A
h :
  ∀ (x : ProjectiveSpectrum ℬ),
    Membership.mem (γ := Set (ProjectiveSpectrum ℬ))
        (Set.preimage (β := ProjectiveSpectrum 𝒜) (comapFun f hf : (p : ProjectiveSpectrum ℬ) → ProjectiveSpectrum 𝒜)
            (zeroLocus 𝒜 s : Set (ProjectiveSpectrum 𝒜)) :
          Set (ProjectiveSpectrum ℬ))
        x ↔
      Membership.mem (γ := Set (ProjectiveSpectrum ℬ)) (zeroLocus ℬ ((⇑f : (a : A) → B) '' s)) x
⊢ Eq (α := Set (ProjectiveSpectrum ℬ))
    (Set.preimage (β := ProjectiveSpectrum 𝒜) (comapFun f hf : (p : ProjectiveSpectrum ℬ) → ProjectiveSpectrum 𝒜)
        (zeroLocus 𝒜 s : Set (ProjectiveSpectrum 𝒜)) :
      Set (ProjectiveSpectrum ℬ))
    (zeroLocus ℬ ((⇑f : (a : A) → B) '' s) : Set (ProjectiveSpectrum ℬ))

Tactic:
ext
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
σ : Type u_4
τ : Type u_5
ψ : Type u_6
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
inst_3 : CommRing B
inst_4 : SetLike τ B
inst_5 : AddSubgroupClass τ B
inst_6 : CommRing C
inst_7 : SetLike ψ C
inst_8 : AddSubgroupClass ψ C
𝒜 : ℕ → σ
ℬ : ℕ → τ
𝒞 : ℕ → ψ
inst_9 : GradedRing 𝒜
inst_10 : GradedRing ℬ
inst_11 : GradedRing 𝒞
f : 𝒜 →+*ᵍ ℬ
g : ℬ →+*ᵍ 𝒞
hf : LE.le (α := HomogeneousIdeal ℬ) (ℬ₊) (HomogeneousIdeal.map f (𝒜₊))
hg : LE.le (α := HomogeneousIdeal 𝒞) (𝒞₊) (HomogeneousIdeal.map g (ℬ₊))
s : Set A
x : ProjectiveSpectrum ℬ
⊢ Membership.mem (γ := Set (ProjectiveSpectrum ℬ))
      (Set.preimage (β := ProjectiveSpectrum 𝒜) (comapFun f hf : (p : ProjectiveSpectrum ℬ) → ProjectiveSpectrum 𝒜)
          (zeroLocus 𝒜 s : Set (ProjectiveSpectrum 𝒜)) :
        Set (ProjectiveSpectrum ℬ))
      x ↔
    Membership.mem (γ := Set (ProjectiveSpectrum ℬ)) (zeroLocus ℬ ((⇑f : (a : A) → B) '' s)) x

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
σ : Type u_4
τ : Type u_5
ψ : Type u_6
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
inst_3 : CommRing B
inst_4 : SetLike τ B
inst_5 : AddSubgroupClass τ B
inst_6 : CommRing C
inst_7 : SetLike ψ C
inst_8 : AddSubgroupClass ψ C
𝒜 : ℕ → σ
ℬ : ℕ → τ
𝒞 : ℕ → ψ
inst_9 : GradedRing 𝒜
inst_10 : GradedRing ℬ
inst_11 : GradedRing 𝒞
f : 𝒜 →+*ᵍ ℬ
g : ℬ →+*ᵍ 𝒞
hf : LE.le (α := HomogeneousIdeal ℬ) (ℬ₊) (HomogeneousIdeal.map f (𝒜₊))
hg : LE.le (α := HomogeneousIdeal 𝒞) (𝒞₊) (HomogeneousIdeal.map g (ℬ₊))
⊢ ∀ (a : Set A),
    ∃ (s : Set B),
      Eq (α := Set (ProjectiveSpectrum ℬ))
        (Set.preimage (β := ProjectiveSpectrum 𝒜) (comapFun f hf : (p : ProjectiveSpectrum ℬ) → ProjectiveSpectrum 𝒜)
            (zeroLocus 𝒜 a : Set (ProjectiveSpectrum 𝒜)) :
          Set (ProjectiveSpectrum ℬ))
        (zeroLocus ℬ s : Set (ProjectiveSpectrum ℬ))

Tactic:
exact fun s ↦ ⟨f '' s, by ext; simp⟩
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
σ : Type u_4
τ : Type u_5
ψ : Type u_6
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
inst_3 : CommRing B
inst_4 : SetLike τ B
inst_5 : AddSubgroupClass τ B
inst_6 : CommRing C
inst_7 : SetLike ψ C
inst_8 : AddSubgroupClass ψ C
𝒜 : ℕ → σ
ℬ : ℕ → τ
𝒞 : ℕ → ψ
inst_9 : GradedRing 𝒜
inst_10 : GradedRing ℬ
inst_11 : GradedRing 𝒞
f : 𝒜 →+*ᵍ ℬ
g : ℬ →+*ᵍ 𝒞
hf : LE.le (α := HomogeneousIdeal ℬ) (ℬ₊) (HomogeneousIdeal.map f (𝒜₊))
hg : LE.le (α := HomogeneousIdeal 𝒞) (𝒞₊) (HomogeneousIdeal.map g (ℬ₊))
U : Opens (ProjectiveSpectrum 𝒜)
V : Opens (ProjectiveSpectrum ℬ)
hUV :
  V.carrier ⊆
    (⇑(ProjectiveSpectrum.comap f hf : ContinuousMap.{u_2, u_1} (ProjectiveSpectrum ℬ) (ProjectiveSpectrum 𝒜)) :
        (a : ProjectiveSpectrum ℬ) → ProjectiveSpectrum 𝒜) ⁻¹'
      U.carrier
x : ↥(Opposite.unop (Opposite.op V))
⊢ val
      ((↑(Subtype.mk (p :=
              fun
                (f :
                  (x : ↥(Opposite.unop (Opposite.op V))) →
                    (fun (x : (↑(top ℬ) : Type u_2)) ↦ AtPrime ℬ x.asHomogeneousIdeal.toIdeal)
                      (↑x : (↑(top ℬ) : Type u_2))) ↦
              TopCat.PrelocalPredicate.pred (X := top ℬ) (T := fun (x : (↑(top ℬ) : Type u_2)) ↦
                AtPrime ℬ x.asHomogeneousIdeal.toIdeal)
                (TopCat.LocalPredicate.toPrelocalPredicate (T := fun (x : (↑(top ℬ) : Type u_2)) ↦
                    AtPrime ℬ x.asHomogeneousIdeal.toIdeal) (ProjectiveSpectrum.StructureSheaf.isLocallyFraction ℬ) :
                  TopCat.PrelocalPredicate (X := top ℬ) fun (x : (↑(top ℬ) : Type u_2)) ↦
                    AtPrime ℬ x.asHomogeneousIdeal.toIdeal)
                f)
              (comapStructureSheafFun f hf U (Opposite.unop (Opposite.op V)) hUV
                (↑1 :
                  (x : ↥(Opposite.unop (Opposite.op U))) →
                    (fun (x : (↑(top 𝒜) : Type u_1)) ↦ AtPrime 𝒜 x.asHomogeneousIdeal.toIdeal)
                      (↑x : (↑(top 𝒜) : Type u_1))))
              ⋯) :
          (x : ↥(Opposite.unop (Opposite.op V))) →
            (fun (x : (↑(top ℬ) : Type u_2)) ↦ AtPrime ℬ x.asHomogeneousIdeal.toIdeal) (↑x : (↑(top ℬ) : Type u_2)))
        x) =
    val.{0, u_2, u_5} (ι := ℕ) (σ := τ) (𝒜 := ℬ)
      ((↑1 :
          (x : ↥(Opposite.unop (Opposite.op V))) →
            (fun (x : (↑(top ℬ) : Type u_2)) ↦ AtPrime ℬ x.asHomogeneousIdeal.toIdeal) (↑x : (↑(top ℬ) : Type u_2)))
        x)

Tactic:
simp [comapStructureSheafFun]

Premises used: AlgebraicGeometry.Proj.comapStructureSheafFun
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
σ : Type u_4
τ : Type u_5
ψ : Type u_6
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
inst_3 : CommRing B
inst_4 : SetLike τ B
inst_5 : AddSubgroupClass τ B
inst_6 : CommRing C
inst_7 : SetLike ψ C
inst_8 : AddSubgroupClass ψ C
𝒜 : ℕ → σ
ℬ : ℕ → τ
𝒞 : ℕ → ψ
inst_9 : GradedRing 𝒜
inst_10 : GradedRing ℬ
inst_11 : GradedRing 𝒞
f : 𝒜 →+*ᵍ ℬ
g : ℬ →+*ᵍ 𝒞
hf : LE.le (α := HomogeneousIdeal ℬ) (ℬ₊) (HomogeneousIdeal.map f (𝒜₊))
hg : LE.le (α := HomogeneousIdeal 𝒞) (𝒞₊) (HomogeneousIdeal.map g (ℬ₊))
U : Opens (ProjectiveSpectrum 𝒜)
V : Opens (ProjectiveSpectrum ℬ)
hUV :
  V.carrier ⊆
    (⇑(ProjectiveSpectrum.comap f hf : ContinuousMap.{u_2, u_1} (ProjectiveSpectrum ℬ) (ProjectiveSpectrum 𝒜)) :
        (a : ProjectiveSpectrum ℬ) → ProjectiveSpectrum 𝒜) ⁻¹'
      U.carrier
x : ↥(Opposite.unop (Opposite.op V))
⊢ val
      ((↑(Subtype.mk (p :=
              fun
                (f :
                  (x : ↥(Opposite.unop (Opposite.op V))) →
                    (fun (x : (↑(top ℬ) : Type u_2)) ↦ AtPrime ℬ x.asHomogeneousIdeal.toIdeal)
                      (↑x : (↑(top ℬ) : Type u_2))) ↦
              TopCat.PrelocalPredicate.pred (X := top ℬ) (T := fun (x : (↑(top ℬ) : Type u_2)) ↦
                AtPrime ℬ x.asHomogeneousIdeal.toIdeal)
                (TopCat.LocalPredicate.toPrelocalPredicate (T := fun (x : (↑(top ℬ) : Type u_2)) ↦
                    AtPrime ℬ x.asHomogeneousIdeal.toIdeal) (ProjectiveSpectrum.StructureSheaf.isLocallyFraction ℬ) :
                  TopCat.PrelocalPredicate (X := top ℬ) fun (x : (↑(top ℬ) : Type u_2)) ↦
                    AtPrime ℬ x.asHomogeneousIdeal.toIdeal)
                f)
              (comapStructureSheafFun f hf U (Opposite.unop (Opposite.op V)) hUV
                (↑0 :
                  (x : ↥(Opposite.unop (Opposite.op U))) →
                    (fun (x : (↑(top 𝒜) : Type u_1)) ↦ AtPrime 𝒜 x.asHomogeneousIdeal.toIdeal)
                      (↑x : (↑(top 𝒜) : Type u_1))))
              ⋯) :
          (x : ↥(Opposite.unop (Opposite.op V))) →
            (fun (x : (↑(top ℬ) : Type u_2)) ↦ AtPrime ℬ x.asHomogeneousIdeal.toIdeal) (↑x : (↑(top ℬ) : Type u_2)))
        x) =
    val.{0, u_2, u_5} (ι := ℕ) (σ := τ) (𝒜 := ℬ)
      ((↑0 :
          (x : ↥(Opposite.unop (Opposite.op V))) →
            (fun (x : (↑(top ℬ) : Type u_2)) ↦ AtPrime ℬ x.asHomogeneousIdeal.toIdeal) (↑x : (↑(top ℬ) : Type u_2)))
        x)

Tactic:
simp [comapStructureSheafFun]

Premises used: AlgebraicGeometry.Proj.comapStructureSheafFun
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor
Goal:
A σ : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
p : (↑(top 𝒜) : Type u)
c : NumDenSameDeg 𝒜 p.asHomogeneousIdeal.toIdeal.primeCompl
q : ↥(ProjectiveSpectrum.basicOpen 𝒜 (↑c.den : A))
⊢ Eq (α := Localization (M := A) (↑q : (↑(top 𝒜) : Type u)).asHomogeneousIdeal.toIdeal.primeCompl)
    (val (ι := ℕ) (σ := σ) (𝒜 := 𝒜)
      ((↑(sectionInBasicOpen 𝒜 p c) :
          (x : ↥(Opposite.unop (Opposite.op (ProjectiveSpectrum.basicOpen 𝒜 (↑c.den : A))))) →
            (fun (x : (↑(top 𝒜) : Type u)) ↦ AtPrime 𝒜 x.asHomogeneousIdeal.toIdeal) (↑x : (↑(top 𝒜) : Type u)))
        q))
    (Localization.mk (↑c.num : A)
      (Subtype.mk (p := fun (x : A) ↦ x ∈ (↑q : (↑(top 𝒜) : Type u)).asHomogeneousIdeal.toIdeal.primeCompl) (↑c.den : A)
        ⋯))

Tactic:
rfl

Premises used: Localization.mk, Quotient.mk', OreLocalization.oreDiv, rfl, HomogeneousLocalization.NumDenSameDeg.embedding, HomogeneousLocalization.val
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor
Goal:
A B σ τ : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
inst_3 : CommRing B
inst_4 : SetLike τ B
inst_5 : AddSubgroupClass τ B
𝒜 : ℕ → σ
ℬ : ℕ → τ
inst_6 : GradedRing 𝒜
inst_7 : GradedRing ℬ
f : 𝒜 →+*ᵍ ℬ
hf : LE.le (α := HomogeneousIdeal ℬ) (ℬ₊) (HomogeneousIdeal.map f (𝒜₊))
p : ProjectiveSpectrum ℬ
rw : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
rw [← Iso.eq_inv_comp, Iso.comp_inv_eq]

Premises used: CategoryTheory.Iso.comp_inv_eq, CategoryTheory.Iso.eq_inv_comp
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor
Goal:
A B σ τ : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
inst_3 : CommRing B
inst_4 : SetLike τ B
inst_5 : AddSubgroupClass τ B
𝒜 : ℕ → σ
ℬ : ℕ → τ
inst_6 : GradedRing 𝒜
inst_7 : GradedRing ℬ
f : 𝒜 →+*ᵍ ℬ
hf : LE.le (α := HomogeneousIdeal ℬ) (ℬ₊) (HomogeneousIdeal.map f (𝒜₊))
p : ProjectiveSpectrum ℬ
hf₁ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
ext : 1
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor
Goal:
A B σ τ : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
inst_3 : CommRing B
inst_4 : SetLike τ B
inst_5 : AddSubgroupClass τ B
𝒜 : ℕ → σ
ℬ : ℕ → τ
inst_6 : GradedRing 𝒜
inst_7 : GradedRing ℬ
f : 𝒜 →+*ᵍ ℬ
hf : LE.le (α := HomogeneousIdeal ℬ) (ℬ₊) (HomogeneousIdeal.map f (𝒜₊))
p : ProjectiveSpectrum ℬ
hf₁ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
ext x : 2
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor
Goal:
A B σ τ : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
inst_3 : CommRing B
inst_4 : SetLike τ B
inst_5 : AddSubgroupClass τ B
𝒜 : ℕ → σ
ℬ : ℕ → τ
inst_6 : GradedRing 𝒜
inst_7 : GradedRing ℬ
f : 𝒜 →+*ᵍ ℬ
hf : LE.le (α := HomogeneousIdeal ℬ) (ℬ₊) (HomogeneousIdeal.map f (𝒜₊))
p : ProjectiveSpectrum ℬ
x :
  AtPrime 𝒜
    (toIdeal (σ := σ) (𝒜 := 𝒜)
      (asHomogeneousIdeal
        (((ProjectiveSpectrum.comap f hf : C(ProjectiveSpectrum ℬ, ProjectiveSpectrum 𝒜)) :
            (a : ProjectiveSpectrum ℬ) → ProjectiveSpectrum 𝒜)
          p)))
hf₁ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

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

Premises used: HomogeneousLocalization.mk_surjective, rfl
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor
Goal:
A B σ τ : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
inst_3 : CommRing B
inst_4 : SetLike τ B
inst_5 : AddSubgroupClass τ B
𝒜 : ℕ → σ
ℬ : ℕ → τ
inst_6 : GradedRing 𝒜
inst_7 : GradedRing ℬ
f : 𝒜 →+*ᵍ ℬ
hf : LE.le (α := HomogeneousIdeal ℬ) (ℬ₊) (HomogeneousIdeal.map f (𝒜₊))
p : ProjectiveSpectrum ℬ
c :
  NumDenSameDeg 𝒜
    (Ideal.primeCompl
      (toIdeal (σ := σ) (𝒜 := 𝒜)
        (asHomogeneousIdeal
          (((ProjectiveSpectrum.comap f hf : C(ProjectiveSpectrum ℬ, ProjectiveSpectrum 𝒜)) :
              (a : ProjectiveSpectrum ℬ) → ProjectiveSpectrum 𝒜)
            p))))
hf₁ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
simp only [val_localRingHom, val_mk, RingHom.comp_apply]

Premises used: HomogeneousLocalization.val_mk, HomogeneousLocalization.val_localRingHom, RingHom.comp_apply
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor
Goal:
A B σ τ : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
inst_3 : CommRing B
inst_4 : SetLike τ B
inst_5 : AddSubgroupClass τ B
𝒜 : ℕ → σ
ℬ : ℕ → τ
inst_6 : GradedRing 𝒜
inst_7 : GradedRing ℬ
f : 𝒜 →+*ᵍ ℬ
hf : LE.le (α := HomogeneousIdeal ℬ) (ℬ₊) (HomogeneousIdeal.map f (𝒜₊))
p : ProjectiveSpectrum ℬ
c :
  NumDenSameDeg 𝒜
    (Ideal.primeCompl
      (toIdeal (σ := σ) (𝒜 := 𝒜)
        (asHomogeneousIdeal
          (((ProjectiveSpectrum.comap f hf : C(ProjectiveSpectrum ℬ, ProjectiveSpectrum 𝒜)) :
              (a : ProjectiveSpectrum ℬ) → ProjectiveSpectrum 𝒜)
            p))))
hf₁ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
simp only [GradedRingHom.toRingHom_eq_toRingHom, Localization.localRingHom_mk,
    GradedRingHom.coe_toRingHom]

Premises used: GradedRingHom.coe_toRingHom, GradedRingHom.toRingHom_eq_toRingHom, Localization.localRingHom_mk
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor
Goal:
A B σ τ : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
inst_3 : CommRing B
inst_4 : SetLike τ B
inst_5 : AddSubgroupClass τ B
𝒜 : ℕ → σ
ℬ : ℕ → τ
inst_6 : GradedRing 𝒜
inst_7 : GradedRing ℬ
f : 𝒜 →+*ᵍ ℬ
hf : LE.le (α := HomogeneousIdeal ℬ) (ℬ₊) (HomogeneousIdeal.map f (𝒜₊))
p : ProjectiveSpectrum ℬ
c :
  NumDenSameDeg 𝒜
    (Ideal.primeCompl
      (toIdeal (σ := σ) (𝒜 := 𝒜)
        (asHomogeneousIdeal
          (((ProjectiveSpectrum.comap f hf : C(ProjectiveSpectrum ℬ, ProjectiveSpectrum 𝒜)) :
              (a : ProjectiveSpectrum ℬ) → ProjectiveSpectrum 𝒜)
            p))))
hf₁ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
erw [stalkIso'_symm_mk]

Premises used: AlgebraicGeometry.Proj.stalkIso'_symm_mk
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor
Goal:
A B σ τ : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
inst_3 : CommRing B
inst_4 : SetLike τ B
inst_5 : AddSubgroupClass τ B
𝒜 : ℕ → σ
ℬ : ℕ → τ
inst_6 : GradedRing 𝒜
inst_7 : GradedRing ℬ
f : 𝒜 →+*ᵍ ℬ
hf : LE.le (α := HomogeneousIdeal ℬ) (ℬ₊) (HomogeneousIdeal.map f (𝒜₊))
p : ProjectiveSpectrum ℬ
c :
  NumDenSameDeg 𝒜
    (Ideal.primeCompl
      (toIdeal (σ := σ) (𝒜 := 𝒜)
        (asHomogeneousIdeal
          (((ProjectiveSpectrum.comap f hf : C(ProjectiveSpectrum ℬ, ProjectiveSpectrum 𝒜)) :
              (a : ProjectiveSpectrum ℬ) → ProjectiveSpectrum 𝒜)
            p))))
⊢ Eq (α := Localization (M := B) p.asHomogeneousIdeal.toIdeal.primeCompl)
    (Localization.mk ((f : (a : A) → B) (↑c.num : A))
        (Subtype.mk (p := fun (x : B) ↦ x ∈ p.asHomogeneousIdeal.toIdeal.primeCompl) ((f : (a : A) → B) (↑c.den : A))
          ⋯) :
      Localization (M := B) p.asHomogeneousIdeal.toIdeal.primeCompl)
    (val (ι := ℕ) (σ := τ) (𝒜 := ℬ)
        ((↑(sectionInBasicOpen ℬ p (NumDenSameDeg.map f ⋯ c)) :
            (x : ↥(Opposite.unop (Opposite.op (ProjectiveSpectrum.basicOpen ℬ ((f : (a : A) → B) (↑c.den : A)))))) →
              (fun (x : (↑(top ℬ) : Type u)) ↦ AtPrime ℬ x.asHomogeneousIdeal.toIdeal) (↑x : (↑(top ℬ) : Type u)))
          (Subtype.mk (p := fun (x : (↑(top ℬ) : Type u)) ↦
            Membership.mem (γ := Opens (↑(top ℬ) : Type u))
              (Opposite.unop (Opposite.op (ProjectiveSpectrum.basicOpen ℬ ((f : (a : A) → B) (↑c.den : A))))) x)
            p ⋯)) :
      Localization (M := B) p.asHomogeneousIdeal.toIdeal.primeCompl)

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor
Goal:
A B C σ τ ψ : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
inst_3 : CommRing B
inst_4 : SetLike τ B
inst_5 : AddSubgroupClass τ B
inst_6 : CommRing C
inst_7 : SetLike ψ C
inst_8 : AddSubgroupClass ψ C
𝒜 : ℕ → σ
ℬ : ℕ → τ
𝒞 : ℕ → ψ
inst_9 : GradedRing 𝒜
inst_10 : GradedRing ℬ
inst_11 : GradedRing 𝒞
f : 𝒜 →+*ᵍ ℬ
g : ℬ →+*ᵍ 𝒞
hf : LE.le (α := HomogeneousIdeal ℬ) (ℬ₊) (HomogeneousIdeal.map f (𝒜₊))
hg : LE.le (α := HomogeneousIdeal 𝒞) (𝒞₊) (HomogeneousIdeal.map g (ℬ₊))
p : ↥(Proj ℬ)
x :
  (↑((Proj 𝒜).presheaf.stalk
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
              (X := (↑(Proj ℬ).toPresheafedSpace : TopCat)) (Y := (↑(Proj 𝒜).toPresheafedSpace : TopCat))
              (PresheafedSpace.Hom.base (InducedCategory.Hom.hom (sheafedSpaceMap f hf))) :
            (a : ↥(Proj ℬ)) → ↥(Proj 𝒜))
          p)) :
    Type u)
hx :
  IsUnit (M := (↑((Proj ℬ).presheaf.stalk p) : Type u))
    ((CommRingCat.Hom.hom (stalkIso ℬ p).inv :
          (a : AtPrime ℬ p.asHomogeneousIdeal.toIdeal) → (↑((Proj ℬ).presheaf.stalk p) : Type u))
        ((localRingHom f
                (toIdeal (σ := σ) (𝒜 := 𝒜)
                  (asHomogeneousIdeal
                    (((ProjectiveSpectrum.comap f hf : C(ProjectiveSpectrum ℬ, ProjectiveSpectrum 𝒜)) :
                        (a : ProjectiveSpectrum ℬ) → ProjectiveSpectrum 𝒜)
                      p)))
                p.asHomogeneousIdeal.toIdeal ⋯ :
              (a :
                  AtPrime 𝒜
                    ((ProjectiveSpectrum.comap f hf : (a : ProjectiveSpectrum ℬ) → ProjectiveSpectrum 𝒜)
                          p).asHomogeneousIdeal.toIdeal) →
                AtPrime ℬ p.asHomogeneousIdeal.toIdeal)
            ((CommRingCat.Hom.hom
                  (Iso.hom
                    (stalkIso 𝒜
                      (((ProjectiveSpectrum.comap f hf : C(ProjectiveSpectrum ℬ, ProjectiveSpectrum 𝒜)) :
                          (a : ProjectiveSpectrum ℬ) → ProjectiveSpectrum 𝒜)
                        p))) :
                (a :
                    (↑((Proj 𝒜).presheaf.stalk
                          ((ConcreteCategory.hom (sheafedSpaceMap f hf).hom.base : (a : ↥(Proj ℬ)) → ↥(Proj 𝒜)) p)) :
                      Type u)) →
                  AtPrime 𝒜
                    ((ProjectiveSpectrum.comap f hf : (a : ProjectiveSpectrum ℬ) → ProjectiveSpectrum 𝒜)
                          p).asHomogeneousIdeal.toIdeal)
              x) :
          AtPrime ℬ p.asHomogeneousIdeal.toIdeal) :
      (↑((Proj ℬ).presheaf.stalk p) : Type u))
⊢ IsLocalHom (R := (↑(CommRingCat.of (AtPrime ℬ p.asHomogeneousIdeal.toIdeal)) : Type u)) (S :=
    (↑((Proj ℬ).presheaf.stalk p) : Type u)) (CommRingCat.Hom.hom (stalkIso ℬ p).inv)

Tactic:
have : IsLocalHom (stalkIso ℬ p).inv.hom := isLocalHom_of_isIso _
-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor
Goal:
A B σ τ : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
inst_3 : CommRing B
inst_4 : SetLike τ B
inst_5 : AddSubgroupClass τ B
𝒜 : ℕ → σ
ℬ : ℕ → τ
inst_6 : GradedRing 𝒜
inst_7 : GradedRing ℬ
f : 𝒜 →+*ᵍ ℬ
hf : LE.le (α := HomogeneousIdeal ℬ) (ℬ₊) (HomogeneousIdeal.map f (𝒜₊))
s : A
⊢ Eq (α := (Proj ℬ).Opens) (map f hf ⁻¹ᵁ basicOpen 𝒜 s) (basicOpen ℬ ((f : (a : A) → B) s))

Tactic:
rfl

Premises used: ProjectiveSpectrum.basicOpen, Set.Mem, setOf, AlgebraicGeometry.Proj.basicOpen, Set.preimage, Not, rfl