-- 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
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
h :
  (↑1 : A) *
      HMul.hMul (β := A)
        (↑((↑(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)) ⋯,
                              den :=
                                Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 x_1.deg)
                                  ((GradedRingHom.id 𝒜 : (a : A) → A) (↑x_1.den : A)) ⋯,
                              den_mem := ⋯ } :
                            NumDenSameDeg 𝒜
                              (Ideal.primeCompl
                                (HomogeneousIdeal.toIdeal.{0, u_1, u} (σ := σ) (𝒜 := 𝒜)
                                  (ProjectiveSpectrum.asHomogeneousIdeal
                                    (↑((Quiver.Hom.unop (Quiver.Hom.op (homOfLE ⋯)) :
                                            (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 := ⋯ :
                          NumDenSameDeg 𝒜 (Submonoid.powers f) })) :
                  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)) ⋯,
                                den :=
                                  Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 x_1.deg)
                                    ((GradedRingHom.id 𝒜 : (a : A) → A) (↑x_1.den : A)) ⋯,
                                den_mem := ⋯ } :
                              NumDenSameDeg 𝒜
                                (Ideal.primeCompl
                                  (HomogeneousIdeal.toIdeal.{0, u_1, u} (σ := σ) (𝒜 := 𝒜)
                                    (ProjectiveSpectrum.asHomogeneousIdeal
                                      (↑((Quiver.Hom.unop (Quiver.Hom.op (homOfLE ⋯)) :
                                              (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 := ⋯ : NumDenSameDeg 𝒜 (Submonoid.powers f) })) :
                    A)
                  ⋯).2 :
          A)
        (((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))
                ⋯).1 :
          A) =
    (↑1 : A) *
      HMul.hMul (α := A)
        ((↑((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))
                    ⋯).2 :
            A) :
          A)
        ((↑(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)) ⋯,
                          den :=
                            Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 x_1.deg)
                              ((GradedRingHom.id 𝒜 : (a : A) → A) (↑x_1.den : A)) ⋯,
                          den_mem := ⋯ } :
                        NumDenSameDeg 𝒜
                          (Ideal.primeCompl
                            (HomogeneousIdeal.toIdeal.{0, u_1, u} (σ := σ) (𝒜 := 𝒜)
                              (ProjectiveSpectrum.asHomogeneousIdeal
                                (↑((Quiver.Hom.unop (Quiver.Hom.op (homOfLE ⋯)) :
                                        (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 := ⋯ :
                      NumDenSameDeg 𝒜 (Submonoid.powers f) })) :
              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)) ⋯,
                            den :=
                              Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 x_1.deg)
                                ((GradedRingHom.id 𝒜 : (a : A) → A) (↑x_1.den : A)) ⋯,
                            den_mem := ⋯ } :
                          NumDenSameDeg 𝒜
                            (Ideal.primeCompl
                              (HomogeneousIdeal.toIdeal.{0, u_1, u} (σ := σ) (𝒜 := 𝒜)
                                (ProjectiveSpectrum.asHomogeneousIdeal
                                  (↑((Quiver.Hom.unop (Quiver.Hom.op (homOfLE ⋯)) :
                                          (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 := ⋯ :
                        NumDenSameDeg 𝒜 (Submonoid.powers f) })) :
                A)
              ⋯).1
⊢ ∃ (c :
    ↥(↑(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),
    (↑c : A) *
        HMul.hMul (β := A)
          (↑((↑(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)) ⋯,
                                den :=
                                  Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 x_1.deg)
                                    ((GradedRingHom.id 𝒜 : (a : A) → A) (↑x_1.den : A)) ⋯,
                                den_mem := ⋯ } :
                              NumDenSameDeg 𝒜
                                (Ideal.primeCompl
                                  (HomogeneousIdeal.toIdeal.{0, u_1, u} (σ := σ) (𝒜 := 𝒜)
                                    (ProjectiveSpectrum.asHomogeneousIdeal
                                      (↑((Quiver.Hom.unop (Quiver.Hom.op (homOfLE ⋯)) :
                                              (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 := ⋯ : NumDenSameDeg 𝒜 (Submonoid.powers f) })) :
                    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)) ⋯,
                                  den :=
                                    Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 x_1.deg)
                                      ((GradedRingHom.id 𝒜 : (a : A) → A) (↑x_1.den : A)) ⋯,
                                  den_mem := ⋯ } :
                                NumDenSameDeg 𝒜
                                  (Ideal.primeCompl
                                    (HomogeneousIdeal.toIdeal.{0, u_1, u} (σ := σ) (𝒜 := 𝒜)
                                      (ProjectiveSpectrum.asHomogeneousIdeal
                                        (↑((Quiver.Hom.unop (Quiver.Hom.op (homOfLE ⋯)) :
                                                (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 := ⋯ : NumDenSameDeg 𝒜 (Submonoid.powers f) })) :
                      A)
                    ⋯).2 :
            A)
          (((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))
                  ⋯).1 :
            A) =
      (↑c : A) *
        HMul.hMul (α := A)
          ((↑((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))
                      ⋯).2 :
              A) :
            A)
          ((↑(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)) ⋯,
                            den :=
                              Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 x_1.deg)
                                ((GradedRingHom.id 𝒜 : (a : A) → A) (↑x_1.den : A)) ⋯,
                            den_mem := ⋯ } :
                          NumDenSameDeg 𝒜
                            (Ideal.primeCompl
                              (HomogeneousIdeal.toIdeal.{0, u_1, u} (σ := σ) (𝒜 := 𝒜)
                                (ProjectiveSpectrum.asHomogeneousIdeal
                                  (↑((Quiver.Hom.unop (Quiver.Hom.op (homOfLE ⋯)) :
                                          (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 := ⋯ :
                        NumDenSameDeg 𝒜 (Submonoid.powers f) })) :
                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)) ⋯,
                              den :=
                                Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 x_1.deg)
                                  ((GradedRingHom.id 𝒜 : (a : A) → A) (↑x_1.den : A)) ⋯,
                              den_mem := ⋯ } :
                            NumDenSameDeg 𝒜
                              (Ideal.primeCompl
                                (HomogeneousIdeal.toIdeal.{0, u_1, u} (σ := σ) (𝒜 := 𝒜)
                                  (ProjectiveSpectrum.asHomogeneousIdeal
                                    (↑((Quiver.Hom.unop (Quiver.Hom.op (homOfLE ⋯)) :
                                            (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 := ⋯ :
                          NumDenSameDeg 𝒜 (Submonoid.powers f) })) :
                  A)
                ⋯).1

Tactic:
use 1