-- 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
m : ℕ
f_deg : f ∈ 𝒜 m
hm : 0 < m
q : (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1)
x : A
hx : x ∈ carrier f_deg q
n : ℕ
a : A
ha : a ∈ 𝒜 n
i : ℕ
product : A⁰_ f :=
  HMul.hMul (α := HomogeneousLocalization 𝒜 (Submonoid.powers f))
    (HomogeneousLocalization.mk
      { deg := m • n, num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m • n)) (a ^ m) ⋯,
        den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m • n)) (f ^ n) ⋯, den_mem := ⋯ })
    (HomogeneousLocalization.mk
      { deg := m • (i - n),
        num :=
          Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m • (i - n)))
            (HPow.hPow (α := A) ((proj 𝒜 (i - n) : (a : A) → A) x : A) m) ⋯,
        den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m • (i - n))) (f ^ (i - n)) ⋯, den_mem := ⋯ })
h : n ≤ i
h₁ :
  Localization.mk
      (↑(NumDenSameDeg.num
            { deg := m * i,
              num :=
                Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i))
                  ((a *
                      (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ℕ), ↥(𝒜 i)) x : ⨁ (i : ℕ), ↥(𝒜 i)) : (a : ℕ) → ↥(𝒜 a))
                            (i - n)) :
                        A)) ^
                    m)
                  ⋯,
              den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i)) (f ^ i) ⋯, den_mem := ⋯ }) :
        A)
      (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers f) x)
        (↑(NumDenSameDeg.den
              { deg := m * i,
                num :=
                  Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i))
                    ((a *
                        (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ℕ), ↥(𝒜 i)) x : ⨁ (i : ℕ), ↥(𝒜 i)) : (a : ℕ) → ↥(𝒜 a))
                              (i - n)) :
                          A)) ^
                      m)
                    ⋯,
                den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i)) (f ^ i) ⋯, den_mem := ⋯ }) :
          A)
        ⋯) =
    HMul.hMul (α := Localization (Submonoid.powers f))
      (Localization.mk
        (↑(NumDenSameDeg.num
              { deg := m * n, num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * n)) (a ^ m) ⋯,
                den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * n)) (f ^ n) ⋯, den_mem := ⋯ :
                NumDenSameDeg 𝒜 (Submonoid.powers f) }) :
          A)
        (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers f) x)
          (↑(NumDenSameDeg.den
                { deg := m * n, num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * n)) (a ^ m) ⋯,
                  den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * n)) (f ^ n) ⋯, den_mem := ⋯ :
                  NumDenSameDeg 𝒜 (Submonoid.powers f) }) :
            A)
          ⋯))
      (Localization.mk
        (↑(NumDenSameDeg.num
              { deg := m * (i - n),
                num :=
                  Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * (i - n)))
                    ((↑((((decompose 𝒜 : (a : A) → ⨁ (i : ℕ), ↥(𝒜 i)) x : ⨁ (i : ℕ), ↥(𝒜 i)) : (a : ℕ) → ↥(𝒜 a))
                            (i - n)) :
                        A) ^
                      m)
                    ⋯,
                den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * (i - n))) (f ^ (i - n)) ⋯, den_mem := ⋯ :
                NumDenSameDeg 𝒜 (Submonoid.powers f) }) :
          A)
        (Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers f) x)
          (↑(NumDenSameDeg.den
                { deg := m * (i - n),
                  num :=
                    Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * (i - n)))
                      ((↑((((decompose 𝒜 : (a : A) → ⨁ (i : ℕ), ↥(𝒜 i)) x : ⨁ (i : ℕ), ↥(𝒜 i)) : (a : ℕ) → ↥(𝒜 a))
                              (i - n)) :
                          A) ^
                        m)
                      ⋯,
                  den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * (i - n))) (f ^ (i - n)) ⋯, den_mem := ⋯ :
                  NumDenSameDeg 𝒜 (Submonoid.powers f) }) :
            A)
          ⋯))
⊢ HomogeneousLocalization.mk
      { deg := m * i,
        num :=
          Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i))
            ((a *
                (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ℕ), ↥(𝒜 i)) x : ⨁ (i : ℕ), ↥(𝒜 i)) : (a : ℕ) → ↥(𝒜 a)) (i - n)) :
                  A)) ^
              m)
            ⋯,
        den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i)) (f ^ i) ⋯, den_mem := ⋯ } =
    HMul.hMul (α := HomogeneousLocalization 𝒜 (Submonoid.powers f))
      (HomogeneousLocalization.mk
        { deg := m * n, num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * n)) (a ^ m) ⋯,
          den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * n)) (f ^ n) ⋯, den_mem := ⋯ :
          NumDenSameDeg 𝒜 (Submonoid.powers f) })
      (HomogeneousLocalization.mk
        { deg := m * (i - n),
          num :=
            Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * (i - n)))
              ((↑((((decompose 𝒜 : (a : A) → ⨁ (i : ℕ), ↥(𝒜 i)) x : ⨁ (i : ℕ), ↥(𝒜 i)) : (a : ℕ) → ↥(𝒜 a)) (i - n)) :
                  A) ^
                m)
              ⋯,
          den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * (i - n))) (f ^ (i - n)) ⋯, den_mem := ⋯ :
          NumDenSameDeg 𝒜 (Submonoid.powers f) })

Tactic:
rw [HomogeneousLocalization.ext_iff_val, HomogeneousLocalization.val_mk,
            HomogeneousLocalization.val_mul, HomogeneousLocalization.val_mk,
            HomogeneousLocalization.val_mk]

Premises used: HomogeneousLocalization.val_mk, HomogeneousLocalization.ext_iff_val, HomogeneousLocalization.val_mul