-- Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Scheme.lean
lemma fromSpec_toSpec {f : A} {m : ℕ} (f_deg : f ∈ 𝒜 m) (hm : 0 < m) (x : Proj.T| pbo f) :
    FromSpec.toFun f_deg hm (toSpec 𝒜 f x) = x

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 : ↑↑(Proj.restrict ⋯).toPresheafedSpace
i : ℕ
z : A
hzi : z ∈ 𝒜 i
⊢ z ∈ (↑(FromSpec.toFun f_deg hm ((ConcreteCategory.hom (toSpec 𝒜 f)) x))).asHomogeneousIdeal ↔
    z ∈ (↑x).asHomogeneousIdeal

Tactic:
refine (FromSpec.mem_carrier_iff_of_mem f_deg hm _ _ hzi).trans ?_

Result:
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 : ↑↑(Proj.restrict ⋯).toPresheafedSpace
i : ℕ
z : A
hzi : z ∈ 𝒜 i
⊢ HomogeneousLocalization.mk { deg := m * i, num := ⟨z ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ } ∈
      ((ConcreteCategory.hom (toSpec 𝒜 f)) x).asIdeal ↔
    z ∈ (↑x).asHomogeneousIdeal

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 : ↑↑(Proj.restrict ⋯).toPresheafedSpace
⊢ FromSpec.toFun f_deg hm ((ConcreteCategory.hom (toSpec 𝒜 f)) x) = x

Tactic:
refine Subtype.ext <| ProjectiveSpectrum.ext <| HomogeneousIdeal.ext' ?_

Result:
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 : ↑↑(Proj.restrict ⋯).toPresheafedSpace
⊢ ∀ (i : ℕ),
    ∀ x_1 ∈ 𝒜 i,
      x_1 ∈ (↑(FromSpec.toFun f_deg hm ((ConcreteCategory.hom (toSpec 𝒜 f)) x))).asHomogeneousIdeal ↔
        x_1 ∈ (↑x).asHomogeneousIdeal

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 : ↑↑(Proj.restrict ⋯).toPresheafedSpace
⊢ ∀ (i : ℕ),
    ∀ x_1 ∈ 𝒜 i,
      x_1 ∈ (↑(FromSpec.toFun f_deg hm ((ConcreteCategory.hom (toSpec 𝒜 f)) x))).asHomogeneousIdeal ↔
        x_1 ∈ (↑x).asHomogeneousIdeal

Tactic:
intros i z hzi

Result:
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 : ↑↑(Proj.restrict ⋯).toPresheafedSpace
i : ℕ
z : A
hzi : z ∈ 𝒜 i
⊢ z ∈ (↑(FromSpec.toFun f_deg hm ((ConcreteCategory.hom (toSpec 𝒜 f)) x))).asHomogeneousIdeal ↔
    z ∈ (↑x).asHomogeneousIdeal

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 : ↑↑(Proj.restrict ⋯).toPresheafedSpace
i : ℕ
z : A
hzi : z ∈ 𝒜 i
⊢ HomogeneousLocalization.mk { deg := m * i, num := ⟨z ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ } ∈
      ((ConcreteCategory.hom (toSpec 𝒜 f)) x).asIdeal ↔
    z ∈ (↑x).asHomogeneousIdeal

Tactic:
exact (ToSpec.mk_mem_carrier _ _).trans (x.1.2.pow_mem_iff_mem m hm)

Result:
no goals