The following quote is by Matt Emerton (in a comment on MathOverflow)
I think there is a genuine tension between proofs that a professional will like (where professional here may mean professional algebraist!) and ones that are elementary. For professionals, reductions and devissages are easy, natural, and we don’t even think of them as real landmarks in the proof; they are just serve as passages between the key points and ideas. But in writing things out, they can take a lot of words, and seem (as you wrote) mysterious and difficult. I don’t know the best way to deal with this tension.
Interestingly, Matt posted it as part of a discussion about exactly what I wanted to talk about in this post, the teaching of the structure theorem for finitely generated abelian groups, or more generally, of finitely generated modules over a PID.
My personal connection is that I taught this as part of our third-year algebra course this year at the University of Melbourne, and am slated to do so again next year. I think that I did not do a particularly good job of teaching it in 2022, primarily because I got distracted by the reductions and devissages and tried to proceed along those lines as much as possible, when what I have learned is more appropriate for one of these courses is the more prosaic approach involving matrix manipulations. It is with the matrix manipulations (directly proving Smith Normal Form) that I plan to teach this part of the course in 2023 (and beyond, if necessary).
For completeness, allow me to state the professionals’ proof: Split off the quotient by the torsion subgroup to reduce to the torsion case. Then canonically decompose the module into a direct sum of its p-primary components. Then use the fact that is injective over itself to manually split the remaining short exact sequences needed to complete the classification.
While it may not be reasonable to expect a third-year student to follow this proof, I think it is fair to expect any PhD student of mine to be able to understand and execute this proof.