-- Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Basic.lean
@[reassoc]
lemma awayMap_awayToSection  :
    CommRingCat.ofHom (awayMap 𝒜 g_deg hx) ≫ awayToSection 𝒜 x =
      awayToSection 𝒜 f ≫ (Proj 𝒜).presheaf.map (homOfLE (basicOpen_mono _ _ _ ⟨_, hx⟩)).op

Proof state:
case hf.a.a.h.mk.a.intro.mk.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
m' : ℕ
g : A
g_deg : g ∈ 𝒜 m'
x : A
hx : x = f * g
i✝ : ↑(ProjectiveSpectrum.top 𝒜)
hi : i✝ ∈ Opposite.unop (Opposite.op (basicOpen 𝒜 x))
n : ℕ
a : ↥(𝒜 n)
i : ℕ
hb' : (fun x => f ^ x) i ∈ 𝒜 n
⊢ val
      (↑((CommRingCat.Hom.hom (awayToSection 𝒜 x))
            ((CommRingCat.Hom.hom (CommRingCat.ofHom (awayMap 𝒜 g_deg hx)))
              (mk { deg := n, num := a, den := ⟨f ^ i, hb'⟩, den_mem := ⋯ })))
        ⟨i✝, hi⟩) =
    val
      (↑((CommRingCat.Hom.hom ((Proj 𝒜).presheaf.map (homOfLE ⋯).op))
            ((CommRingCat.Hom.hom (awayToSection 𝒜 f)) (mk { deg := n, num := a, den := ⟨f ^ i, hb'⟩, den_mem := ⋯ })))
        ⟨i✝, hi⟩)

Tactic:
erw [ProjectiveSpectrum.Proj.awayToSection_apply]

Result:
case hf.a.a.h.mk.a.intro.mk.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
m' : ℕ
g : A
g_deg : g ∈ 𝒜 m'
x : A
hx : x = f * g
i✝ : ↑(ProjectiveSpectrum.top 𝒜)
hi : i✝ ∈ Opposite.unop (Opposite.op (basicOpen 𝒜 x))
n : ℕ
a : ↥(𝒜 n)
i : ℕ
hb' : (fun x => f ^ x) i ∈ 𝒜 n
⊢ (IsLocalization.map (Localization (↑⟨i✝, hi⟩).asHomogeneousIdeal.toIdeal.primeCompl) (RingHom.id A) ⋯)
      (val
        ((CommRingCat.Hom.hom (CommRingCat.ofHom (awayMap 𝒜 g_deg hx)))
          (mk { deg := n, num := a, den := ⟨f ^ i, hb'⟩, den_mem := ⋯ }))) =
    val
      (↑((CommRingCat.Hom.hom ((Proj 𝒜).presheaf.map (homOfLE ⋯).op))
            ((CommRingCat.Hom.hom (awayToSection 𝒜 f)) (mk { deg := n, num := a, den := ⟨f ^ i, hb'⟩, den_mem := ⋯ })))
        ⟨i✝, hi⟩)

Proof state:
case hf.a.a.h.mk.a.intro.mk.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
m' : ℕ
g : A
g_deg : g ∈ 𝒜 m'
x : A
hx : x = f * g
i✝ : ↑(ProjectiveSpectrum.top 𝒜)
hi : i✝ ∈ Opposite.unop (Opposite.op (basicOpen 𝒜 x))
n : ℕ
a : ↥(𝒜 n)
i : ℕ
hb' : (fun x => f ^ x) i ∈ 𝒜 n
⊢ ∃ c,
    ↑c *
        (↑(↑((fun x_1 =>
                        { deg := x_1.deg, num := ⟨(RingHom.id A) ↑x_1.num, ⋯⟩, den := ⟨(RingHom.id A) ↑x_1.den, ⋯⟩,
                          den_mem := ⋯ })
                      { deg := n, num := a, den := ⟨f ^ i, hb'⟩, den_mem := ⋯ }).num,
                ⟨↑((fun x_1 =>
                          { deg := x_1.deg, num := ⟨(RingHom.id A) ↑x_1.num, ⋯⟩, den := ⟨(RingHom.id A) ↑x_1.den, ⋯⟩,
                            den_mem := ⋯ })
                        { deg := n, num := a, den := ⟨f ^ i, hb'⟩, den_mem := ⋯ }).den,
                  ⋯⟩).2 *
          ((RingHom.id A) (↑a * g ^ i), ⟨(RingHom.id A) ↑⟨x ^ i, ⋯⟩, ⋯⟩).1) =
      ↑c *
        (↑((RingHom.id A) (↑a * g ^ i), ⟨(RingHom.id A) ↑⟨x ^ i, ⋯⟩, ⋯⟩).2 *
          (↑((fun x_1 =>
                      { deg := x_1.deg, num := ⟨(RingHom.id A) ↑x_1.num, ⋯⟩, den := ⟨(RingHom.id A) ↑x_1.den, ⋯⟩,
                        den_mem := ⋯ })
                    { deg := n, num := a, den := ⟨f ^ i, hb'⟩, den_mem := ⋯ }).num,
              ⟨↑((fun x_1 =>
                        { deg := x_1.deg, num := ⟨(RingHom.id A) ↑x_1.num, ⋯⟩, den := ⟨(RingHom.id A) ↑x_1.den, ⋯⟩,
                          den_mem := ⋯ })
                      { deg := n, num := a, den := ⟨f ^ i, hb'⟩, den_mem := ⋯ }).den,
                ⋯⟩).1)

Tactic:
use 1

Result:
case h
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' : ℕ
g : A
g_deg : g ∈ 𝒜 m'
x : A
hx : x = f * g
i✝ : ↑(ProjectiveSpectrum.top 𝒜)
hi : i✝ ∈ Opposite.unop (Opposite.op (basicOpen 𝒜 x))
n : ℕ
a : ↥(𝒜 n)
i : ℕ
hb' : (fun x => f ^ x) i ∈ 𝒜 n
⊢ ↑1 *
      (↑(↑((fun x_1 =>
                      { deg := x_1.deg, num := ⟨(RingHom.id A) ↑x_1.num, ⋯⟩, den := ⟨(RingHom.id A) ↑x_1.den, ⋯⟩,
                        den_mem := ⋯ })
                    { deg := n, num := a, den := ⟨f ^ i, hb'⟩, den_mem := ⋯ }).num,
              ⟨↑((fun x_1 =>
                        { deg := x_1.deg, num := ⟨(RingHom.id A) ↑x_1.num, ⋯⟩, den := ⟨(RingHom.id A) ↑x_1.den, ⋯⟩,
                          den_mem := ⋯ })
                      { deg := n, num := a, den := ⟨f ^ i, hb'⟩, den_mem := ⋯ }).den,
                ⋯⟩).2 *
        ((RingHom.id A) (↑a * g ^ i), ⟨(RingHom.id A) ↑⟨x ^ i, ⋯⟩, ⋯⟩).1) =
    ↑1 *
      (↑((RingHom.id A) (↑a * g ^ i), ⟨(RingHom.id A) ↑⟨x ^ i, ⋯⟩, ⋯⟩).2 *
        (↑((fun x_1 =>
                    { deg := x_1.deg, num := ⟨(RingHom.id A) ↑x_1.num, ⋯⟩, den := ⟨(RingHom.id A) ↑x_1.den, ⋯⟩,
                      den_mem := ⋯ })
                  { deg := n, num := a, den := ⟨f ^ i, hb'⟩, den_mem := ⋯ }).num,
            ⟨↑((fun x_1 =>
                      { deg := x_1.deg, num := ⟨(RingHom.id A) ↑x_1.num, ⋯⟩, den := ⟨(RingHom.id A) ↑x_1.den, ⋯⟩,
                        den_mem := ⋯ })
                    { deg := n, num := a, den := ⟨f ^ i, hb'⟩, den_mem := ⋯ }).den,
              ⋯⟩).1)

Proof state:
case hf.a.a.h.mk.a.intro.mk.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
m' : ℕ
g : A
g_deg : g ∈ 𝒜 m'
x : A
hx : x = f * g
i✝ : ↑(ProjectiveSpectrum.top 𝒜)
hi : i✝ ∈ Opposite.unop (Opposite.op (basicOpen 𝒜 x))
n : ℕ
a : ↥(𝒜 n)
i : ℕ
hb' : (fun x => f ^ x) i ∈ 𝒜 n
⊢ Localization.mk ((RingHom.id A) (↑a * g ^ i)) ⟨(RingHom.id A) ↑⟨x ^ i, ⋯⟩, ⋯⟩ =
    val
      (↑((CommRingCat.Hom.hom ((Proj 𝒜).presheaf.map (homOfLE ⋯).op))
            ((CommRingCat.Hom.hom (awayToSection 𝒜 f)) (mk { deg := n, num := a, den := ⟨f ^ i, hb'⟩, den_mem := ⋯ })))
        ⟨i✝, hi⟩)

Tactic:
refine Localization.mk_eq_mk_iff.mpr ?_

Result:
case hf.a.a.h.mk.a.intro.mk.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
m' : ℕ
g : A
g_deg : g ∈ 𝒜 m'
x : A
hx : x = f * g
i✝ : ↑(ProjectiveSpectrum.top 𝒜)
hi : i✝ ∈ Opposite.unop (Opposite.op (basicOpen 𝒜 x))
n : ℕ
a : ↥(𝒜 n)
i : ℕ
hb' : (fun x => f ^ x) i ∈ 𝒜 n
⊢ (Localization.r (↑⟨i✝, hi⟩).asHomogeneousIdeal.toIdeal.primeCompl)
    ((RingHom.id A) (↑a * g ^ i), ⟨(RingHom.id A) ↑⟨x ^ i, ⋯⟩, ⋯⟩)
    (↑((fun x_1 =>
              { deg := x_1.deg, num := ⟨(RingHom.id A) ↑x_1.num, ⋯⟩, den := ⟨(RingHom.id A) ↑x_1.den, ⋯⟩,
                den_mem := ⋯ })
            { deg := n, num := a, den := ⟨f ^ i, hb'⟩, den_mem := ⋯ }).num,
      ⟨↑((fun x_1 =>
                { deg := x_1.deg, num := ⟨(RingHom.id A) ↑x_1.num, ⋯⟩, den := ⟨(RingHom.id A) ↑x_1.den, ⋯⟩,
                  den_mem := ⋯ })
              { deg := n, num := a, den := ⟨f ^ i, hb'⟩, den_mem := ⋯ }).den,
        ⋯⟩)