∀ {X Y Z T : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) (h : Z ⟶ T)
  {Z_1 : CategoryTheory.Functor T.Modules X.Modules}
  (h_1 :
    AlgebraicGeometry.Scheme.Modules.pullback
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g) h) ⟶
      Z_1),
  CategoryTheory.CategoryStruct.comp
      (AlgebraicGeometry.Scheme.Modules.pullbackComp f (CategoryTheory.CategoryStruct.comp g h)).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Functor.whiskerRight (AlgebraicGeometry.Scheme.Modules.pullbackComp g h).inv
          (AlgebraicGeometry.Scheme.Modules.pullback f))
        (CategoryTheory.CategoryStruct.comp
          ((AlgebraicGeometry.Scheme.Modules.pullback h).associator (AlgebraicGeometry.Scheme.Modules.pullback g)
              (AlgebraicGeometry.Scheme.Modules.pullback f)).hom
          (CategoryTheory.CategoryStruct.comp
            ((AlgebraicGeometry.Scheme.Modules.pullback h).whiskerLeft
              (AlgebraicGeometry.Scheme.Modules.pullbackComp f g).hom)
            (CategoryTheory.CategoryStruct.comp
              (AlgebraicGeometry.Scheme.Modules.pullbackComp (CategoryTheory.CategoryStruct.comp f g) h).hom h_1)))) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) h_1