-- Module: Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
σ : Type u_4
τ : Type u_5
ψ : Type u_6
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 : CommRing C
inst_7 : SetLike ψ C
inst_8 : AddSubgroupClass ψ C
𝒜 : ℕ → σ
ℬ : ℕ → τ
𝒞 : ℕ → ψ
inst_9 : GradedRing 𝒜
inst_10 : GradedRing ℬ
inst_11 : GradedRing 𝒞
f : 𝒜 →+*ᵍ ℬ
g : ℬ →+*ᵍ 𝒞
hf : LE.le (α := HomogeneousIdeal ℬ) (ℬ₊) (HomogeneousIdeal.map f (𝒜₊))
hg : LE.le (α := HomogeneousIdeal 𝒞) (𝒞₊) (HomogeneousIdeal.map g (ℬ₊))
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
x y :
  (↑(Functor.obj
        (ObjectProperty.FullSubcategory.obj (P :=
            (Presheaf.IsSheaf (Opens.grothendieckTopology (↑(top 𝒜) : Type u_1)) :
              (P : (Opens (↑(top 𝒜) : Type u_1))ᵒᵖ ⥤ CommRingCat) → Prop))
            (structureSheaf 𝒜 : TopCat.Sheaf CommRingCat (top 𝒜)) :
          (Opens (↑(top 𝒜) : Type u_1))ᵒᵖ ⥤ CommRingCat)
        (Opposite.op U)) :
    Type u_1)
x_1 : ↥(Opposite.unop (Opposite.op V))
⊢ val
      ((↑(Subtype.mk (p :=
              fun
                (f :
                  (x : ↥(Opposite.unop (Opposite.op V))) →
                    (fun (x : (↑(top ℬ) : Type u_2)) ↦ AtPrime ℬ x.asHomogeneousIdeal.toIdeal)
                      (↑x : (↑(top ℬ) : Type u_2))) ↦
              TopCat.PrelocalPredicate.pred (X := top ℬ) (T := fun (x : (↑(top ℬ) : Type u_2)) ↦
                AtPrime ℬ x.asHomogeneousIdeal.toIdeal)
                (TopCat.LocalPredicate.toPrelocalPredicate (T := fun (x : (↑(top ℬ) : Type u_2)) ↦
                    AtPrime ℬ x.asHomogeneousIdeal.toIdeal) (ProjectiveSpectrum.StructureSheaf.isLocallyFraction ℬ) :
                  TopCat.PrelocalPredicate (X := top ℬ) fun (x : (↑(top ℬ) : Type u_2)) ↦
                    AtPrime ℬ x.asHomogeneousIdeal.toIdeal)
                f)
              (comapStructureSheafFun f hf U (Opposite.unop (Opposite.op V)) hUV
                (↑(x * y) :
                  (x : ↥(Opposite.unop (Opposite.op U))) →
                    (fun (x : (↑(top 𝒜) : Type u_1)) ↦ AtPrime 𝒜 x.asHomogeneousIdeal.toIdeal)
                      (↑x : (↑(top 𝒜) : Type u_1))))
              ⋯) :
          (x : ↥(Opposite.unop (Opposite.op V))) →
            (fun (x : (↑(top ℬ) : Type u_2)) ↦ AtPrime ℬ x.asHomogeneousIdeal.toIdeal) (↑x : (↑(top ℬ) : Type u_2)))
        x_1) =
    val
      ((↑(Subtype.mk (p :=
                fun
                  (f :
                    (x : ↥(Opposite.unop (Opposite.op V))) →
                      (fun (x : (↑(top ℬ) : Type u_2)) ↦ AtPrime ℬ x.asHomogeneousIdeal.toIdeal)
                        (↑x : (↑(top ℬ) : Type u_2))) ↦
                TopCat.PrelocalPredicate.pred (X := top ℬ) (T := fun (x : (↑(top ℬ) : Type u_2)) ↦
                  AtPrime ℬ x.asHomogeneousIdeal.toIdeal)
                  (TopCat.LocalPredicate.toPrelocalPredicate (T := fun (x : (↑(top ℬ) : Type u_2)) ↦
                      AtPrime ℬ x.asHomogeneousIdeal.toIdeal) (ProjectiveSpectrum.StructureSheaf.isLocallyFraction ℬ) :
                    TopCat.PrelocalPredicate (X := top ℬ) fun (x : (↑(top ℬ) : Type u_2)) ↦
                      AtPrime ℬ x.asHomogeneousIdeal.toIdeal)
                  f)
                (comapStructureSheafFun f hf U (Opposite.unop (Opposite.op V)) hUV
                  (↑x :
                    (x : ↥(Opposite.unop (Opposite.op U))) →
                      (fun (x : (↑(top 𝒜) : Type u_1)) ↦ AtPrime 𝒜 x.asHomogeneousIdeal.toIdeal)
                        (↑x : (↑(top 𝒜) : Type u_1))))
                ⋯ *
              Subtype.mk (p :=
                fun
                  (f :
                    (x : ↥(Opposite.unop (Opposite.op V))) →
                      (fun (x : (↑(top ℬ) : Type u_2)) ↦ AtPrime ℬ x.asHomogeneousIdeal.toIdeal)
                        (↑x : (↑(top ℬ) : Type u_2))) ↦
                TopCat.PrelocalPredicate.pred (X := top ℬ) (T := fun (x : (↑(top ℬ) : Type u_2)) ↦
                  AtPrime ℬ x.asHomogeneousIdeal.toIdeal)
                  (TopCat.LocalPredicate.toPrelocalPredicate (T := fun (x : (↑(top ℬ) : Type u_2)) ↦
                      AtPrime ℬ x.asHomogeneousIdeal.toIdeal) (ProjectiveSpectrum.StructureSheaf.isLocallyFraction ℬ) :
                    TopCat.PrelocalPredicate (X := top ℬ) fun (x : (↑(top ℬ) : Type u_2)) ↦
                      AtPrime ℬ x.asHomogeneousIdeal.toIdeal)
                  f)
                (comapStructureSheafFun f hf U (Opposite.unop (Opposite.op V)) hUV
                  (↑y :
                    (x : ↥(Opposite.unop (Opposite.op U))) →
                      (fun (x : (↑(top 𝒜) : Type u_1)) ↦ AtPrime 𝒜 x.asHomogeneousIdeal.toIdeal)
                        (↑x : (↑(top 𝒜) : Type u_1))))
                ⋯) :
          (x : ↥(Opposite.unop (Opposite.op V))) →
            (fun (x : (↑(top ℬ) : Type u_2)) ↦ AtPrime ℬ x.asHomogeneousIdeal.toIdeal) (↑x : (↑(top ℬ) : Type u_2)))
        x_1)

Tactic:
simp [comapStructureSheafFun]

Premises used: AlgebraicGeometry.Proj.comapStructureSheafFun