-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor
Goal:
A B σ τ : Type u
inst : CommRing A
inst_1 : SetLike σ A
inst_2 : AddSubgroupClass σ A
inst_3 : CommRing B
inst_4 : SetLike τ B
inst_5 : AddSubgroupClass τ B
𝒜 : ℕ → σ
ℬ : ℕ → τ
inst_6 : GradedRing 𝒜
inst_7 : GradedRing ℬ
f : 𝒜 →+*ᵍ ℬ
hf : LE.le (α := HomogeneousIdeal ℬ) (ℬ₊) (HomogeneousIdeal.map f (𝒜₊))
i : ℕ
s : A
hs : s ∈ 𝒜 i
n : ℕ
x : A
hx : x ∈ 𝒜 (n • i)
p : ↥(Opposite.unop (Opposite.op (basicOpen ℬ ((f : (a : A) → B) s))) : Opens (↑(top ℬ) : Type u))
hf₁ :
  Eq (α :=
    Localization (M := B)
      (Ideal.primeCompl
        (HomogeneousSubmodule.toSubmodule (σA := τ) (𝒜 := ℬ)
          (asHomogeneousIdeal
            (↑((Quiver.Hom.unop (Quiver.Hom.op (homOfLE ⋯)) :
                    (a : ↥(Opposite.unop (Opposite.op (basicOpen ℬ ((f : (a : A) → B) s))))) →
                      ↥(Opposite.unop (Opposite.op (map f hf ⁻¹ᵁ basicOpen 𝒜 s))))
                  p) :
              ProjectiveSpectrum ℬ)))))
    (val (ι := ℕ) (σ := τ) (𝒜 := ℬ)
      (HomogeneousLocalization.mk
        ((fun
              (x :
                NumDenSameDeg 𝒜
                  (Ideal.primeCompl
                    (Ideal.comap f
                      (HomogeneousSubmodule.toSubmodule (σA := τ) (𝒜 := ℬ)
                        (asHomogeneousIdeal
                          (↑((Quiver.Hom.unop (Quiver.Hom.op (homOfLE ⋯)) :
                                  (a : ↥(Opposite.unop (Opposite.op (basicOpen ℬ ((f : (a : A) → B) s))))) →
                                    ↥(Opposite.unop (Opposite.op (map f hf ⁻¹ᵁ basicOpen 𝒜 s))))
                                p) :
                            ProjectiveSpectrum ℬ)))))) ↦
            ({ deg := x.deg, num := Subtype.mk (p := fun (x_1 : B) ↦ x_1 ∈ ℬ x.deg) ((f : (a : A) → B) (↑x.num : A)) ⋯,
                den := Subtype.mk (p := fun (x_1 : B) ↦ x_1 ∈ ℬ x.deg) ((f : (a : A) → B) (↑x.den : A)) ⋯,
                den_mem := ⋯ } :
              NumDenSameDeg ℬ
                (Ideal.primeCompl
                  (HomogeneousSubmodule.toSubmodule (σA := τ) (𝒜 := ℬ)
                    (asHomogeneousIdeal
                      (↑((Quiver.Hom.unop (Quiver.Hom.op (homOfLE ⋯)) :
                              (a : ↥(Opposite.unop (Opposite.op (basicOpen ℬ ((f : (a : A) → B) s))))) →
                                ↥(Opposite.unop (Opposite.op (map f hf ⁻¹ᵁ basicOpen 𝒜 s))))
                            p) :
                        ProjectiveSpectrum ℬ))))))
          ((fun (x : NumDenSameDeg 𝒜 (Submonoid.powers s)) ↦
              ({ deg := x.deg,
                  num :=
                    Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ 𝒜 x.deg) ((GradedRingHom.id 𝒜 : (a : A) → A) (↑x.num : A)) ⋯,
                  den :=
                    Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ 𝒜 x.deg) ((GradedRingHom.id 𝒜 : (a : A) → A) (↑x.den : A)) ⋯,
                  den_mem := ⋯ } :
                NumDenSameDeg 𝒜
                  (Ideal.primeCompl
                    (toIdeal (σ := σ) (𝒜 := 𝒜)
                      (asHomogeneousIdeal
                        (↑(Subtype.mk (p := fun (x : ProjectiveSpectrum 𝒜) ↦
                              Membership.mem (γ := Opens (ProjectiveSpectrum 𝒜))
                                (Opposite.unop (Opposite.op (basicOpen 𝒜 s)) : Opens (↑(top 𝒜) : Type u)) x)
                              (((ProjectiveSpectrum.comap f hf : C(ProjectiveSpectrum ℬ, ProjectiveSpectrum 𝒜)) :
                                  (a : ProjectiveSpectrum ℬ) → ProjectiveSpectrum 𝒜)
                                (↑((Quiver.Hom.unop (Quiver.Hom.op (homOfLE ⋯)) :
                                        (a : ↥(Opposite.unop (Opposite.op (basicOpen ℬ ((f : (a : A) → B) s))))) →
                                          ↥(Opposite.unop (Opposite.op (map f hf ⁻¹ᵁ basicOpen 𝒜 s))))
                                      p) :
                                  ProjectiveSpectrum ℬ))
                              ⋯) :
                          (↑(top 𝒜) : Type u)))))))
            { deg := n • i, num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (n • i)) x hx,
              den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (n • i)) (s ^ n) ⋯, den_mem := ⋯ }))))
    (val (ι := ℕ) (σ := τ) (𝒜 := ℬ)
      (HomogeneousLocalization.mk
        ((fun (x : NumDenSameDeg (A := B) ℬ (Submonoid.powers ((f : (a : A) → B) s) : Submonoid B)) ↦
            ({ deg := x.deg,
                num :=
                  Subtype.mk (p := fun (x_1 : B) ↦ x_1 ∈ ℬ x.deg) ((GradedRingHom.id ℬ : (a : B) → B) (↑x.num : B)) ⋯,
                den :=
                  Subtype.mk (p := fun (x_1 : B) ↦ x_1 ∈ ℬ x.deg) ((GradedRingHom.id ℬ : (a : B) → B) (↑x.den : B)) ⋯,
                den_mem := ⋯ } :
              NumDenSameDeg ℬ (↑p : (↑(top ℬ) : Type u)).asHomogeneousIdeal.toIdeal.primeCompl))
          { deg := n • i, num := Subtype.mk (p := fun (x : B) ↦ x ∈ ℬ (n • i)) ((f : (a : A) → B) x) ⋯,
            den := Subtype.mk (p := fun (x : B) ↦ x ∈ ℬ (n • i)) (HPow.hPow (α := B) ((f : (a : A) → B) s : B) n) ⋯,
            den_mem := ⋯ })))
