-- 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
q : (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1)
a b : A
ha : a ∈ carrier f_deg q
hb : b ∈ carrier f_deg q
i : ℕ
change :
  HomogeneousLocalization.mk
      {
        deg :=
          NumDenSameDeg.deg (x := Submonoid.powers f)
              { deg := m * i,
                num :=
                  Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i))
                    (HPow.hPow (α := A) ((proj 𝒜 i : (a : A) → A) (a + b) : A) m) ⋯,
                den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i)) (f ^ i) ⋯, den_mem := ⋯ :
                NumDenSameDeg 𝒜 (Submonoid.powers f) } +
            NumDenSameDeg.deg (x := Submonoid.powers f)
              { deg := m * i,
                num :=
                  Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i))
                    (HPow.hPow (α := A) ((proj 𝒜 i : (a : A) → A) (a + b) : A) m) ⋯,
                den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i)) (f ^ i) ⋯, den_mem := ⋯ :
                NumDenSameDeg 𝒜 (Submonoid.powers f) },
        num :=
          Subtype.mk (p := fun (x : A) ↦
            x ∈
              𝒜
                (NumDenSameDeg.deg (x := Submonoid.powers f)
                    { deg := m * i,
                      num :=
                        Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i))
                          (HPow.hPow (α := A) ((proj 𝒜 i : (a : A) → A) (a + b) : A) m) ⋯,
                      den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i)) (f ^ i) ⋯, den_mem := ⋯ :
                      NumDenSameDeg 𝒜 (Submonoid.powers f) } +
                  NumDenSameDeg.deg (x := Submonoid.powers f)
                    { deg := m * i,
                      num :=
                        Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i))
                          (HPow.hPow (α := A) ((proj 𝒜 i : (a : A) → A) (a + b) : A) m) ⋯,
                      den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i)) (f ^ i) ⋯, den_mem := ⋯ :
                      NumDenSameDeg 𝒜 (Submonoid.powers f) }))
            ((↑(NumDenSameDeg.num
                    { deg := m * i,
                      num :=
                        Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i))
                          (HPow.hPow (α := A) ((proj 𝒜 i : (a : A) → A) (a + b) : A) m) ⋯,
                      den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i)) (f ^ i) ⋯, den_mem := ⋯ :
                      NumDenSameDeg 𝒜 (Submonoid.powers f) }) :
                A) *
              (↑(NumDenSameDeg.num
                    { deg := m * i,
                      num :=
                        Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i))
                          (HPow.hPow (α := A) ((proj 𝒜 i : (a : A) → A) (a + b) : A) m) ⋯,
                      den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i)) (f ^ i) ⋯, den_mem := ⋯ :
                      NumDenSameDeg 𝒜 (Submonoid.powers f) }) :
                A))
            ⋯,
        den :=
          Subtype.mk (p := fun (x : A) ↦
            x ∈
              𝒜
                (NumDenSameDeg.deg (x := Submonoid.powers f)
                    { deg := m * i,
                      num :=
                        Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i))
                          (HPow.hPow (α := A) ((proj 𝒜 i : (a : A) → A) (a + b) : A) m) ⋯,
                      den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i)) (f ^ i) ⋯, den_mem := ⋯ :
                      NumDenSameDeg 𝒜 (Submonoid.powers f) } +
                  NumDenSameDeg.deg (x := Submonoid.powers f)
                    { deg := m * i,
                      num :=
                        Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i))
                          (HPow.hPow (α := A) ((proj 𝒜 i : (a : A) → A) (a + b) : A) m) ⋯,
                      den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i)) (f ^ i) ⋯, den_mem := ⋯ :
                      NumDenSameDeg 𝒜 (Submonoid.powers f) }))
            ((↑(NumDenSameDeg.den
                    { deg := m * i,
                      num :=
                        Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i))
                          (HPow.hPow (α := A) ((proj 𝒜 i : (a : A) → A) (a + b) : A) m) ⋯,
                      den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i)) (f ^ i) ⋯, den_mem := ⋯ :
                      NumDenSameDeg 𝒜 (Submonoid.powers f) }) :
                A) *
              (↑(NumDenSameDeg.den
                    { deg := m * i,
                      num :=
                        Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i))
                          (HPow.hPow (α := A) ((proj 𝒜 i : (a : A) → A) (a + b) : A) m) ⋯,
                      den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i)) (f ^ i) ⋯, den_mem := ⋯ :
                      NumDenSameDeg 𝒜 (Submonoid.powers f) }) :
                A))
            ⋯,
        den_mem := ⋯ } ∈
    q.asIdeal
⊢ HMul.hMul (α := (↑(CommRingCat.of (A⁰_ f)) : Type u_1))
      (HomogeneousLocalization.mk
        { deg := m * i,
          num :=
            Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i)) (HPow.hPow (α := A) ((proj 𝒜 i : (a : A) → A) (a + b) : A) m)
              ⋯,
          den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i)) (f ^ i) ⋯, den_mem := ⋯ :
          NumDenSameDeg 𝒜 (Submonoid.powers f) })
      (HomogeneousLocalization.mk
        { deg := m * i,
          num :=
            Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i)) (HPow.hPow (α := A) ((proj 𝒜 i : (a : A) → A) (a + b) : A) m)
              ⋯,
          den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i)) (f ^ i) ⋯, den_mem := ⋯ :
          NumDenSameDeg 𝒜 (Submonoid.powers f) }) ∈
    q.asIdeal

Tactic:
change (HomogeneousLocalization.mk ⟨_, _, _, _⟩ : A⁰_ f) ∈ q.1

Premises used: HomogeneousLocalization.NumDenSameDeg.mk, HomogeneousLocalization.mk, PrimeSpectrum.asIdeal