-- 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 (α :=
    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 := ⋯ }))
⊢ Eq.{u + 1} (α := (fun (x : (↑(top ℬ) : Type u)) ↦ AtPrime ℬ x.asHomogeneousIdeal.toIdeal) (↑p : (↑(top ℬ) : Type u)))
    ((↑((CommRingCat.Hom.hom (Scheme.Hom.appLE (map f hf) (basicOpen 𝒜 s) (basicOpen ℬ ((f : (a : A) → B) s)) ⋯) :
              (a : (↑Γ(Proj 𝒜, basicOpen 𝒜 s) : Type u)) → (↑Γ(Proj ℬ, basicOpen ℬ ((f : (a : A) → B) s)) : Type u))
            ((CommRingCat.Hom.hom (awayToSection 𝒜 s) : (a : Away 𝒜 s) → (↑Γ(Proj 𝒜, basicOpen 𝒜 s) : Type u))
              (Away.mk 𝒜 hs n x hx))) :
        (x : ↥(Opposite.unop (Opposite.op (basicOpen ℬ ((f : (a : A) → B) s))))) →
          (fun (x : (↑(top ℬ) : Type u)) ↦ AtPrime ℬ x.asHomogeneousIdeal.toIdeal) (↑x : (↑(top ℬ) : Type u)))
      p)
    ((↑((CommRingCat.Hom.hom (awayToSection ℬ ((f : (a : A) → B) s)) :
              (a : Away ℬ ((f : (a : A) → B) s)) → (↑Γ(Proj ℬ, basicOpen ℬ ((f : (a : A) → B) s)) : Type u))
            (Away.mk ℬ ⋯ n ((f : (a : A) → B) x) ⋯)) :
        (x : ↥(Opposite.unop (Opposite.op (basicOpen ℬ ((f : (a : A) → B) s))))) →
          (fun (x : (↑(top ℬ) : Type u)) ↦ AtPrime ℬ x.asHomogeneousIdeal.toIdeal) (↑x : (↑(top ℬ) : Type u)))
      p)

Tactic:
change HomogeneousLocalization.mk _ = .mk _

Premises used: HomogeneousLocalization.mk