∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) {Z : AlgebraicGeometry.Scheme} (g : Y ⟶ Z) [AlgebraicGeometry.Smooth f]
  [AlgebraicGeometry.Smooth g], AlgebraicGeometry.Smooth (CategoryTheory.CategoryStruct.comp f g)