-- 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
x₁ x₂ :
  (↑(↑(Proj.restrict (U := Functor.obj (C := Opens (↑Proj.T : Type u_1)) (Opens.toTopCat Proj.T) (pbo f))
              ⋯).toPresheafedSpace :
        TopCat) :
    Type u_1)
h :
  Eq (α := (↑(↑(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))
        x₁ :
      (↑(↑(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))
        x₂ :
      (↑(↑(Spec A⁰_ f).toPresheafedSpace : TopCat) : Type u_1))
this :
  Eq (α :=
    (↑(↑(Proj.restrict (U := Functor.obj (C := Opens (↑Proj.T : Type u_1)) (Opens.toTopCat Proj.T) (pbo f))
                ⋯).toPresheafedSpace :
          TopCat) :
      Type u_1))
    (FromSpec.toFun f_deg hm
      ((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))
        x₁))
    (FromSpec.toFun f_deg hm
      ((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))
        x₂))
rwa :
  ∀
    (this :
      x₁ =
        FromSpec.toFun f_deg hm
          ((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))
            x₂)),
    x₁ = x₂
⊢ x₁ = x₂
have rwa₁ : ∀ (this : x₁ = x₂), x₁ = x₂
Tactic: rwa [fromSpec_toSpec, fromSpec_toSpec] at this
Cleared hypotheses: this