The <a href="https://en.wikipedia.org/wiki/Alternating_sign_matrix#Alternating_sign_matrix_conjecture">alternating sign matrix conjecture</a> was first proved by Doron Zeilberger; the proof was enormously computational. Later, Greg Kuperberg gave a much shorter proof using results from statistical mechanics. Kuperberg's proof is still not trivial, but it is more conceptual. (It's worth mentioning that very recently, Fischer and Konvalinka have announced a <a href="https://arxiv.org/abs/1912.01354">bijective proof</a> of the same theorem, which is pleasing to a combinatorialist, but far from trivial, and hence probably not an answer to the question.)