-- 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 𝒜 ⋯)
y : NumDenSameDeg 𝒜 (Submonoid.powers f)
hy :
  Membership.mem (γ := Submonoid (A⁰_ f))
    (Ideal.primeCompl
      (PrimeSpectrum.asIdeal
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1))) (CC := carrier)
              (X :=
              (↑(Proj.restrict (U := Functor.obj (C := Opens (↑Proj.T : Type u_1)) (Opens.toTopCat Proj.T) (pbo f))
                      ⋯).toPresheafedSpace :
                TopCat))
              (PresheafedSpace.Hom.base (LocallyRingedSpace.Hom.toHom (toSpec 𝒜 f))) :
            (a : (↑(↑(Proj.restrict ⋯).toPresheafedSpace : TopCat) : Type u_1)) →
              (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1))
          x)))
    (HomogeneousLocalization.mk y)
⊢ HomogeneousLocalization.val
      (HMul.hMul (α := AtPrime 𝒜 (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal) (β :=
        AtPrime 𝒜 (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal)
        ((algebraMap (A⁰_ f) (AtPrime 𝒜 (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal) :
              (a : A⁰_ f) → AtPrime 𝒜 (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal)
            (↑(Subtype.mk (p := fun (x_1 : A⁰_ f) ↦
                  Membership.mem (γ := Submonoid (A⁰_ f))
                    (Ideal.primeCompl
                      (PrimeSpectrum.asIdeal
                        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u_1}) ↦ C((↑X : Type u_1), (↑Y : Type u_1)))
                              (CC := carrier) (X :=
                              (↑(Proj.restrict (U :=
                                      Functor.obj (C := Opens (↑Proj.T : Type u_1)) (Opens.toTopCat Proj.T) (pbo f))
                                      ⋯).toPresheafedSpace :
                                TopCat))
                              (PresheafedSpace.Hom.base (LocallyRingedSpace.Hom.toHom (toSpec 𝒜 f))) :
                            (a : (↑(↑(Proj.restrict ⋯).toPresheafedSpace : TopCat) : Type u_1)) →
                              (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1))
                          x)))
                    x_1)
                  (HomogeneousLocalization.mk y) hy) :
              A⁰_ f) :
          AtPrime 𝒜 (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal)
        (HomogeneousLocalization.mk
          { deg := y.deg, num := y.den, den := y.num, den_mem := ⋯ :
            NumDenSameDeg 𝒜 (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toIdeal.primeCompl })) =
    HomogeneousLocalization.val.{0, u_1, u_2} (ι := ℕ) (σ := σ) (𝒜 := 𝒜) 1

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

Premises used: HomogeneousLocalization.map_mk, Localization.mk_eq_mk', GradedRingHom.id_apply, HomogeneousLocalization.val_one, HomogeneousLocalization.val_mk, HomogeneousLocalization.val_mul, IsLocalization.mk'_mul_mk'_eq_one', RingHom.algebraMap_toAlgebra