-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
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)
hf :
  ∀ (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)))
⊢ Eq.{u + 1} (α :=
    (x_1 :
        ↥(Opposite.unop (Opposite.op (basicOpen 𝒜 x)) :
            TopologicalSpace.Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u))) →
      (fun (x : (↑(ProjectiveSpectrum.top 𝒜) : Type u)) ↦ AtPrime 𝒜 x.asHomogeneousIdeal.toIdeal)
        (↑x_1 : (↑(ProjectiveSpectrum.top 𝒜) : Type u)))
    (↑((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)))
    (↑((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)))

Tactic:
ext ⟨i, hi⟩