⊢ Eq (α :=
    HomogeneousLocalization ℬ
      (Ideal.primeCompl
        (HomogeneousSubmodule.toSubmodule (σA := τ) (𝒜 := ℬ)
          (asHomogeneousIdeal
            (↑((Quiver.Hom.unop (Quiver.Hom.op (homOfLE ⋯)) :
                    (a : ↥(Opposite.unop (Opposite.op (basicOpen ℬ ((f : (a : A) → B) s))))) →
                      ↥(Opposite.unop (Opposite.op (map f hf ⁻¹ᵁ basicOpen 𝒜 s))))
                  p) :
              ProjectiveSpectrum ℬ)))))
    (HomogeneousLocalization.mk
      ((fun
            (x :
              NumDenSameDeg 𝒜
                (Ideal.primeCompl
                  (Ideal.comap f
                    (HomogeneousSubmodule.toSubmodule (σA := τ) (𝒜 := ℬ)
                      (asHomogeneousIdeal
                        (↑((Quiver.Hom.unop (Quiver.Hom.op (homOfLE ⋯)) :
                                (a : ↥(Opposite.unop (Opposite.op (basicOpen ℬ ((f : (a : A) → B) s))))) →
                                  ↥(Opposite.unop (Opposite.op (map f hf ⁻¹ᵁ basicOpen 𝒜 s))))
                              p) :
                          ProjectiveSpectrum ℬ)))))) ↦
          ({ deg := x.deg, num := Subtype.mk (p := fun (x_1 : B) ↦ x_1 ∈ ℬ x.deg) ((f : (a : A) → B) (↑x.num : A)) ⋯,
              den := Subtype.mk (p := fun (x_1 : B) ↦ x_1 ∈ ℬ x.deg) ((f : (a : A) → B) (↑x.den : A)) ⋯,
              den_mem := ⋯ } :
            NumDenSameDeg ℬ
              (Ideal.primeCompl
                (HomogeneousSubmodule.toSubmodule (σA := τ) (𝒜 := ℬ)
                  (asHomogeneousIdeal
                    (↑((Quiver.Hom.unop (Quiver.Hom.op (homOfLE ⋯)) :
                            (a : ↥(Opposite.unop (Opposite.op (basicOpen ℬ ((f : (a : A) → B) s))))) →
                              ↥(Opposite.unop (Opposite.op (map f hf ⁻¹ᵁ basicOpen 𝒜 s))))
                          p) :
                      ProjectiveSpectrum ℬ))))))
        ((fun (x : NumDenSameDeg 𝒜 (Submonoid.powers s)) ↦
            ({ deg := x.deg,
                num :=
                  Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ 𝒜 x.deg) ((GradedRingHom.id 𝒜 : (a : A) → A) (↑x.num : A)) ⋯,
                den :=
                  Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ 𝒜 x.deg) ((GradedRingHom.id 𝒜 : (a : A) → A) (↑x.den : A)) ⋯,
                den_mem := ⋯ } :
              NumDenSameDeg 𝒜
                (Ideal.primeCompl
                  (toIdeal (σ := σ) (𝒜 := 𝒜)
                    (asHomogeneousIdeal
                      (↑(Subtype.mk (p := fun (x : ProjectiveSpectrum 𝒜) ↦
                            Membership.mem (γ := Opens (ProjectiveSpectrum 𝒜))
                              (Opposite.unop (Opposite.op (basicOpen 𝒜 s)) : Opens (↑(top 𝒜) : Type u)) x)
                            (((ProjectiveSpectrum.comap f hf : C(ProjectiveSpectrum ℬ, ProjectiveSpectrum 𝒜)) :
                                (a : ProjectiveSpectrum ℬ) → ProjectiveSpectrum 𝒜)
                              (↑((Quiver.Hom.unop (Quiver.Hom.op (homOfLE ⋯)) :
                                      (a : ↥(Opposite.unop (Opposite.op (basicOpen ℬ ((f : (a : A) → B) s))))) →
                                        ↥(Opposite.unop (Opposite.op (map f hf ⁻¹ᵁ basicOpen 𝒜 s))))
                                    p) :
                                ProjectiveSpectrum ℬ))
                            ⋯) :
                        (↑(top 𝒜) : Type u)))))))
          { deg := n • i, num := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (n • i)) x hx,
            den := Subtype.mk (p := fun (x : A) ↦ x ∈ 𝒜 (n • i)) (s ^ n) ⋯, den_mem := ⋯ })))
    (HomogeneousLocalization.mk
      ((fun (x : NumDenSameDeg (A := B) ℬ (Submonoid.powers ((f : (a : A) → B) s) : Submonoid B)) ↦
          ({ deg := x.deg,
              num :=
                Subtype.mk (p := fun (x_1 : B) ↦ x_1 ∈ ℬ x.deg) ((GradedRingHom.id ℬ : (a : B) → B) (↑x.num : B)) ⋯,
              den :=
                Subtype.mk (p := fun (x_1 : B) ↦ x_1 ∈ ℬ x.deg) ((GradedRingHom.id ℬ : (a : B) → B) (↑x.den : B)) ⋯,
              den_mem := ⋯ } :
            NumDenSameDeg ℬ (↑p : (↑(top ℬ) : Type u)).asHomogeneousIdeal.toIdeal.primeCompl))
        { deg := n • i, num := Subtype.mk (p := fun (x : B) ↦ x ∈ ℬ (n • i)) ((f : (a : A) → B) x) ⋯,
          den := Subtype.mk (p := fun (x : B) ↦ x ∈ ℬ (n • i)) (HPow.hPow (α := B) ((f : (a : A) → B) s : B) n) ⋯,
          den_mem := ⋯ }))

Tactic:
ext