-- Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Scheme.lean
/--
If `x` is a point in the basic open set `D(f)` where `f` is a homogeneous element of positive
degree, then the homogeneously localized ring `A⁰ₓ` has the universal property of the localization
of `A⁰_f` at `φ(x)` where `φ : Proj|D(f) ⟶ Spec A⁰_f` is the morphism of locally ringed space
constructed as above.
-/
lemma isLocalization_atPrime (f) (x : pbo f) {m} (f_deg : f ∈ 𝒜 m) (hm : 0 < m) :
    @IsLocalization (Away 𝒜 f) _ ((toSpec 𝒜 f).base x).asIdeal.primeCompl
      (AtPrime 𝒜 x.1.asHomogeneousIdeal.toIdeal) _
      (mapId 𝒜 (Submonoid.powers_le.mpr x.2)).toAlgebra

Proof state:
case intro.mk.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
x : ↥(pbo f)
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
this : Algebra (A⁰_ f) (AtPrime 𝒜 (↑x).asHomogeneousIdeal.toIdeal) := (mapId 𝒜 ⋯).toAlgebra
y z : NumDenSameDeg 𝒜 (Submonoid.powers f)
e :
  (algebraMap A (Localization (↑x).asHomogeneousIdeal.toIdeal.primeCompl)) (↑z.den * ↑y.num) =
    (algebraMap A (Localization (↑x).asHomogeneousIdeal.toIdeal.primeCompl)) (↑y.den * ↑z.num)
c : A
hcx : c ∈ (↑x).asHomogeneousIdeal.toIdeal.primeCompl
i : ℕ
hi : ↑(((decompose 𝒜) c) i) ∉ (↑x).asHomogeneousIdeal.toIdeal
hc :
  ↑(((decompose 𝒜) (↑⟨c, hcx⟩ * (↑z.den * ↑y.num))) (i + z.deg + y.deg)) =
    ↑(((decompose 𝒜) (↑⟨c, hcx⟩ * (↑y.den * ↑z.num))) (i + y.deg + z.deg))
⊢ ↑(((decompose 𝒜) c) i) * (↑z.den * ↑y.num) = ↑(((decompose 𝒜) c) i) * (↑y.den * ↑z.num)

Tactic:
rwa [← mul_assoc, coe_decompose_mul_add_of_right_mem, coe_decompose_mul_add_of_right_mem,
  ← mul_assoc, coe_decompose_mul_add_of_right_mem, coe_decompose_mul_add_of_right_mem,
  mul_assoc, mul_assoc] at hc

Result:
case intro.mk.intro.b_mem
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
x : ↥(pbo f)
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
this : Algebra (A⁰_ f) (AtPrime 𝒜 (↑x).asHomogeneousIdeal.toIdeal) := (mapId 𝒜 ⋯).toAlgebra
y z : NumDenSameDeg 𝒜 (Submonoid.powers f)
e :
  (algebraMap A (Localization (↑x).asHomogeneousIdeal.toIdeal.primeCompl)) (↑z.den * ↑y.num) =
    (algebraMap A (Localization (↑x).asHomogeneousIdeal.toIdeal.primeCompl)) (↑y.den * ↑z.num)
c : A
hcx : c ∈ (↑x).asHomogeneousIdeal.toIdeal.primeCompl
i : ℕ
hi : ↑(((decompose 𝒜) c) i) ∉ (↑x).asHomogeneousIdeal.toIdeal
hc : ↑(((decompose 𝒜) ↑⟨c, hcx⟩) i) * ↑z.den * ↑y.num = ↑(((decompose 𝒜) (↑⟨c, hcx⟩ * ↑y.den)) (i + y.deg)) * ↑z.num
⊢ ↑y.den ∈ 𝒜 y.deg

case intro.mk.intro.b_mem
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
x : ↥(pbo f)
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
this : Algebra (A⁰_ f) (AtPrime 𝒜 (↑x).asHomogeneousIdeal.toIdeal) := (mapId 𝒜 ⋯).toAlgebra
y z : NumDenSameDeg 𝒜 (Submonoid.powers f)
e :
  (algebraMap A (Localization (↑x).asHomogeneousIdeal.toIdeal.primeCompl)) (↑z.den * ↑y.num) =
    (algebraMap A (Localization (↑x).asHomogeneousIdeal.toIdeal.primeCompl)) (↑y.den * ↑z.num)
c : A
hcx : c ∈ (↑x).asHomogeneousIdeal.toIdeal.primeCompl
i : ℕ
hi : ↑(((decompose 𝒜) c) i) ∉ (↑x).asHomogeneousIdeal.toIdeal
hc :
  ↑(((decompose 𝒜) ↑⟨c, hcx⟩) i) * ↑z.den * ↑y.num =
    ↑(((decompose 𝒜) (↑⟨c, hcx⟩ * ↑y.den * ↑z.num)) (i + y.deg + z.deg))
