-- 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
h :
  ∀ (x : ↥(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
                  (↑1 :
                    (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) =
      val.{0, u_2, u_5} (ι := ℕ) (σ := τ) (𝒜 := ℬ)
        ((↑1 :
            (x : ↥(Opposite.unop (Opposite.op V))) →
              (fun (x : (↑(top ℬ) : Type u_2)) ↦ AtPrime ℬ x.asHomogeneousIdeal.toIdeal) (↑x : (↑(top ℬ) : Type u_2)))
          x)
⊢ 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
        (↑1 :
          (x : ↥(Opposite.unop (Opposite.op U))) →
            (fun (x : (↑(top 𝒜) : Type u_1)) ↦ AtPrime 𝒜 x.asHomogeneousIdeal.toIdeal) (↑x : (↑(top 𝒜) : Type u_1))))
      ⋯ =
    1

Tactic:
ext