-- 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 : ℕ
rw :
  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 𝒜)))
    ((⇑(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)) ⁻¹'
      (↑(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) }) :
        Set (PrimeSpectrum (A⁰_ f))))
⊢ 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 𝒜)))
  (Subtype.val (p := fun (x : (↑Proj.T : Type u_1)) ↦ Membership.mem (γ := Opens (↑Proj.T : Type u_1)) (pbo f) x) ⁻¹'
    (↑(pbo
          (↑(HomogeneousLocalization.NumDenSameDeg.num
                { 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) }) :
            A)) :
      Set (ProjectiveSpectrum 𝒜)))
Tactic: rw [Opens.carrier_eq_coe, toSpec_preimage_basicOpen, ProjectiveSpectrum.basicOpen_pow 𝒜 _ m hm]