Explanatory vs Non-explanatory Proofs In a philosophical context, I’m currently thinking about how best to explicate mathematicians’ judgements that some correct proofs are ‘explanatory’ while others are not. In this vein, I’m trying to collect examples of theorems that have two salient proofs, one of which is judged to be explanatory whilst the other is not (even better if the examples exhibit strong disagreement regarding which proof is more explanatory). Other things being equal, simpler examples are preferred, and I’m especially interested in examples from abstract algebra, order theory and topology. Pointers towards relevant debates in the history of math would also be appreciated. 
(Disclaimer: this question is related to but distinct from the question below, which concerns the relationship between explanation and beauty in mathematical proof: An example of a proof that is explanatory but not beautiful? (or vice versa).)
 A: Paul Halmos once gave the following example in a talk for a general audience. Suppose there is a tennis tournament with 128 players. In the first round 64 of them are paired off with the other 64, they play their games, and all the losers are ejected from the tournament. In the next round the remaining 64 players are paired off and this time the 32 losers are ejected. Eventually one player is left, who wins the tournament. How many games were played in total?
The most obvious way to solve this is to add up 64 + 32 + ...  If you remember a formula about geometric series, you can find this sum quickly.
But the explanatory proof is different. Every player aside from the eventual winner loses exactly one game, the game in which they are ejected. So the total number of games = the total number of losers = 127.
A: Here is a related situation which may guide later posts: plant ten trees in five rows with four trees per row.
After pushing dots around on paper and realizing that every tree has to belong to two rows, one ends up with ten dots in a pentagram configuration, usually regular.  This is a solution, but does not yield much in the way of understanding.
If one instead pushes rows around, one finds many more solutions, since any arrangement of five lines in which no two are parallel (edit: and no three concurrent, oops) leads to another configuration. Then one sees that the problem is about incidence structures, and understands how to generalize the problem and solution set.
Gerhard "Really, It's In The Telling" Paseman, 2019.11.05.
A: This is a well-known and well-documented example: the first proof of the Alternating Sign Matrix theorem was a complicated, inductive "manipulation of generating function"-style argument by Zeilberger; shortly thereafter Kuperberg gave a shorter proof based on a connection to the six-vertex model of statistical mechanics and the Yang-Baxter equation. The history of the Alternating Sign Matrix conjecture is beautifully told in the book Proofs and Confirmations by Bressoud.
