-- 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
hc : ↑⟨c, hcx⟩ * (↑z.den * ↑y.num) = ↑⟨c, hcx⟩ * (↑y.den * ↑z.num)
i : ℕ
hi : ↑(((decompose 𝒜) c) i) ∉ (↑x).asHomogeneousIdeal.toIdeal
⊢ ∃ i, ∃ c ∈ 𝒜 i, c ∉ (↑x).asHomogeneousIdeal ∧ c * (↑z.den * ↑y.num) = c * (↑y.den * ↑z.num)

Tactic:
refine ⟨i, _, (decompose 𝒜 c i).2, hi, ?_⟩

Result:
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
hc : ↑⟨c, hcx⟩ * (↑z.den * ↑y.num) = ↑⟨c, hcx⟩ * (↑y.den * ↑z.num)
i : ℕ
hi : ↑(((decompose 𝒜) c) i) ∉ (↑x).asHomogeneousIdeal.toIdeal
⊢ ↑(((decompose 𝒜) c) i) * (↑z.den * ↑y.num) = ↑(((decompose 𝒜) c) i) * (↑y.den * ↑z.num)

Proof state:
case exists_of_eq.intro.intro.intro.intro.intro.intro.h.e_6.h.e_a
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⁰_ f) (AtPrime 𝒜 (↑x).asHomogeneousIdeal.toIdeal)) (HomogeneousLocalization.mk y) =
    (algebraMap (A⁰_ f) (AtPrime 𝒜 (↑x).asHomogeneousIdeal.toIdeal)) (HomogeneousLocalization.mk z)
i : ℕ
c : A
hc : c ∈ 𝒜 i
hc' : c ∉ (↑x).asHomogeneousIdeal
e : c * (↑z.den * ↑y.num) = c * (↑y.den * ↑z.num)
⊢ ↑z.den * (c ^ m * ↑y.num) = ↑y.den * (c ^ m * ↑z.num)

Tactic:
rw [mul_left_comm, mul_left_comm y.den.1, ← tsub_add_cancel_of_le (show 1 ≤ m from hm),
  pow_succ, mul_assoc, mul_assoc, e]

Result:
no goals

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
⊢ 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

Tactic:
simp only [RingHom.algebraMap_toAlgebra, map_mk, RingHom.id_apply, val_mul, val_mk, mk_eq_mk',
  val_one, IsLocalization.mk'_mul_mk'_eq_one']

Result:
no goals