-- 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
i_1 : (↑(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_1
n : ℕ
a : ↥(𝒜 n)
i : ℕ
hb' : (fun (x : ℕ) ↦ f ^ x) i ∈ 𝒜 n
⊢ Eq (α := Localization (M := A) i_1.asHomogeneousIdeal.toIdeal.primeCompl)
    (Localization.mk ((RingHom.id A : (a : A) → A) ((↑a : A) * g ^ i))
        (Subtype.mk (p := fun (x_1 : A) ↦
          x_1 ∈
            (↑(Subtype.mk (p := fun (x_2 : (↑(ProjectiveSpectrum.top 𝒜) : Type u)) ↦
                        Membership.mem (γ := TopologicalSpace.Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u))
                          (basicOpen 𝒜 x : (Proj 𝒜).Opens) x_2)
                        i_1 hi) :
                    (↑(ProjectiveSpectrum.top 𝒜) : Type u)).asHomogeneousIdeal.toIdeal.primeCompl)
          ((RingHom.id A : (a : A) → A)
            (↑(Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1) (x ^ i) ⋯) :
              A))
          ⋯) :
      Localization (M := A)
        (↑(Subtype.mk (p := fun (x_1 : (↑(ProjectiveSpectrum.top 𝒜) : Type u)) ↦
                    Membership.mem (γ := TopologicalSpace.Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u))
                      (basicOpen 𝒜 x : (Proj 𝒜).Opens) x_1)
                    i_1 hi) :
                (↑(ProjectiveSpectrum.top 𝒜) : Type u)).asHomogeneousIdeal.toIdeal.primeCompl)
    (val.{0, u, u_1} (ι := ℕ) (σ := σ) (𝒜 := 𝒜)
        ((↑((CommRingCat.Hom.hom ((Proj 𝒜).presheaf.map (Quiver.Hom.op (homOfLE ⋯))) :
                  (a : (↑Γ(Proj 𝒜, basicOpen 𝒜 f) : Type u)) → (↑Γ(Proj 𝒜, basicOpen 𝒜 x) : Type u))
                ((CommRingCat.Hom.hom (awayToSection 𝒜 f) : (a : Away 𝒜 f) → (↑Γ(Proj 𝒜, basicOpen 𝒜 f) : Type u))
                  (mk
                    { deg := n, num := a, den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 n) (f ^ i) hb',
                      den_mem := ⋯ }))) :
            (x_1 : ↥(basicOpen 𝒜 x)) →
              AtPrime 𝒜 (↑x_1 : (↑(ProjectiveSpectrum.top 𝒜) : Type u)).asHomogeneousIdeal.toIdeal)
          (Subtype.mk (p := fun (x_1 : (↑(ProjectiveSpectrum.top 𝒜) : Type u)) ↦
            Membership.mem (γ := TopologicalSpace.Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u))
              (basicOpen 𝒜 x : (Proj 𝒜).Opens) x_1)
            i_1 hi)) :
      Localization (M := A) i_1.asHomogeneousIdeal.toIdeal.primeCompl)
