-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor (goal)
Goal:
A : Type u_1
B : Type u_2
σ : Type u_4
τ : Type u_5
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 (𝒜₊))
U : Opens (ProjectiveSpectrum 𝒜)
V : Opens (ProjectiveSpectrum ℬ)
hUV :
  V.carrier ⊆
    (⇑(ProjectiveSpectrum.comap f hf : ContinuousMap.{u_2, u_1} (ProjectiveSpectrum ℬ) (ProjectiveSpectrum 𝒜)) :
        (a : ProjectiveSpectrum ℬ) → ProjectiveSpectrum 𝒜) ⁻¹'
      U.carrier
s : (x : ↥U) → AtPrime 𝒜 (↑x : ProjectiveSpectrum 𝒜).asHomogeneousIdeal.toSubmodule
hs :
  TopCat.PrelocalPredicate.pred (X := top 𝒜) (T := fun (x : (↑(top 𝒜) : Type u_1)) ↦
    AtPrime 𝒜 x.asHomogeneousIdeal.toIdeal)
    (TopCat.LocalPredicate.toPrelocalPredicate (T := fun (x : (↑(top 𝒜) : Type u_1)) ↦
        AtPrime 𝒜 x.asHomogeneousIdeal.toIdeal) (ProjectiveSpectrum.StructureSheaf.isLocallyFraction 𝒜) :
      TopCat.PrelocalPredicate (X := top 𝒜) fun (x : (↑(top 𝒜) : Type u_1)) ↦ AtPrime 𝒜 x.asHomogeneousIdeal.toIdeal)
    s
p : (↑(top ℬ) : Type u_2)
hpV : p ∈ V
W : Opens (↑(top 𝒜) : Type u_1)
m :
  Membership.mem (α := (↑(top 𝒜) : Type u_1)) W
    ((↑(Subtype.mk (p := fun (x : (↑(top 𝒜) : Type u_1)) ↦ x ∈ U)
            (((ProjectiveSpectrum.comap f hf : ContinuousMap.{u_2, u_1} (ProjectiveSpectrum ℬ) (ProjectiveSpectrum 𝒜)) :
                (a : ProjectiveSpectrum ℬ) → ProjectiveSpectrum 𝒜)
              p)
            ⋯) :
        (↑(top 𝒜) : Type u_1)) :
      (↑(top 𝒜) : Type u_1))
iWU : W ⟶ U
i : ℕ
a b : ↥(𝒜 i)
hb : ∀ (x : ↥W), (↑b : A) ∉ (↑x : (↑(top 𝒜) : Type u_1)).asHomogeneousIdeal
h_frac :
  ∀ (x : ↥W),
    Eq (α := AtPrime 𝒜 (↑x : (↑(top 𝒜) : Type u_1)).asHomogeneousIdeal.toIdeal)
      ((fun (x : ↥W) ↦
          (s ((iWU : (a : ↥W) → ↥U) x) :
            AtPrime 𝒜
              (HomogeneousSubmodule.toSubmodule.{0, 0, u_4, u_4, u_1, u_1} (σA := σ) (𝒜 := 𝒜)
                (asHomogeneousIdeal (↑((iWU : (a : ↥W) → ↥U) x) : ProjectiveSpectrum 𝒜)))))
        x)
      (HomogeneousLocalization.mk { deg := i, num := a, den := b, den_mem := ⋯ })
x :
  ↥(((Opens.comap (ProjectiveSpectrum.comap f hf) :
              FrameHom.{u_1, u_2} (Opens (ProjectiveSpectrum 𝒜)) (Opens (ProjectiveSpectrum ℬ))) :
            (a : Opens (ProjectiveSpectrum 𝒜)) → Opens (ProjectiveSpectrum ℬ))
          W ⊓
        V :
      Opens (↑(top ℬ) : Type u_2))
q : (↑(top ℬ) : Type u_2)
hqW :
  q ∈
    (↑(((Opens.comap (ProjectiveSpectrum.comap f hf) :
                FrameHom.{u_1, u_2} (Opens (ProjectiveSpectrum 𝒜)) (Opens (ProjectiveSpectrum ℬ))) :
              (a : Opens (ProjectiveSpectrum 𝒜)) → Opens (ProjectiveSpectrum ℬ))
            W :
          Opens (ProjectiveSpectrum ℬ)) :
      Set (↑(top ℬ) : Type u_2))