⊢ ↑z.num ∈ 𝒜 z.deg

case intro.mk.intro.b_mem
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
x : ↥(pbo f)
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
this : Algebra (A⁰_ f) (AtPrime 𝒜 (↑x).asHomogeneousIdeal.toIdeal) := (mapId 𝒜 ⋯).toAlgebra
y z : NumDenSameDeg 𝒜 (Submonoid.powers f)
e :
  (algebraMap A (Localization (↑x).asHomogeneousIdeal.toIdeal.primeCompl)) (↑z.den * ↑y.num) =
    (algebraMap A (Localization (↑x).asHomogeneousIdeal.toIdeal.primeCompl)) (↑y.den * ↑z.num)
c : A
hcx : c ∈ (↑x).asHomogeneousIdeal.toIdeal.primeCompl
i : ℕ
hi : ↑(((decompose 𝒜) c) i) ∉ (↑x).asHomogeneousIdeal.toIdeal
hc :
  ↑(((decompose 𝒜) (↑⟨c, hcx⟩ * ↑z.den)) (i + z.deg)) * ↑y.num =
    ↑(((decompose 𝒜) (↑⟨c, hcx⟩ * (↑y.den * ↑z.num))) (i + y.deg + z.deg))
⊢ ↑z.den ∈ 𝒜 z.deg

case intro.mk.intro.b_mem
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
x : ↥(pbo f)
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
this : Algebra (A⁰_ f) (AtPrime 𝒜 (↑x).asHomogeneousIdeal.toIdeal) := (mapId 𝒜 ⋯).toAlgebra
y z : NumDenSameDeg 𝒜 (Submonoid.powers f)
e :
  (algebraMap A (Localization (↑x).asHomogeneousIdeal.toIdeal.primeCompl)) (↑z.den * ↑y.num) =
    (algebraMap A (Localization (↑x).asHomogeneousIdeal.toIdeal.primeCompl)) (↑y.den * ↑z.num)
c : A
hcx : c ∈ (↑x).asHomogeneousIdeal.toIdeal.primeCompl
i : ℕ
hi : ↑(((decompose 𝒜) c) i) ∉ (↑x).asHomogeneousIdeal.toIdeal
hc :
  ↑(((decompose 𝒜) (↑⟨c, hcx⟩ * ↑z.den * ↑y.num)) (i + z.deg + y.deg)) =
    ↑(((decompose 𝒜) (↑⟨c, hcx⟩ * (↑y.den * ↑z.num))) (i + y.deg + z.deg))
⊢ ↑y.num ∈ 𝒜 y.deg

Proof state:
case map_units'.mk.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
x : ↥(pbo f)
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
this : Algebra (A⁰_ f) (AtPrime 𝒜 (↑x).asHomogeneousIdeal.toIdeal) := (mapId 𝒜 ⋯).toAlgebra
y : NumDenSameDeg 𝒜 (Submonoid.powers f)
hy : HomogeneousLocalization.mk y ∈ ((ConcreteCategory.hom (toSpec 𝒜 f).base) x).asIdeal.primeCompl
⊢ IsUnit ((algebraMap (A⁰_ f) (AtPrime 𝒜 (↑x).asHomogeneousIdeal.toIdeal)) ↑⟨HomogeneousLocalization.mk y, hy⟩)

Tactic:
refine isUnit_of_mul_eq_one _
  (.mk ⟨y.deg, y.den, y.num, (mk_mem_toSpec_base_apply _ _ _).not.mp hy⟩) <| val_injective _ ?_

Result:
case map_units'.mk.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
x : ↥(pbo f)
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
this : Algebra (A⁰_ f) (AtPrime 𝒜 (↑x).asHomogeneousIdeal.toIdeal) := (mapId 𝒜 ⋯).toAlgebra
y : NumDenSameDeg 𝒜 (Submonoid.powers f)
hy : HomogeneousLocalization.mk y ∈ ((ConcreteCategory.hom (toSpec 𝒜 f).base) x).asIdeal.primeCompl
⊢ HomogeneousLocalization.val
      ((algebraMap (A⁰_ f) (AtPrime 𝒜 (↑x).asHomogeneousIdeal.toIdeal)) ↑⟨HomogeneousLocalization.mk y, hy⟩ *
        HomogeneousLocalization.mk { deg := y.deg, num := y.den, den := y.num, den_mem := ⋯ }) =
    HomogeneousLocalization.val 1