-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor (goal)
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))
⊢ 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)
have hf₁ : Eq (α :=
  HomogeneousLocalization ℬ
    (Ideal.primeCompl
      (HomogeneousSubmodule.toSubmodule (σA := τ) (𝒜 := ℬ)
        (asHomogeneousIdeal
          (↑((Quiver.Hom.unop (Quiver.Hom.op (homOfLE sorry)) :
                  (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 sorry)) :
                              (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)) sorry,
            den := Subtype.mk (p := fun (x_1 : B) ↦ x_1 ∈ ℬ x.deg) ((f : (a : A) → B) (↑x.den : A)) sorry, den_mem := sorry } :
          NumDenSameDeg ℬ
            (Ideal.primeCompl
              (HomogeneousSubmodule.toSubmodule (σA := τ) (𝒜 := ℬ)
                (asHomogeneousIdeal
                  (↑((Quiver.Hom.unop (Quiver.Hom.op (homOfLE sorry)) :
                          (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)) sorry,
              den :=
                Subtype.mk (p := fun (x_1 : A) ↦ x_1 ∈ 𝒜 x.deg) ((GradedRingHom.id 𝒜 : (a : A) → A) (↑x.den : A)) sorry,
              den_mem := sorry } :
            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 sorry)) :
                                    (a : ↥(Opposite.unop (Opposite.op (basicOpen ℬ ((f : (a : A) → B) s))))) →
                                      ↥(Opposite.unop (Opposite.op (map f hf ⁻¹ᵁ basicOpen 𝒜 s))))
                                  p) :
                              ProjectiveSpectrum ℬ))
                          sorry) :
                      (↑(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) sorry, den_mem := sorry })))
  (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)) sorry,
            den := Subtype.mk (p := fun (x_1 : B) ↦ x_1 ∈ ℬ x.deg) ((GradedRingHom.id ℬ : (a : B) → B) (↑x.den : B)) sorry,
            den_mem := sorry } :
          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) sorry,
        den := Subtype.mk (p := fun (x : B) ↦ x ∈ ℬ (n • i)) (HPow.hPow (α := B) ((f : (a : A) → B) s : B) n) sorry,
        den_mem := sorry }))
Tactic: change HomogeneousLocalization.mk _ = .mk _