-- Module: Mathlib.AlgebraicGeometry.Spec
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
            (CommRingCat.ofHom
                (comap (CommRingCat.Hom.hom (f ≫ g)) (unop (op U))
                  ((TopologicalSpace.Opens.map (topMap (f ≫ g))).obj (unop (op U))) ⋯) ≫
              𝟙
                ((sheafedSpaceObj T).presheaf.obj
                  ((TopologicalSpace.Opens.map (sheafedSpaceMap (f ≫ g)).hom.base).op.obj (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))
    ((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))
⊢ Eq (α :=
    (↑(((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 (f ≫ g)) (unop (op U))
                  ((TopologicalSpace.Opens.map (topMap (f ≫ g))).obj (unop (op U))) ⋯) ≫
              (sheafedSpaceObj T).presheaf.map
                (NatTrans.app (𝟙 (TopologicalSpace.Opens.map (sheafedSpaceMap (f ≫ g)).hom.base).op) (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))
    ((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))

Tactic:
erw [(sheafedSpaceObj T).presheaf.map_id]

Premises used: CategoryTheory.Functor.map_id, AlgebraicGeometry.PresheafedSpace.presheaf, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, AlgebraicGeometry.Spec.sheafedSpaceObj