-- 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
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)
⊢ 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))))
      ⋯ =
    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))))
        ⋯
have h : ∀ (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))))
              sorry) :
          (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))))
                sorry +
              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))))
                sorry) :
          (x : ↥(Opposite.unop (Opposite.op V))) →
            (fun (x : (↑(top ℬ) : Type u_2)) ↦ AtPrime ℬ x.asHomogeneousIdeal.toIdeal) (↑x : (↑(top ℬ) : Type u_2)))
        x_1)
Tactic: ext