It is often said that instead of proving a great theorem a mathematician's fondest dream is to prove a great lemma. Something like Kőnig's tree lemma, or Yoneda's lemma, or really anything from this list.
When I was first learning algebra, one of the key lemmas we were taught was Zorn's lemma. It was almost magical in its power and utility. However, I can't remember the last time Zorn's lemma appeared in one of my papers (even though I'm an algebraist). In pondering why this is, a few reasons occurred to me, which I'll list below. I don't want to lose my old friend Zorn, and so my question is:
What are some reasons to keep (or, perhaps in line with my thoughts, abandon) Zorn's lemma?
Edited to add: One purpose to this question is to know whether or not I should be rewriting my proofs to use Zorn's lemma, instead of my usual practice of using transfinite recursion, if there is a mathematical reason to prefer one over the other. Hopefully this clarifies the mathematical content of this question.
To motivate the discussion, let me give an example of how I would now teach ungraduates a result that was taught to me using Zorn's lemma.
Theorem: Every vector space $V$ has a basis.
Proof: First, fix a well-ordering for $V$. We will recursively work our way through the ordering, deciding whether to keep or discard elements of $V$. Suppose we have reached a vector $v$; we keep it if it is linearly independent from the previously kept vectors (equivalently, it is not in their span), otherwise we discard it. If $B$ is the set of kept vectors we see it is a basis as follows. Any vector $v\in V$ is in the span of $B$, because it is either in $B$ or in the span of the vectors previously kept. On the other hand, the elements of $B$ are linearly independent because a nontrivial combination $c_1 v_1 + \dotsb +c_k v_k=0$, where $v_1<v_2<\dotsb<v_k$ and $c_k\neq 0$ can be rearranged so $v_k$ is a linear combination of the previous vectors, so $v_k$ cannot belong to $B$ after all. $\quad\square$
Here are some of the benefits I see for this type of proof over the usual Zorn's lemma argument.
1. The use of choice is disentangled from the other parts of the proof.
When applying Zorn's lemma, it is difficult to see exactly how the axiom of choice is being used to reach the conclusion of a maximal element. One way to visualize its use is that Zorn's lemma lets us recursively build a maximal chain through the poset. This chain must have a greatest element. However, this construction is hidden behind the magic words "Abracadabra Zornify".
Is it a historical artifact that choice is hidden this way?
2. We can more easily see whether or not to use a choice principle.
In the proof above, if $V$ is already well-orderable (without AC), then we don't need to ever use the axiom of choice.
3. Zorn's lemma is no easier than transfinite recursion.
Each part of transfinite recursion already (implicitly) occurs in most Zorn's lemma arguments. The base case of the recursion corresponds, roughly, to showing that that the poset is nonempty (i.e., has some starting point). The successor ordinal step often occurs at the end; after asserting that some maximal element of the poset exists, we show that this maximal element has some claimed property by working by contradiction, and then passing to a slightly bigger element of the poset (i.e., the next successor). The limit ordinal step occurs when we show that chains have upper bounds.
4. Zorn's lemma often includes unnecessary complications.
In the proof I gave above, there is no need to define a complicated set, together with a poset relation. We can use strong induction, to avoid differentiating between the zero, successor, and nonzero limit steps. We don't need to combine the contradiction at the end with any successor step; they are entirely separated.
5. Transfinite recursion is a more fundamental principle.
As a matter of pedagogy, shouldn't we teach students about transfinite induction before we teach them a version of it that is also combined with AC, and that requires the construction of a complicated poset?
6. Transfinite recursion applies to situations where Zorn's lemma does not.
To give just one example: There are some recursions that continue along all of the ordinals (for a proper class amount of time). Zorn's requires, as a hypothesis, an end.