At that point I'd start wondering why there doesn't appear to be a simple proof. For example, maybe some kind of generalization of the result is false and you need the complexity to "break the correspondence" with the generalization.