∀ {R S : CommRingCat} (f : R ⟶ S),
  CategoryTheory.CategoryStruct.comp f (AlgebraicGeometry.Scheme.ΓSpecIso S).inv =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.ΓSpecIso R).inv
      (AlgebraicGeometry.Scheme.Hom.appTop (AlgebraicGeometry.Spec.map f))