hqV : q ∈ (↑V : Set (↑(top ℬ) : Type u_2))
⊢ Eq (α :=
    AtPrime ℬ
      (↑(Subtype.mk (p := fun (x : (↑(top ℬ) : Type u_2)) ↦
                Membership.mem (γ := Opens (↑(top ℬ) : Type u_2))
                  (((Opens.comap (ProjectiveSpectrum.comap f hf) :
                            FrameHom.{u_1, u_2} (Opens (ProjectiveSpectrum 𝒜)) (Opens (ProjectiveSpectrum ℬ))) :
                          (a : Opens (ProjectiveSpectrum 𝒜)) → Opens (ProjectiveSpectrum ℬ))
                        W ⊓
                      V :
                    Opens (↑(top ℬ) : Type u_2))
                  x)
                q ⋯) :
            (↑(top ℬ) : Type u_2)).asHomogeneousIdeal.toIdeal)
    ((fun
          (x :
            ↥(((Opens.comap (ProjectiveSpectrum.comap f hf) :
                        FrameHom.{u_1, u_2} (Opens (ProjectiveSpectrum 𝒜)) (Opens (ProjectiveSpectrum ℬ))) :
                      (a : Opens (ProjectiveSpectrum 𝒜)) → Opens (ProjectiveSpectrum ℬ))
                    W ⊓
                  V :
                Opens (↑(top ℬ) : Type u_2))) ↦
        (comapStructureSheafFun f hf U V hUV s
            ((Opens.infLERight
                  (((Opens.comap (ProjectiveSpectrum.comap f hf) :
                        FrameHom.{u_1, u_2} (Opens (ProjectiveSpectrum 𝒜)) (Opens (ProjectiveSpectrum ℬ))) :
                      (a : Opens (ProjectiveSpectrum 𝒜)) → Opens (ProjectiveSpectrum ℬ))
                    W)
                  V :
                (a :
                    ↥((Opens.comap (ProjectiveSpectrum.comap f hf) :
                            (a : Opens (ProjectiveSpectrum 𝒜)) → Opens (ProjectiveSpectrum ℬ))
                          W ⊓
                        V)) →
                  ↥V)
              x) :
          AtPrime ℬ
            (HomogeneousSubmodule.toSubmodule.{0, 0, u_5, u_5, u_2, u_2} (σA := τ) (𝒜 := ℬ)
              (asHomogeneousIdeal
                (↑((Opens.infLERight
                          (((Opens.comap (ProjectiveSpectrum.comap f hf) :
                                FrameHom.{u_1, u_2} (Opens (ProjectiveSpectrum 𝒜)) (Opens (ProjectiveSpectrum ℬ))) :
                              (a : Opens (ProjectiveSpectrum 𝒜)) → Opens (ProjectiveSpectrum ℬ))
                            W)
                          V :
                        (a :
                            ↥((Opens.comap (ProjectiveSpectrum.comap f hf) :
                                    (a : Opens (ProjectiveSpectrum 𝒜)) → Opens (ProjectiveSpectrum ℬ))
                                  W ⊓
                                V)) →
                          ↥V)
                      x) :
                  ProjectiveSpectrum ℬ)))))
      (Subtype.mk (p := fun (x : (↑(top ℬ) : Type u_2)) ↦
        Membership.mem (γ := Opens (↑(top ℬ) : Type u_2))
          (((Opens.comap (ProjectiveSpectrum.comap f hf) :
                    FrameHom.{u_1, u_2} (Opens (ProjectiveSpectrum 𝒜)) (Opens (ProjectiveSpectrum ℬ))) :
                  (a : Opens (ProjectiveSpectrum 𝒜)) → Opens (ProjectiveSpectrum ℬ))
                W ⊓
              V :
            Opens (↑(top ℬ) : Type u_2))
          x)
        q ⋯))
    (HomogeneousLocalization.mk
      { deg := i, num := ((f.gradedAddHom i : AddMonoidHom.{u_1, u_2} ↥(𝒜 i) ↥(ℬ i)) : (a : ↥(𝒜 i)) → ↥(ℬ i)) a,
        den := ((f.gradedAddHom i : AddMonoidHom.{u_1, u_2} ↥(𝒜 i) ↥(ℬ i)) : (a : ↥(𝒜 i)) → ↥(ℬ i)) b, den_mem := ⋯ })