have hf : ((Localization.r.{u} (M := A)
        (↑(Subtype.mk (p := fun (x_1 : (↑(ProjectiveSpectrum.top 𝒜) : Type u)) ↦
                    Membership.mem (γ := TopologicalSpace.Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u))
                      (basicOpen 𝒜 x : (Proj 𝒜).Opens) x_1)
                    i_1 hi) :
                (↑(ProjectiveSpectrum.top 𝒜) : Type u)).asHomogeneousIdeal.toIdeal.primeCompl :
      Con
        (A ×
          ↥(↑(Subtype.mk (p := fun (x_1 : (↑(ProjectiveSpectrum.top 𝒜) : Type u)) ↦
                        Membership.mem (γ := TopologicalSpace.Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u))
                          (basicOpen 𝒜 x : (Proj 𝒜).Opens) x_1)
                        i_1 hi) :
                    (↑(ProjectiveSpectrum.top 𝒜) : Type u)).asHomogeneousIdeal.toIdeal.primeCompl)) :
    (a : A × ↥(↑⟨i_1, hi⟩ : (↑(ProjectiveSpectrum.top 𝒜) : Type u)).asHomogeneousIdeal.toIdeal.primeCompl) →
      A × ↥(↑⟨i_1, hi⟩ : (↑(ProjectiveSpectrum.top 𝒜) : Type u)).asHomogeneousIdeal.toIdeal.primeCompl → Prop)
  (((RingHom.id A : (a : A) → A) ((↑a : A) * g ^ i),
      Subtype.mk (p := fun (x_1 : A) ↦
        x_1 ∈
          (↑(Subtype.mk (p := fun (x_2 : (↑(ProjectiveSpectrum.top 𝒜) : Type u)) ↦
                      Membership.mem (γ := TopologicalSpace.Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u))
                        (basicOpen 𝒜 x : (Proj 𝒜).Opens) x_2)
                      i_1 hi) :
                  (↑(ProjectiveSpectrum.top 𝒜) : Type u)).asHomogeneousIdeal.toIdeal.primeCompl)
        ((RingHom.id A : (a : A) → A)
          (↑(Subtype.mk (p := fun (x_1 : A) ↦ Membership.mem (γ := Submonoid A) (Submonoid.powers x) x_1) (x ^ i) sorry) :
            A))
        sorry) :
    A ×
      ↥(↑(Subtype.mk (p := fun (x_1 : (↑(ProjectiveSpectrum.top 𝒜) : Type u)) ↦
                    Membership.mem (γ := TopologicalSpace.Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u))
                      (basicOpen 𝒜 x : (Proj 𝒜).Opens) x_1)
                    i_1 hi) :
                (↑(ProjectiveSpectrum.top 𝒜) : Type u)).asHomogeneousIdeal.toIdeal.primeCompl)
  ((↑(NumDenSameDeg.num
          ((fun (x_1 : NumDenSameDeg 𝒜 (Submonoid.powers f)) ↦
              ({ deg := x_1.deg,
                  num :=
                    Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 x_1.deg) ((GradedRingHom.id 𝒜 : (a : A) → A) (↑x_1.num : A)) sorry,
                  den :=
                    Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 x_1.deg) ((GradedRingHom.id 𝒜 : (a : A) → A) (↑x_1.den : A)) sorry,
                  den_mem := sorry } :
                NumDenSameDeg 𝒜
                  (Ideal.primeCompl
                    (HomogeneousIdeal.toIdeal.{0, u_1, u} (σ := σ) (𝒜 := 𝒜)
                      (ProjectiveSpectrum.asHomogeneousIdeal
                        (↑((Quiver.Hom.unop (Quiver.Hom.op (homOfLE sorry)) :
                                (a : ↥(Opposite.unop (Opposite.op (basicOpen 𝒜 x)))) →
                                  ↥(Opposite.unop (Opposite.op (basicOpen 𝒜 f))))
                              (Subtype.mk (p := fun (x_2 : (↑(ProjectiveSpectrum.top 𝒜) : Type u)) ↦
                                Membership.mem (γ := TopologicalSpace.Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u))
                                  (basicOpen 𝒜 x : (Proj 𝒜).Opens) x_2)
                                i_1 hi)) :
                          (↑(ProjectiveSpectrum.top 𝒜) : Type u)))))))
            { deg := n, num := a, den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 n) (f ^ i) hb', den_mem := sorry })) :
      A),
    Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ i_1.asHomogeneousIdeal.toIdeal.primeCompl)
      (↑(NumDenSameDeg.den
            ((fun (x_1 : NumDenSameDeg 𝒜 (Submonoid.powers f)) ↦
                ({ deg := x_1.deg,
                    num :=
                      Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 x_1.deg) ((GradedRingHom.id 𝒜 : (a : A) → A) (↑x_1.num : A))
                        sorry,
                    den :=
                      Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 x_1.deg) ((GradedRingHom.id 𝒜 : (a : A) → A) (↑x_1.den : A))
                        sorry,
                    den_mem := sorry } :
                  NumDenSameDeg 𝒜
                    (Ideal.primeCompl
                      (HomogeneousIdeal.toIdeal.{0, u_1, u} (σ := σ) (𝒜 := 𝒜)
                        (ProjectiveSpectrum.asHomogeneousIdeal
                          (↑((Quiver.Hom.unop (Quiver.Hom.op (homOfLE sorry)) :
                                  (a : ↥(Opposite.unop (Opposite.op (basicOpen 𝒜 x)))) →
                                    ↥(Opposite.unop (Opposite.op (basicOpen 𝒜 f))))
                                (Subtype.mk (p := fun (x_2 : (↑(ProjectiveSpectrum.top 𝒜) : Type u)) ↦
                                  Membership.mem (γ := TopologicalSpace.Opens (↑(ProjectiveSpectrum.top 𝒜) : Type u))
                                    (basicOpen 𝒜 x : (Proj 𝒜).Opens) x_2)
                                  i_1 hi)) :
                            (↑(ProjectiveSpectrum.top 𝒜) : Type u)))))))
              { deg := n, num := a, den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 n) (f ^ i) hb', den_mem := sorry })) :
        A)
      sorry)
Tactic: refine Localization.mk_eq_mk_iff.mpr ?_