My example is perhaps not exactly what you had in mind, but I hope that will make it more interesting, thus my reason for posting it. I thought of mentioning the (very elementary) but delightfully clever method of proving polynomials equal by comparing them evaluated at finitely many points (which is applied in, for example in A Proof in the Spirit of Zeilberger of an Amazing Identity of Ramanujan) but instead I thought I would point out the notion of reflective proof from dependent type theory:

To write a formal (computer checkable proof) you must justify every single step of reasoning all the way down to the axioms of the foundation. Of course that would make proving simple things like $((ab)cd)e = a(bc)(de)$ a terrible chore requiring repeated applications of the associativity (infact proving something as simple as $1 + 100 = 101$ could require $100$ applications of the definition of plus!). The idea of reflection is to reduce trivial reasoning steps to computation, This is described in Section 4 of Henk Barendregt's Proofs of correctness in Mathematics and Industry, but it was also applied heavily in a recent formal proof of the four color theorem.