have a₁ : Eq (α :=
  Localization (M := B)
    (Ideal.primeCompl
      (HomogeneousSubmodule.toSubmodule.{0, 0, u_5, u_5, u_2, u_2} (σA := τ) (𝒜 := ℬ)
        (asHomogeneousIdeal
          (↑((Opens.infLERight
                    (((Opens.comap (ProjectiveSpectrum.comap f hf) :
                          FrameHom.{u_1, u_2} (Opens (ProjectiveSpectrum 𝒜)) (Opens (ProjectiveSpectrum ℬ))) :
                        (a : Opens (ProjectiveSpectrum 𝒜)) → Opens (ProjectiveSpectrum ℬ))
                      W)
                    V :
                  (a :
                      ↥((Opens.comap (ProjectiveSpectrum.comap f hf) :
                              (a : Opens (ProjectiveSpectrum 𝒜)) → Opens (ProjectiveSpectrum ℬ))
                            W ⊓
                          V)) →
                    ↥V)
                (Subtype.mk (p := fun (x : (↑(top ℬ) : Type u_2)) ↦
                  Membership.mem (γ := Opens (↑(top ℬ) : Type u_2))
                    (((Opens.comap (ProjectiveSpectrum.comap f hf) :
                              FrameHom.{u_1, u_2} (Opens (ProjectiveSpectrum 𝒜)) (Opens (ProjectiveSpectrum ℬ))) :
                            (a : Opens (ProjectiveSpectrum 𝒜)) → Opens (ProjectiveSpectrum ℬ))
                          W ⊓
                        V :
                      Opens (↑(top ℬ) : Type u_2))
                    x)
                  q sorry)) :
            ProjectiveSpectrum ℬ)))))
  (val.{0, u_2, u_5} (ι := ℕ) (σ := τ) (𝒜 := ℬ)
    ((fun
          (x :
            ↥(((Opens.comap (ProjectiveSpectrum.comap f hf) :
                        FrameHom.{u_1, u_2} (Opens (ProjectiveSpectrum 𝒜)) (Opens (ProjectiveSpectrum ℬ))) :
                      (a : Opens (ProjectiveSpectrum 𝒜)) → Opens (ProjectiveSpectrum ℬ))
                    W ⊓
                  V :
                Opens (↑(top ℬ) : Type u_2))) ↦
        (comapStructureSheafFun f hf U V hUV s
            ((Opens.infLERight
                  (((Opens.comap (ProjectiveSpectrum.comap f hf) :
                        FrameHom.{u_1, u_2} (Opens (ProjectiveSpectrum 𝒜)) (Opens (ProjectiveSpectrum ℬ))) :
                      (a : Opens (ProjectiveSpectrum 𝒜)) → Opens (ProjectiveSpectrum ℬ))
                    W)
                  V :
                (a :
                    ↥((Opens.comap (ProjectiveSpectrum.comap f hf) :
                            (a : Opens (ProjectiveSpectrum 𝒜)) → Opens (ProjectiveSpectrum ℬ))
                          W ⊓
                        V)) →
                  ↥V)
              x) :
          AtPrime ℬ
            (HomogeneousSubmodule.toSubmodule.{0, 0, u_5, u_5, u_2, u_2} (σA := τ) (𝒜 := ℬ)
              (asHomogeneousIdeal
                (↑((Opens.infLERight
                          (((Opens.comap (ProjectiveSpectrum.comap f hf) :
                                FrameHom.{u_1, u_2} (Opens (ProjectiveSpectrum 𝒜)) (Opens (ProjectiveSpectrum ℬ))) :
                              (a : Opens (ProjectiveSpectrum 𝒜)) → Opens (ProjectiveSpectrum ℬ))
                            W)
                          V :
                        (a :
                            ↥((Opens.comap (ProjectiveSpectrum.comap f hf) :
                                    (a : Opens (ProjectiveSpectrum 𝒜)) → Opens (ProjectiveSpectrum ℬ))
                                  W ⊓
                                V)) →
                          ↥V)
                      x) :
                  ProjectiveSpectrum ℬ)))))
      (Subtype.mk (p := fun (x : (↑(top ℬ) : Type u_2)) ↦
        Membership.mem (γ := Opens (↑(top ℬ) : Type u_2))
          (((Opens.comap (ProjectiveSpectrum.comap f hf) :
                    FrameHom.{u_1, u_2} (Opens (ProjectiveSpectrum 𝒜)) (Opens (ProjectiveSpectrum ℬ))) :
                  (a : Opens (ProjectiveSpectrum 𝒜)) → Opens (ProjectiveSpectrum ℬ))
                W ⊓
              V :
            Opens (↑(top ℬ) : Type u_2))
          x)
        q sorry)))
  (val.{0, u_2, u_5} (σ := τ) (𝒜 := ℬ)
    (HomogeneousLocalization.mk
      { deg := i, num := ((f.gradedAddHom i : AddMonoidHom.{u_1, u_2} ↥(𝒜 i) ↥(ℬ i)) : (a : ↥(𝒜 i)) → ↥(ℬ i)) a,
        den := ((f.gradedAddHom i : AddMonoidHom.{u_1, u_2} ↥(𝒜 i) ↥(ℬ i)) : (a : ↥(𝒜 i)) → ↥(ℬ i)) b, den_mem := sorry }))
Tactic: ext