I think your examples illustrate each of my first two points perfectly. I don't think I've ever seen such a long and laborious proof for the binomial theorem as that in the second example. The two proofs are the same, of course (sometimes there exist several different ways to prove the same thing), the second is just way more explicit (also the first is missing equations 4.1 and 4.2, which are integrated into the second proof, making the first proof artificially shorter and artificially less comprehensible).
As to my second point, it seems pretty obvious to me that the goal of the second proof is to teach mathematical induction to people who are still struggling with basic arithmetic, not principally to prove the binomial theorem, since it includes weird things like putting "inductive hypothesis" and "inductive conclusion" in quotes, and he even writes in long hand that multiplication distributes over addition, i.e. that a(x+y) = ax + ay. Until one has internalised these basic arithmetic operations of course you're going to struggle with induction and the binomial theorem, and you're going to prefer to have examples where everything is spelled out in detail. And that's fine! But if you have internalised those details, making them explicit really does get in the way. Really. The core of the proof of the binomial theorem (which is to say, the reason why it's true) is the first proof you gave; but the second proof completely obscures that behind a haze of mechanical arithmetic manipulation and pattern-matching.
So, if you find the second proof clearer and/or more appropriate (which is fine!), all that says is that you are "in phase" with that material, it does not necessarily make one better than the other or more appropriate than the other in any other context or for anyone else. If students are having trouble with basic arithmetic manipulation, just don't force them to learn harder stuff until that's sorted out. They have to be ready for it. It is a good and happy thing that you have found material with which you are "in phase"; as I said last time, this is often very difficult. Please stop blaming your difficulties on the material when the problem is that you're using inappropriate material. Thanks! :)
I am OP's "friend who is a maths PhD". I'd just like to expand Grovulent's version of my position a bit to make it a little more convincing. To my mind, all of the problems are explained by the following three things:
1) Echoing vlasev [1], I think a very good analogy of the relation between proofs in mathematical logic and proofs in "normal" mathematics is that of the difference between programming in assembly (portability issues notwithstanding, though mathematical logic is probably a friendly RISC arch) and programming in a dense high-level language like Haskell. The productivity gain from using the high-level language, that permits skipping all those pesky unimportant details, is astronomical, and no amount of complaining from people who find Haskell hard to grok is going to stop us using it. (Drink the Koolaide, my friend, drink it up!) I think it is uncontroversial that this be true for research mathematics, but of course we don't want to just throw students in the deep end, which is why the education system attempts to build this knowledge gradually, which leads me to...
2) More practically, I think most peoples' problems learning mathematics come from (if you'll forgive a mathematical metaphor!) the person being out of phase with the material. This is subtler than what Grovulent described. Excellent material exists for all stages of one's mathematical development, of this I am certain; the hard part is ensuring that one is using material that is hard enough to be challenging, but not so hard as to be crushingly incomprehensible. This goes for people doing research in mathematics as well as people being introduced to calculus for the first time, and is very difficult to know when you are the student in question. We generally rely on the education system and expert advice to match students to the appropriate material, and clearly the system doesn't always work very well given how many people are out-of-phase with the material in front of them. In general, most mathematicians love talking about mathematics, and the love teaching it too! They love helping people understand and appreciate this marvel of human ingenuity. Just browse Math.SE[2] and Mathoverflow[3] for a while if you don't believe me.
3) Finally, an additional element is that many people expect to be able to learn mathematics quite easily without much or any deep reflection, because that's how they've always learned things in the past. But you simply can't learn mathematics like that, and you'll be disappointed and frustrated if you try to. (I certainly concede that mathematicians could do a better job of warning students about this.) Learning mathematics involves being in an almost constant state of uncertainty, and of making many, many mistakes, often in front of many other people, and being comfortable with all that. This is a state of affairs that many people find disconcerting, and there's nothing mathematicians can do about that bar suggesting that the student chill out and try not to let their ego get in the way of their education.
As to my second point, it seems pretty obvious to me that the goal of the second proof is to teach mathematical induction to people who are still struggling with basic arithmetic, not principally to prove the binomial theorem, since it includes weird things like putting "inductive hypothesis" and "inductive conclusion" in quotes, and he even writes in long hand that multiplication distributes over addition, i.e. that a(x+y) = ax + ay. Until one has internalised these basic arithmetic operations of course you're going to struggle with induction and the binomial theorem, and you're going to prefer to have examples where everything is spelled out in detail. And that's fine! But if you have internalised those details, making them explicit really does get in the way. Really. The core of the proof of the binomial theorem (which is to say, the reason why it's true) is the first proof you gave; but the second proof completely obscures that behind a haze of mechanical arithmetic manipulation and pattern-matching.
So, if you find the second proof clearer and/or more appropriate (which is fine!), all that says is that you are "in phase" with that material, it does not necessarily make one better than the other or more appropriate than the other in any other context or for anyone else. If students are having trouble with basic arithmetic manipulation, just don't force them to learn harder stuff until that's sorted out. They have to be ready for it. It is a good and happy thing that you have found material with which you are "in phase"; as I said last time, this is often very difficult. Please stop blaming your difficulties on the material when the problem is that you're using inappropriate material. Thanks! :)