-- Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Scheme.lean
theorem carrier.denom_not_mem : f ∉ carrier.asIdeal f_deg hm q := fun rid =>
  q.isPrime.ne_top <|
    (Ideal.eq_top_iff_one _).mpr
      (by
        convert rid m
        rw [HomogeneousLocalization.ext_iff_val, HomogeneousLocalization.val_one,
          HomogeneousLocalization.val_mk]
        dsimp
        simp_rw [decompose_of_mem_same _ f_deg]
        simp only [mk_eq_monoidOf_mk', Submonoid.LocalizationMap.mk'_self])

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
q : ↑↑(Spec A⁰_ f).toPresheafedSpace
rid : f ∈ asIdeal f_deg hm q
⊢ 1 ∈ q.asIdeal

Tactic:
convert rid m

Result:
case h.e'_5
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
q : ↑↑(Spec A⁰_ f).toPresheafedSpace
rid : f ∈ asIdeal f_deg hm q
⊢ 1 = HomogeneousLocalization.mk { deg := m * m, num := ⟨(proj 𝒜 m) f ^ m, ⋯⟩, den := ⟨f ^ m, ⋯⟩, den_mem := ⋯ }

Proof state:
case h.e'_5
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
q : ↑↑(Spec A⁰_ f).toPresheafedSpace
rid : f ∈ asIdeal f_deg hm q
⊢ 1 = HomogeneousLocalization.mk { deg := m * m, num := ⟨(proj 𝒜 m) f ^ m, ⋯⟩, den := ⟨f ^ m, ⋯⟩, den_mem := ⋯ }

Tactic:
rw [HomogeneousLocalization.ext_iff_val, HomogeneousLocalization.val_one,
  HomogeneousLocalization.val_mk]

Result:
case h.e'_5
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
q : ↑↑(Spec A⁰_ f).toPresheafedSpace
rid : f ∈ asIdeal f_deg hm q
⊢ 1 =
    Localization.mk ↑{ deg := m * m, num := ⟨(proj 𝒜 m) f ^ m, ⋯⟩, den := ⟨f ^ m, ⋯⟩, den_mem := ⋯ }.num
      ⟨↑{ deg := m * m, num := ⟨(proj 𝒜 m) f ^ m, ⋯⟩, den := ⟨f ^ m, ⋯⟩, den_mem := ⋯ }.den, ⋯⟩

Proof state:
case h.e'_5
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
q : ↑↑(Spec A⁰_ f).toPresheafedSpace
rid : f ∈ asIdeal f_deg hm q
⊢ 1 = Localization.mk (f ^ m) ⟨f ^ m, ⋯⟩

Tactic:
simp only [mk_eq_monoidOf_mk', Submonoid.LocalizationMap.mk'_self]

Result:
no goals

Proof state:
case h.e'_5
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
q : ↑↑(Spec A⁰_ f).toPresheafedSpace
rid : f ∈ asIdeal f_deg hm q
⊢ 1 =
    Localization.mk ↑{ deg := m * m, num := ⟨(proj 𝒜 m) f ^ m, ⋯⟩, den := ⟨f ^ m, ⋯⟩, den_mem := ⋯ }.num
      ⟨↑{ deg := m * m, num := ⟨(proj 𝒜 m) f ^ m, ⋯⟩, den := ⟨f ^ m, ⋯⟩, den_mem := ⋯ }.den, ⋯⟩

Tactic:
dsimp

Result:
case h.e'_5
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
q : ↑↑(Spec A⁰_ f).toPresheafedSpace
rid : f ∈ asIdeal f_deg hm q
⊢ 1 = Localization.mk (↑(((decompose 𝒜) f) m) ^ m) ⟨f ^ m, ⋯⟩

Proof state:
case h.e'_5
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
q : ↑↑(Spec A⁰_ f).toPresheafedSpace
rid : f ∈ asIdeal f_deg hm q
⊢ 1 = Localization.mk (↑(((decompose 𝒜) f) m) ^ m) ⟨f ^ m, ⋯⟩

Tactic:
simp_rw [decompose_of_mem_same _ f_deg]

Result:
case h.e'_5
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
q : ↑↑(Spec A⁰_ f).toPresheafedSpace
rid : f ∈ asIdeal f_deg hm q
⊢ 1 = Localization.mk (f ^ m) ⟨f ^ m, ⋯⟩