-- Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Scheme.lean
lemma awayToSection_apply (f : A) (x p) :
    (((ProjectiveSpectrum.Proj.awayToSection 𝒜 f).1 x).val p).val =
      IsLocalization.map (M := Submonoid.powers f) (T := p.1.1.toIdeal.primeCompl) _
        (RingHom.id _) (Submonoid.powers_le.mpr p.2) x.val

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
x : ↑(CommRingCat.of (A⁰_ f))
p : ↥(unop (op (pbo f)))
⊢ HomogeneousLocalization.val (↑((awayToSection 𝒜 f).hom' x) p) =
    (IsLocalization.map (Localization (↑p).asHomogeneousIdeal.toIdeal.primeCompl) (RingHom.id A) ⋯)
      (HomogeneousLocalization.val x)

Tactic:
obtain ⟨x, rfl⟩ := HomogeneousLocalization.mk_surjective x

Result:
case 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
p : ↥(unop (op (pbo f)))
x : HomogeneousLocalization.NumDenSameDeg 𝒜 (Submonoid.powers f)
⊢ HomogeneousLocalization.val (↑((awayToSection 𝒜 f).hom' (HomogeneousLocalization.mk x)) p) =
    (IsLocalization.map (Localization (↑p).asHomogeneousIdeal.toIdeal.primeCompl) (RingHom.id A) ⋯)
      (HomogeneousLocalization.mk x).val

Proof state:
case 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
p : ↥(unop (op (pbo f)))
x : HomogeneousLocalization.NumDenSameDeg 𝒜 (Submonoid.powers f)
⊢ IsLocalization.mk' (Localization (↑p).asHomogeneousIdeal.toIdeal.primeCompl) ↑x.num ⟨↑x.den, ⋯⟩ =
    IsLocalization.mk' (Localization (↑p).asHomogeneousIdeal.toIdeal.primeCompl) ((RingHom.id A) ↑x.num)
      ⟨(RingHom.id A) ↑⟨↑x.den, ⋯⟩, ⋯⟩

Tactic:
rfl

Result:
no goals

Proof state:
case 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
p : ↥(unop (op (pbo f)))
x : HomogeneousLocalization.NumDenSameDeg 𝒜 (Submonoid.powers f)
⊢ HomogeneousLocalization.val (↑((awayToSection 𝒜 f).hom' (HomogeneousLocalization.mk x)) p) =
    (IsLocalization.map (Localization (↑p).asHomogeneousIdeal.toIdeal.primeCompl) (RingHom.id A) ⋯)
      (HomogeneousLocalization.mk x).val

Tactic:
show (HomogeneousLocalization.mapId 𝒜 _ _).val = _

Result:
case 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
p : ↥(unop (op (pbo f)))
x : HomogeneousLocalization.NumDenSameDeg 𝒜 (Submonoid.powers f)
⊢ ((HomogeneousLocalization.mapId 𝒜 ⋯) (HomogeneousLocalization.mk x)).val =
    (IsLocalization.map (Localization (↑p).asHomogeneousIdeal.toIdeal.primeCompl) (RingHom.id A) ⋯)
      (HomogeneousLocalization.mk x).val

Proof state:
case 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
p : ↥(unop (op (pbo f)))
x : HomogeneousLocalization.NumDenSameDeg 𝒜 (Submonoid.powers f)
⊢ Localization.mk ↑x.num ⟨↑x.den, ⋯⟩ =
    (IsLocalization.map (Localization (↑p).asHomogeneousIdeal.toIdeal.primeCompl) (RingHom.id A) ⋯)
      (Localization.mk ↑x.num ⟨↑x.den, ⋯⟩)

Tactic:
rw [Localization.mk_eq_mk', Localization.mk_eq_mk', IsLocalization.map_mk']

Result:
case 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
p : ↥(unop (op (pbo f)))
x : HomogeneousLocalization.NumDenSameDeg 𝒜 (Submonoid.powers f)
⊢ IsLocalization.mk' (Localization (↑p).asHomogeneousIdeal.toIdeal.primeCompl) ↑x.num ⟨↑x.den, ⋯⟩ =
    IsLocalization.mk' (Localization (↑p).asHomogeneousIdeal.toIdeal.primeCompl) ((RingHom.id A) ↑x.num)
      ⟨(RingHom.id A) ↑⟨↑x.den, ⋯⟩, ⋯⟩

Proof state:
case 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
p : ↥(unop (op (pbo f)))
x : HomogeneousLocalization.NumDenSameDeg 𝒜 (Submonoid.powers f)
⊢ ((HomogeneousLocalization.mapId 𝒜 ⋯) (HomogeneousLocalization.mk x)).val =
    (IsLocalization.map (Localization (↑p).asHomogeneousIdeal.toIdeal.primeCompl) (RingHom.id A) ⋯)
      (HomogeneousLocalization.mk x).val

Tactic:
dsimp [HomogeneousLocalization.mapId, HomogeneousLocalization.map]

Result:
case 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
p : ↥(unop (op (pbo f)))
x : HomogeneousLocalization.NumDenSameDeg 𝒜 (Submonoid.powers f)
⊢ Localization.mk ↑x.num ⟨↑x.den, ⋯⟩ =
    (IsLocalization.map (Localization (↑p).asHomogeneousIdeal.toIdeal.primeCompl) (RingHom.id A) ⋯)
      (Localization.mk ↑x.num ⟨↑x.den, ⋯⟩)