-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor (goal)
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
⊢ 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
have 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))))
              sorry) :
          (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)
Tactic: ext