-- 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
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
a : ↑(CommRingCat.of (Away 𝒜 f))
⊢ ↑((CommRingCat.Hom.hom (CommRingCat.ofHom (awayMap 𝒜 g_deg hx) ≫ awayToSection 𝒜 x)) a) =
    ↑((CommRingCat.Hom.hom (awayToSection 𝒜 f ≫ (Proj 𝒜).presheaf.map (homOfLE ⋯).op)) a)

Tactic:
ext ⟨i, hi⟩

Result:
case hf.a.a.h.mk.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
m' : ℕ
g : A
g_deg : g ∈ 𝒜 m'
x : A
hx : x = f * g
a : ↑(CommRingCat.of (Away 𝒜 f))
i : ↑(ProjectiveSpectrum.top 𝒜)
hi : i ∈ Opposite.unop (Opposite.op (basicOpen 𝒜 x))
⊢ val (↑((CommRingCat.Hom.hom (CommRingCat.ofHom (awayMap 𝒜 g_deg hx) ≫ awayToSection 𝒜 x)) a) ⟨i, hi⟩) =
    val (↑((CommRingCat.Hom.hom (awayToSection 𝒜 f ≫ (Proj 𝒜).presheaf.map (homOfLE ⋯).op)) a) ⟨i, hi⟩)

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' : ℕ
g : A
g_deg : g ∈ 𝒜 m'
x : A
hx : x = f * g
⊢ CommRingCat.ofHom (awayMap 𝒜 g_deg hx) ≫ awayToSection 𝒜 x = awayToSection 𝒜 f ≫ (Proj 𝒜).presheaf.map (homOfLE ⋯).op

Tactic:
ext a

Result:
case hf.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
m' : ℕ
g : A
g_deg : g ∈ 𝒜 m'
x : A
hx : x = f * g
a : ↑(CommRingCat.of (Away 𝒜 f))
⊢ (CommRingCat.Hom.hom (CommRingCat.ofHom (awayMap 𝒜 g_deg hx) ≫ awayToSection 𝒜 x)) a =
    (CommRingCat.Hom.hom (awayToSection 𝒜 f ≫ (Proj 𝒜).presheaf.map (homOfLE ⋯).op)) a

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 (CommRingCat.ofHom (awayMap 𝒜 g_deg hx) ≫ awayToSection 𝒜 x))
            (mk { deg := n, num := a, den := ⟨(fun x => f ^ x) i, hb'⟩, den_mem := ⋯ }))
        ⟨i✝, hi⟩) =
    val
      (↑((CommRingCat.Hom.hom (awayToSection 𝒜 f ≫ (Proj 𝒜).presheaf.map (homOfLE ⋯).op))
            (mk { deg := n, num := a, den := ⟨(fun x => f ^ x) i, hb'⟩, den_mem := ⋯ }))
        ⟨i✝, hi⟩)

Tactic:
simp only [homOfLE_leOfHom, CommRingCat.hom_comp, RingHom.coe_comp, Function.comp_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
⊢ 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⟩)

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
⊢ (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⟩)

Tactic:
rw [CommRingCat.hom_ofHom, val_awayMap_mk, Localization.mk_eq_mk', IsLocalization.map_mk',
  ← Localization.mk_eq_mk']

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.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⟩)

Proof state:
case hf.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
m' : ℕ
g : A
g_deg : g ∈ 𝒜 m'
x : A
hx : x = f * g
a : ↑(CommRingCat.of (Away 𝒜 f))
⊢ (CommRingCat.Hom.hom (CommRingCat.ofHom (awayMap 𝒜 g_deg hx) ≫ awayToSection 𝒜 x)) a =
    (CommRingCat.Hom.hom (awayToSection 𝒜 f ≫ (Proj 𝒜).presheaf.map (homOfLE ⋯).op)) a

Tactic:
apply Subtype.ext

Result:
case hf.a.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
m' : ℕ
g : A
g_deg : g ∈ 𝒜 m'
x : A
hx : x = f * g
a : ↑(CommRingCat.of (Away 𝒜 f))
⊢ ↑((CommRingCat.Hom.hom (CommRingCat.ofHom (awayMap 𝒜 g_deg hx) ≫ awayToSection 𝒜 x)) a) =
    ↑((CommRingCat.Hom.hom (awayToSection 𝒜 f ≫ (Proj 𝒜).presheaf.map (homOfLE ⋯).op)) a)