-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
Goal:
A : Type u_1
σ : Type u_2
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
f : A
x : ↥(pbo f)
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
this : Algebra (A⁰_ f) (AtPrime 𝒜 (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal) :=
  RingHom.toAlgebra (mapId 𝒜 ⋯)
i : ℕ
a : ↥(𝒜 i)
b : A
hb : b ∈ 𝒜 i
hb' : b ∉ (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal
toIsLocalizationMap :
  Eq (α := Localization (M := A) (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl)
    ((algebraMap A (Localization (M := A) (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl) :
          (a : A) → Localization (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl)
        (f ^ i * ((↑a : A) * b ^ m)) :
      Localization (M := A) (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl)
    ((algebraMap A (Localization (M := A) (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl) :
          (a : A) → Localization (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl)
        (f ^ i * b * ((↑a : A) * b ^ (m - 1))) :
      Localization (M := A) (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl)
toIsLocalizationMap₁ :
  Eq (α := Localization (M := A) (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl)
    ((algebraMap A (Localization (M := A) (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl) :
          (a : A) → Localization (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl)
        (f ^ i * ((↑a : A) * b ^ m)) :
      Localization (M := A) (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl)
    ((algebraMap A (Localization (M := A) (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl) :
          (a : A) → Localization (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl)
        (f ^ i * (↑a : A) * (b * b ^ (m - 1))) :
      Localization (M := A) (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl)
toIsLocalizationMap₂ :
  Eq (α := Localization (M := A) (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl)
    ((algebraMap A (Localization (M := A) (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl) :
          (a : A) → Localization (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl)
        (f ^ i * ((↑a : A) * b ^ m)) :
      Localization (M := A) (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl)
    ((algebraMap A (Localization (M := A) (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl) :
          (a : A) → Localization (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl)
        (f ^ i * (↑a : A) * b ^ (m - 1 + 1)) :
      Localization (M := A) (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl)
toIsLocalizationMap₃ :
  Eq (α := Localization (M := A) (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl)
    ((algebraMap A (Localization (M := A) (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl) :
          (a : A) → Localization (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl)
        (f ^ i * ((↑a : A) * b ^ m)) :
      Localization (M := A) (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl)
    ((algebraMap A (Localization (M := A) (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl) :
          (a : A) → Localization (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl)
        (f ^ i * ((↑a : A) * b ^ (m - 1 + 1))) :
      Localization (M := A) (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl)
toIsLocalizationMap₄ toIsLocalizationMap₅ :
  Eq (α := Localization (M := A) (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl)
    ((algebraMap A (Localization (M := A) (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl) :
          (a : A) → Localization (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl)
        (f ^ i * ((↑a : A) * b ^ m)) :
      Localization (M := A) (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl)
    ((algebraMap A (Localization (M := A) (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl) :
          (a : A) → Localization (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl)
        (f ^ i * ((↑a : A) * b ^ m)) :
      Localization (M := A) (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl)
⊢ Eq (α := Localization (M := A) (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl)
    ((algebraMap A (Localization (M := A) (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl) :
          (a : A) → Localization (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl)
        (f ^ i * ((↑a : A) * b ^ m)) :
      Localization (M := A) (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl)
    ((algebraMap A (Localization (M := A) (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl) :
          (a : A) → Localization (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl)
        (b * f ^ i * ((↑a : A) * b ^ (m - 1))) :
      Localization (M := A) (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl)

Tactic:
rw [mul_comm b, mul_mul_mul_comm, ← pow_succ', mul_assoc, tsub_add_cancel_of_le (by lia)]

Premises used: mul_mul_mul_comm, mul_assoc, tsub_add_cancel_of_le, mul_comm, pow_succ'