-- 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
hm : 0 < m
a : A
i : ℕ
⊢ Eq (α :=
    Set
      (↑(↑(Proj.restrict (U := Functor.obj (C := Opens (↑Proj.T : Type u_1)) (Opens.toTopCat Proj.T) (pbo f))
                  ⋯).toPresheafedSpace :
            TopCat) :
        Type u_1))
    (Subtype.val (p := fun (x : (↑Proj.T : Type u_1)) ↦ Membership.mem (γ := Opens (↑Proj.T : Type u_1)) (pbo f) x) ⁻¹'
      (↑(pbo (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ℕ), ↥(𝒜 i)) a : ⨁ (i : ℕ), ↥(𝒜 i)) : (a : ℕ) → ↥(𝒜 a)) i) : A)) :
        Set (ProjectiveSpectrum 𝒜)))
    (Set.preimage (β := (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1))
      (⇑(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))
            (toSpec 𝒜 f)) :
        (a : (↑(↑(Proj.restrict ⋯).toPresheafedSpace : TopCat) : Type u_1)) →
          (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1))
      (Opens.carrier
        (sbo
          HomogeneousLocalization.mk
            { deg := m * i,
              num :=
                Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i))
                  ((↑((((decompose 𝒜 : (a : A) → ⨁ (i : ℕ), ↥(𝒜 i)) a : ⨁ (i : ℕ), ↥(𝒜 i)) : (a : ℕ) → ↥(𝒜 a)) i) : A) ^
                    m)
                  ⋯,
              den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i)) (f ^ i) ⋯, den_mem := ⋯ :
              HomogeneousLocalization.NumDenSameDeg 𝒜 (Submonoid.powers f) })))
have rw : Eq (α :=
  Set
    (↑(↑(Proj.restrict (U := Functor.obj (C := Opens (↑Proj.T : Type u_1)) (Opens.toTopCat Proj.T) (pbo f))
                sorry).toPresheafedSpace :
          TopCat) :
      Type u_1))
  (Subtype.val (p := fun (x : (↑Proj.T : Type u_1)) ↦ Membership.mem (γ := Opens (↑Proj.T : Type u_1)) (pbo f) x) ⁻¹'
    (↑(pbo (↑((((decompose 𝒜 : (a : A) → ⨁ (i : ℕ), ↥(𝒜 i)) a : ⨁ (i : ℕ), ↥(𝒜 i)) : (a : ℕ) → ↥(𝒜 a)) i) : A)) :
      Set (ProjectiveSpectrum 𝒜)))
  ((⇑(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))
                  sorry).toPresheafedSpace :
            TopCat))
          (toSpec 𝒜 f)) :
      (a : (↑(↑(Proj.restrict sorry).toPresheafedSpace : TopCat) : Type u_1)) →
        (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1)) ⁻¹'
    (↑(sbo
          HomogeneousLocalization.mk
            { deg := m * i,
              num :=
                Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i))
                  ((↑((((decompose 𝒜 : (a : A) → ⨁ (i : ℕ), ↥(𝒜 i)) a : ⨁ (i : ℕ), ↥(𝒜 i)) : (a : ℕ) → ↥(𝒜 a)) i) : A) ^
                    m)
                  sorry,
              den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (m * i)) (f ^ i) sorry, den_mem := sorry :
              HomogeneousLocalization.NumDenSameDeg 𝒜 (Submonoid.powers f) }) :
      Set (PrimeSpectrum (A⁰_ f))))
Tactic: rw [Opens.carrier_eq_coe, toSpec_preimage_basicOpen, ProjectiveSpectrum.basicOpen_pow 𝒜 _ m hm]