-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Spec (goal)
Goal:
R S T : CommRingCat
f : R ⟶ S
g : S ⟶ T
U : TopologicalSpace.Opens (↑(↑(sheafedSpaceObj R).toPresheafedSpace : TopCat) : Type u)
x : (↑((sheafedSpaceObj R).presheaf.obj (op U)) : Type u)
h :
  Eq (α :=
    (↑(((TopologicalSpace.Opens.map (sheafedSpaceMap g ≫ sheafedSpaceMap f).hom.base).op ⋙
              (sheafedSpaceObj T).presheaf).obj
          (op U)) :
      Type u))
    ((CommRingCat.Hom.hom
            (𝟙
              ((sheafedSpaceObj T).presheaf.obj
                ((TopologicalSpace.Opens.map (sheafedSpaceMap (f ≫ g)).hom.base).op.obj (op U)))) :
          (a :
              (↑(((TopCat.Presheaf.pushforward CommRingCat (sheafedSpaceMap (f ≫ g)).hom.base).obj
                        (sheafedSpaceObj T).presheaf).obj
                    (op U)) :
                Type u)) →
            (↑(((TopologicalSpace.Opens.map (sheafedSpaceMap g ≫ sheafedSpaceMap f).hom.base).op ⋙
                      (sheafedSpaceObj T).presheaf).obj
                  (op U)) :
              Type u))
        ((CommRingCat.Hom.hom
              (CommRingCat.ofHom
                (RingHom.comp
                  (comap (CommRingCat.Hom.hom g)
                    (unop ((TopologicalSpace.Opens.map (sheafedSpaceMap f).hom.base).op.obj (op U)))
                    ((TopologicalSpace.Opens.map (topMap (f ≫ g))).obj U) ⋯)
                  (comap (CommRingCat.Hom.hom f) U
                    (unop ((TopologicalSpace.Opens.map (sheafedSpaceMap f).hom.base).op.obj (op U))) ⋯))) :
            (a : (↑((sheafedSpaceObj R).presheaf.obj (op U)) : Type u)) →
              (↑(((TopCat.Presheaf.pushforward CommRingCat (sheafedSpaceMap (f ≫ g)).hom.base).obj
                        (sheafedSpaceObj T).presheaf).obj
                    (op U)) :
                Type u))
          x) :
      (↑(((TopologicalSpace.Opens.map (sheafedSpaceMap g ≫ sheafedSpaceMap f).hom.base).op ⋙
                (sheafedSpaceObj T).presheaf).obj
            (op U)) :
        Type u))
    ((CommRingCat.Hom.hom ((sheafedSpaceMap g ≫ sheafedSpaceMap f).hom.c.app (op U)) :
          (a : (↑((sheafedSpaceObj R).presheaf.obj (op U)) : Type u)) →
            (↑(((TopologicalSpace.Opens.map (sheafedSpaceMap g ≫ sheafedSpaceMap f).hom.base).op ⋙
                      (sheafedSpaceObj T).presheaf).obj
                  (op U)) :
              Type u))
        x :
      (↑(((TopologicalSpace.Opens.map (sheafedSpaceMap g ≫ sheafedSpaceMap f).hom.base).op ⋙
                (sheafedSpaceObj T).presheaf).obj
            (op U)) :
        Type u))
h₁ : TopologicalSpace.Opens (↑(PrimeSpectrum.Top (↑S : Type u)) : Type u)
h₂ :
  ∀ p ∈ unop ((TopologicalSpace.Opens.map (sheafedSpaceMap f).hom.base).op.obj (op U)),
    PrimeSpectrum.comap (CommRingCat.Hom.hom f) p ∈ U
⊢ Eq (α :=
    (↑(((TopologicalSpace.Opens.map (sheafedSpaceMap g ≫ sheafedSpaceMap f).hom.base).op ⋙
              (sheafedSpaceObj T).presheaf).obj
          (op U)) :
      Type u))
    ((CommRingCat.Hom.hom
            (𝟙
              ((sheafedSpaceObj T).presheaf.obj
                ((TopologicalSpace.Opens.map (sheafedSpaceMap (f ≫ g)).hom.base).op.obj (op U)))) :
          (a :
              (↑(((TopCat.Presheaf.pushforward CommRingCat (sheafedSpaceMap (f ≫ g)).hom.base).obj
                        (sheafedSpaceObj T).presheaf).obj
                    (op U)) :
                Type u)) →
            (↑(((TopologicalSpace.Opens.map (sheafedSpaceMap g ≫ sheafedSpaceMap f).hom.base).op ⋙
                      (sheafedSpaceObj T).presheaf).obj
                  (op U)) :
              Type u))
        ((CommRingCat.Hom.hom
              (CommRingCat.ofHom
                (comap ((CommRingCat.Hom.hom g).comp (CommRingCat.Hom.hom f)) U
                  ((TopologicalSpace.Opens.map (topMap (f ≫ g))).obj U) ⋯)) :
            (a : (↑((sheafedSpaceObj R).presheaf.obj (op U)) : Type u)) →
              (↑(((TopCat.Presheaf.pushforward CommRingCat (sheafedSpaceMap (f ≫ g)).hom.base).obj
                        (sheafedSpaceObj T).presheaf).obj
                    (op U)) :
                Type u))
          x) :
      (↑(((TopologicalSpace.Opens.map (sheafedSpaceMap g ≫ sheafedSpaceMap f).hom.base).op ⋙
                (sheafedSpaceObj T).presheaf).obj
            (op U)) :
        Type u))
    ((CommRingCat.Hom.hom ((sheafedSpaceMap g ≫ sheafedSpaceMap f).hom.c.app (op U)) :
          (a : (↑((sheafedSpaceObj R).presheaf.obj (op U)) : Type u)) →
            (↑(((TopologicalSpace.Opens.map (sheafedSpaceMap g ≫ sheafedSpaceMap f).hom.base).op ⋙
                      (sheafedSpaceObj T).presheaf).obj
                  (op U)) :
              Type u))
        x :
      (↑(((TopologicalSpace.Opens.map (sheafedSpaceMap g ≫ sheafedSpaceMap f).hom.base).op ⋙
                (sheafedSpaceObj T).presheaf).obj
            (op U)) :
        Type u))
have h₃ : ∀ p ∈ (TopologicalSpace.Opens.map (topMap (f ≫ g))).obj U,
  PrimeSpectrum.comap (CommRingCat.Hom.hom g) p ∈
    unop ((TopologicalSpace.Opens.map (sheafedSpaceMap f).hom.base).op.obj (op U))
Tactic: rw [comap_comp]