-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor
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
rcases :
  ∀ (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 := ⋯ })),
    ∃ (V_1 : Opens (↑(top ℬ) : Type u_2)) (_ :
      (↑(Subtype.mk (p := fun (x : (↑(top ℬ) : Type u_2)) ↦ x ∈ V) p hpV) : (↑(top ℬ) : Type u_2)) ∈ V_1) (i : V_1 ⟶ V),
      TopCat.PrelocalPredicate.pred (X := top ℬ) (T := fun (x : (↑(top ℬ) : Type u_2)) ↦
        AtPrime ℬ x.asHomogeneousIdeal.toIdeal)
        (ProjectiveSpectrum.StructureSheaf.isFractionPrelocal ℬ :
          TopCat.PrelocalPredicate (X := top ℬ) fun (x : (↑(top ℬ) : Type u_2)) ↦
            AtPrime ℬ x.asHomogeneousIdeal.toIdeal)
        (U := V_1) fun (x : ↥V_1) ↦
        (comapStructureSheafFun f hf U V hUV s ((i : (a : ↥V_1) → ↥V) x) :
          AtPrime ℬ
            (HomogeneousSubmodule.toSubmodule.{0, 0, u_5, u_5, u_2, u_2} (σA := τ) (𝒜 := ℬ)
              (asHomogeneousIdeal (↑((i : (a : ↥V_1) → ↥V) x) : ProjectiveSpectrum ℬ))))
⊢ ∃ (V_1 : Opens (↑(top ℬ) : Type u_2)) (_ :
    (↑(Subtype.mk (p := fun (x : (↑(top ℬ) : Type u_2)) ↦ x ∈ V) p hpV) : (↑(top ℬ) : Type u_2)) ∈ V_1) (i : V_1 ⟶ V),
    TopCat.PrelocalPredicate.pred (X := top ℬ) (T := fun (x : (↑(top ℬ) : Type u_2)) ↦
      AtPrime ℬ x.asHomogeneousIdeal.toIdeal)
      (ProjectiveSpectrum.StructureSheaf.isFractionPrelocal ℬ :
        TopCat.PrelocalPredicate (X := top ℬ) fun (x : (↑(top ℬ) : Type u_2)) ↦ AtPrime ℬ x.asHomogeneousIdeal.toIdeal)
      (U := V_1) fun (x : ↥V_1) ↦
      (comapStructureSheafFun f hf U V hUV s ((i : (a : ↥V_1) → ↥V) x) :
        AtPrime ℬ
          (HomogeneousSubmodule.toSubmodule.{0, 0, u_5, u_5, u_2, u_2} (σA := τ) (𝒜 := ℬ)
            (asHomogeneousIdeal (↑((i : (a : ↥V_1) → ↥V) x) : ProjectiveSpectrum ℬ))))

Tactic:
rcases hs ⟨.comap f hf p, hUV hpV⟩ with ⟨W, m, iWU, i, a, b, hb, h_frac⟩

Premises used: AlgebraicGeometry.ProjectiveSpectrum.comap, Subtype.mk, DFunLike.coe