∀ {C : Type u} [inst : SizeOf C] (X : CategoryTheory.FreeMonoidalCategory C)
  {Y₁ Y₂ : CategoryTheory.FreeMonoidalCategory C} (f : Y₁.Hom Y₂),
  sizeOf (CategoryTheory.FreeMonoidalCategory.Hom.whiskerLeft X f) = 1 + sizeOf X + sizeOf Y₁ + sizeOf Y₂ + sizeOf f