This isn't particularly down-to-earth, but of course before February or March you had the situation where DHJ (which can be phrased in completely finitary language) was only provable via ergodic-theory methods (which are infinitary.)