-- Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Scheme.lean
lemma toSpec_fromSpec {f : A} {m : ℕ} (f_deg : f ∈ 𝒜 m) (hm : 0 < m) (x : Spec.T (A⁰_ f)) :
    toSpec 𝒜 f (FromSpec.toFun f_deg hm x) = x

Proof state:
case asIdeal
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
x : ↑↑(Spec A⁰_ f).toPresheafedSpace
⊢ ((ConcreteCategory.hom (toSpec 𝒜 f)) (FromSpec.toFun f_deg hm x)).asIdeal = x.asIdeal

Tactic:
ext z

Result:
case asIdeal.h
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
x : ↑↑(Spec A⁰_ f).toPresheafedSpace
z : ↑(CommRingCat.of (A⁰_ f))
⊢ z ∈ ((ConcreteCategory.hom (toSpec 𝒜 f)) (FromSpec.toFun f_deg hm x)).asIdeal ↔ z ∈ x.asIdeal

Proof state:
case asIdeal.h.intro
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
x : ↑↑(Spec A⁰_ f).toPresheafedSpace
z : HomogeneousLocalization.NumDenSameDeg 𝒜 (Submonoid.powers f)
⊢ HomogeneousLocalization.mk z ∈ ((ConcreteCategory.hom (toSpec 𝒜 f)) (FromSpec.toFun f_deg hm x)).asIdeal ↔
    ↑z.num ∈ FromSpec.carrier f_deg x

Tactic:
exact ToSpec.mk_mem_carrier _ z

Result:
no goals

Proof state:
case asIdeal.h
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
x : ↑↑(Spec A⁰_ f).toPresheafedSpace
z : ↑(CommRingCat.of (A⁰_ f))
⊢ z ∈ ((ConcreteCategory.hom (toSpec 𝒜 f)) (FromSpec.toFun f_deg hm x)).asIdeal ↔ z ∈ x.asIdeal

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

Result:
case asIdeal.h.intro
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
x : ↑↑(Spec A⁰_ f).toPresheafedSpace
z : HomogeneousLocalization.NumDenSameDeg 𝒜 (Submonoid.powers f)
⊢ HomogeneousLocalization.mk z ∈ ((ConcreteCategory.hom (toSpec 𝒜 f)) (FromSpec.toFun f_deg hm x)).asIdeal ↔
    HomogeneousLocalization.mk z ∈ x.asIdeal

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
x : ↑↑(Spec A⁰_ f).toPresheafedSpace
⊢ (ConcreteCategory.hom (toSpec 𝒜 f)) (FromSpec.toFun f_deg hm x) = x

Tactic:
apply PrimeSpectrum.ext

Result:
case asIdeal
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
x : ↑↑(Spec A⁰_ f).toPresheafedSpace
⊢ ((ConcreteCategory.hom (toSpec 𝒜 f)) (FromSpec.toFun f_deg hm x)).asIdeal = x.asIdeal

Proof state:
case asIdeal.h.intro
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
x : ↑↑(Spec A⁰_ f).toPresheafedSpace
z : HomogeneousLocalization.NumDenSameDeg 𝒜 (Submonoid.powers f)
⊢ HomogeneousLocalization.mk z ∈ ((ConcreteCategory.hom (toSpec 𝒜 f)) (FromSpec.toFun f_deg hm x)).asIdeal ↔
    HomogeneousLocalization.mk z ∈ x.asIdeal

Tactic:
rw [← FromSpec.num_mem_carrier_iff f_deg hm x]

Result:
case asIdeal.h.intro
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
x : ↑↑(Spec A⁰_ f).toPresheafedSpace
z : HomogeneousLocalization.NumDenSameDeg 𝒜 (Submonoid.powers f)
⊢ HomogeneousLocalization.mk z ∈ ((ConcreteCategory.hom (toSpec 𝒜 f)) (FromSpec.toFun f_deg hm x)).asIdeal ↔
    ↑z.num ∈ FromSpec.carrier f_deg x