-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme (goal)
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 : ℕ
⊢ 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
have 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) sorry,
              den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i)) (f ^ i) sorry, den_mem := sorry :
              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) sorry,
              den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i)) (f ^ i) sorry, den_mem := sorry :
              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) sorry,
                    den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i)) (f ^ i) sorry, den_mem := sorry :
                    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) sorry,
                    den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i)) (f ^ i) sorry, den_mem := sorry :
                    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) sorry,
                    den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i)) (f ^ i) sorry, den_mem := sorry :
                    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) sorry,
                    den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i)) (f ^ i) sorry, den_mem := sorry :
                    NumDenSameDeg 𝒜 (Submonoid.powers f) }) :
              A))
          sorry,
      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) sorry,
                    den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i)) (f ^ i) sorry, den_mem := sorry :
                    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) sorry,
                    den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i)) (f ^ i) sorry, den_mem := sorry :
                    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) sorry,
                    den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i)) (f ^ i) sorry, den_mem := sorry :
                    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) sorry,
                    den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i)) (f ^ i) sorry, den_mem := sorry :
                    NumDenSameDeg 𝒜 (Submonoid.powers f) }) :
              A))
          sorry,
      den_mem := sorry } ∈
  q.asIdeal
Tactic: change (HomogeneousLocalization.mk ⟨_, _, _, _⟩ : A⁰_ f) ∈ q.1