-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic (goal)
Goal:
σ : Type u_1
A : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
𝒜 : ℕ → σ
inst_3 : GradedRing 𝒜
f : A
m' : ℕ
g : A
g_deg : g ∈ 𝒜 m'
x : A
hx : x = f * g
a : (↑(CommRingCat.of (Away 𝒜 f)) : Type u)
i : (↑(ProjectiveSpectrum.top 𝒜) : Type u)
hi :
  Membership.mem (γ := TopologicalSpace.Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u))
    (Opposite.unop (Opposite.op (basicOpen 𝒜 x)) : TopologicalSpace.Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u)) i
⊢ Eq (α :=
    Localization (M := A)
      (↑(Subtype.mk (p := fun (x_1 : (↑(ProjectiveSpectrum.top 𝒜) : Type u)) ↦
                  Membership.mem (γ := TopologicalSpace.Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u))
                    (Opposite.unop (Opposite.op (basicOpen 𝒜 x)) :
                      TopologicalSpace.Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u))
                    x_1)
                  i hi) :
              (↑(ProjectiveSpectrum.top 𝒜) : Type u)).asHomogeneousIdeal.toIdeal.primeCompl)
    (val.{0, u, u_1} (ι := ℕ) (σ := σ) (𝒜 := 𝒜)
      ((↑((CommRingCat.Hom.hom (CommRingCat.ofHom (awayMap 𝒜 g_deg hx) ≫ awayToSection 𝒜 x) :
                (a : (↑(CommRingCat.of (Away 𝒜 f)) : Type u)) → (↑Γ(Proj 𝒜, basicOpen 𝒜 x) : Type u))
              a) :
          (x_1 : ↥(Opposite.unop (Opposite.op (basicOpen 𝒜 x)))) →
            (fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u)) ↦ AtPrime 𝒜 x.asHomogeneousIdeal.toIdeal)
              (↑x_1 : (↑(ProjectiveSpectrum.top 𝒜) : Type u)))
        (Subtype.mk (p := fun (x_1 : (↑(ProjectiveSpectrum.top 𝒜) : Type u)) ↦
          Membership.mem (γ := TopologicalSpace.Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u))
            (Opposite.unop (Opposite.op (basicOpen 𝒜 x)) :
              TopologicalSpace.Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u))
            x_1)
          i hi)))
    (val.{0, u, u_1} (ι := ℕ) (σ := σ) (𝒜 := 𝒜)
      ((↑((CommRingCat.Hom.hom (awayToSection 𝒜 f ≫ (Proj 𝒜).presheaf.map (Quiver.Hom.op (homOfLE ⋯))) :
                (a : (↑(CommRingCat.of (Away 𝒜 f)) : Type u)) → (↑Γ(Proj 𝒜, basicOpen 𝒜 x) : Type u))
              a) :
          (x_1 : ↥(Opposite.unop (Opposite.op (basicOpen 𝒜 x)))) →
            (fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u)) ↦ AtPrime 𝒜 x.asHomogeneousIdeal.toIdeal)
              (↑x_1 : (↑(ProjectiveSpectrum.top 𝒜) : Type u)))
        (Subtype.mk (p := fun (x_1 : (↑(ProjectiveSpectrum.top 𝒜) : Type u)) ↦
          Membership.mem (γ := TopologicalSpace.Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u))
            (Opposite.unop (Opposite.op (basicOpen 𝒜 x)) :
              TopologicalSpace.Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u))
            x_1)
          i hi)))
have hf : ∀ (n : ℕ) (a : ↥(𝒜 n)) (i_1 : ℕ) (hb' : (fun (x : ℕ) ↦ f ^ x) i_1 ∈ 𝒜 n),
  Eq (α :=
    Localization (M := A)
      (↑(Subtype.mk (p := fun (x_1 : (↑(ProjectiveSpectrum.top 𝒜) : Type u)) ↦
                  Membership.mem (γ := TopologicalSpace.Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u))
                    (Opposite.unop (Opposite.op (basicOpen 𝒜 x)) :
                      TopologicalSpace.Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u))
                    x_1)
                  i hi) :
              (↑(ProjectiveSpectrum.top 𝒜) : Type u)).asHomogeneousIdeal.toIdeal.primeCompl)
    (val.{0, u, u_1} (ι := ℕ) (σ := σ) (𝒜 := 𝒜)
      ((↑((CommRingCat.Hom.hom (CommRingCat.ofHom (awayMap 𝒜 g_deg hx) ≫ awayToSection 𝒜 x) :
                (a : (↑(CommRingCat.of (Away 𝒜 f)) : Type u)) → (↑Γ(Proj 𝒜, basicOpen 𝒜 x) : Type u))
              (mk
                { deg := n, num := a, den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 n) ((fun (x : ℕ) ↦ f ^ x) i_1) hb',
                  den_mem := sorry })) :
          (x_1 : ↥(Opposite.unop (Opposite.op (basicOpen 𝒜 x)))) →
            (fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u)) ↦ AtPrime 𝒜 x.asHomogeneousIdeal.toIdeal)
              (↑x_1 : (↑(ProjectiveSpectrum.top 𝒜) : Type u)))
        (Subtype.mk (p := fun (x_1 : (↑(ProjectiveSpectrum.top 𝒜) : Type u)) ↦
          Membership.mem (γ := TopologicalSpace.Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u))
            (Opposite.unop (Opposite.op (basicOpen 𝒜 x)) :
              TopologicalSpace.Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u))
            x_1)
          i hi)))
    (val.{0, u, u_1} (ι := ℕ) (σ := σ) (𝒜 := 𝒜)
      ((↑((CommRingCat.Hom.hom (awayToSection 𝒜 f ≫ (Proj 𝒜).presheaf.map (Quiver.Hom.op (homOfLE sorry))) :
                (a : (↑(CommRingCat.of (Away 𝒜 f)) : Type u)) → (↑Γ(Proj 𝒜, basicOpen 𝒜 x) : Type u))
              (mk
                { deg := n, num := a, den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 n) ((fun (x : ℕ) ↦ f ^ x) i_1) hb',
                  den_mem := sorry })) :
          (x_1 : ↥(Opposite.unop (Opposite.op (basicOpen 𝒜 x)))) →
            (fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u)) ↦ AtPrime 𝒜 x.asHomogeneousIdeal.toIdeal)
              (↑x_1 : (↑(ProjectiveSpectrum.top 𝒜) : Type u)))
        (Subtype.mk (p := fun (x_1 : (↑(ProjectiveSpectrum.top 𝒜) : Type u)) ↦
          Membership.mem (γ := TopologicalSpace.Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u))
            (Opposite.unop (Opposite.op (basicOpen 𝒜 x)) :
              TopologicalSpace.Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u))
            x_1)
          i hi)))
Tactic: obtain ⟨⟨n, a, ⟨b, hb'⟩, i, rfl : _ = b⟩, rfl⟩ := mk_surjective a
Cleared hypotheses: a