-- 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 x_1 : A⁰_ f
x_2 : ↥(unop (op (pbo f)))
⊢ HomogeneousLocalization.val.{0, u_1, u_2} (ι := ℕ) (σ := σ) (𝒜 := 𝒜)
      ((↑(Subtype.mk (p :=
              fun
                (f_1 :
                  (x : ↥(unop (op (pbo f)))) →
                    (fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦
                        HomogeneousLocalization.AtPrime 𝒜 x.asHomogeneousIdeal.toIdeal)
                      (↑x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))) ↦
              PrelocalPredicate.pred (X := ProjectiveSpectrum.top 𝒜) (T :=
                fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦
                HomogeneousLocalization.AtPrime 𝒜 x.asHomogeneousIdeal.toIdeal)
                (LocalPredicate.toPrelocalPredicate (T := fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦
                    HomogeneousLocalization.AtPrime 𝒜 x.asHomogeneousIdeal.toIdeal) (isLocallyFraction 𝒜) :
                  PrelocalPredicate (X := ProjectiveSpectrum.top 𝒜) fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦
                    HomogeneousLocalization.AtPrime 𝒜 x.asHomogeneousIdeal.toIdeal)
                f_1)
              (fun (x_3 : ↥(unop (op (pbo f)))) ↦
                (HomogeneousLocalization.mapId 𝒜 ⋯ :
                    (a : HomogeneousLocalization 𝒜 (Submonoid.powers f)) →
                      HomogeneousLocalization 𝒜
                        (↑x_3 : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)).asHomogeneousIdeal.toIdeal.primeCompl)
                  (x * x_1))
              ⋯) :
          (x : ↥(unop (op (pbo f)))) →
            (fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦
                HomogeneousLocalization.AtPrime 𝒜 x.asHomogeneousIdeal.toIdeal)
              (↑x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)))
        x_2) =
    HomogeneousLocalization.val
      ((↑(HMul.hMul (α :=
              (↑(Functor.obj (C := (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ)
                    (ObjectProperty.FullSubcategory.obj (P :=
                        (CategoryTheory.Presheaf.IsSheaf
                            (Opens.grothendieckTopology (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) :
                          (P : (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ ⥤ CommRingCat) → Prop))
                        (structureSheaf 𝒜 : TopCat.Sheaf CommRingCat (ProjectiveSpectrum.top 𝒜)) :
                      (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ ⥤ CommRingCat)
                    (op (pbo f) : (Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))ᵒᵖ)) :
                Type u_1))
              (Subtype.mk (p :=
                fun
                  (f_1 :
                    (x : ↥(unop (op (pbo f)))) →
                      (fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦
                          HomogeneousLocalization.AtPrime 𝒜 x.asHomogeneousIdeal.toIdeal)
                        (↑x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))) ↦
                PrelocalPredicate.pred (X := ProjectiveSpectrum.top 𝒜) (T :=
                  fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦
                  HomogeneousLocalization.AtPrime 𝒜 x.asHomogeneousIdeal.toIdeal)
                  (LocalPredicate.toPrelocalPredicate (T := fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦
                      HomogeneousLocalization.AtPrime 𝒜 x.asHomogeneousIdeal.toIdeal) (isLocallyFraction 𝒜) :
                    PrelocalPredicate (X := ProjectiveSpectrum.top 𝒜)
                      fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦
                      HomogeneousLocalization.AtPrime 𝒜 x.asHomogeneousIdeal.toIdeal)
                  f_1)
                (fun (x_3 : ↥(unop (op (pbo f)))) ↦
                  (HomogeneousLocalization.mapId 𝒜 ⋯ :
                      (a : HomogeneousLocalization 𝒜 (Submonoid.powers f)) →
                        HomogeneousLocalization 𝒜
                          (↑x_3 : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)).asHomogeneousIdeal.toIdeal.primeCompl)
                    x)
                ⋯)
              (Subtype.mk (p :=
                fun
                  (f_1 :
                    (x : ↥(unop (op (pbo f)))) →
                      (fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦
                          HomogeneousLocalization.AtPrime 𝒜 x.asHomogeneousIdeal.toIdeal)
                        (↑x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1))) ↦
                PrelocalPredicate.pred (X := ProjectiveSpectrum.top 𝒜) (T :=
                  fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦
                  HomogeneousLocalization.AtPrime 𝒜 x.asHomogeneousIdeal.toIdeal)
                  (LocalPredicate.toPrelocalPredicate (T := fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦
                      HomogeneousLocalization.AtPrime 𝒜 x.asHomogeneousIdeal.toIdeal) (isLocallyFraction 𝒜) :
                    PrelocalPredicate (X := ProjectiveSpectrum.top 𝒜)
                      fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦
                      HomogeneousLocalization.AtPrime 𝒜 x.asHomogeneousIdeal.toIdeal)
                  f_1)
                (fun (x : ↥(unop (op (pbo f)))) ↦
                  (HomogeneousLocalization.mapId 𝒜 ⋯ :
                      (a : HomogeneousLocalization 𝒜 (Submonoid.powers f)) →
                        HomogeneousLocalization 𝒜
                          (↑x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)).asHomogeneousIdeal.toIdeal.primeCompl)
                    x_1)
                ⋯)) :
          (x : ↥(unop (op (pbo f)))) →
            (fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)) ↦
                HomogeneousLocalization.AtPrime 𝒜 x.asHomogeneousIdeal.toIdeal)
              (↑x : (↑(ProjectiveSpectrum.top 𝒜) : Type u_1)))
        x_2)

Tactic:
simp only [map_mul, HomogeneousLocalization.val_mul, Proj.mul_apply]

Premises used: AlgebraicGeometry.Proj.mul_apply, HomogeneousLocalization.val_mul, map_mul