Is Leray's theorem on commutative Hopf algebras proven in Milnor-Moore? 
Question 1. Is a correct proof of Leray's theorem (the one that says that
  a connected graded Hopf algebra $H$ over a field of characteristic $0$ is
  isomorphic as an algebra to the symmetric algebra $\operatorname*{Sym}\left(
H^{+}/\left(  H^{+}\right)  ^{2}\right)  $, where $H^{+}=\operatorname*{Ker}
\epsilon$ is the kernel of the counit $\epsilon$ of $H$) contained in
  any version of the famous article "On the structure of Hopf algebras" by
  Milnor and Moore?
Question 2. What are the currently existing sources for Leray's theorem?


Detailed version. One of the earliest, and still most influential, papers
on Hopf algebras is the article "On the structure of Hopf algebras" by Milnor
and Moore. It exists in two versions:
[A] John W. Milnor, John C. Moore, On the structure of Hopf algebras
(preprint), reprinted in Milnor's Collected Papers.
[B] John W. Milnor, John C. Moore, On the structure of Hopf algebras, The
Annals of Mathematics, Second Series, Vol. 81, No. 2 (Mar., 1965), pp. 211--264.
I am interested in the following theorem, which I shall call Leray's theorem
despite being utterly confused about its provenance (possibly Hopf, Samelson
and Borel have some claims here as well -- any help with the history?):

Leray's theorem. Let $\mathbf{k}$ be a commutative $\mathbb{Q}$-algebra.
  Let $H$ be a graded Hopf algebra over $\mathbf{k}$ (in the modern meaning of
  this word -- i.e., it has to have an associative multiplication $m$, a unit
  $u$, a coassociative comultiplication $\Delta$, a counit $\epsilon$, and an
  antipode $S$; and all these maps are graded). Assume that $H$ is connected
  (i.e., the $0$-th graded component of $H$ is isomorphic to $\mathbf{k}$) and
  commutative (i.e., all $a,b\in H$ satisfy $ab=ba$). Let $H^{+}
=\operatorname*{Ker}\epsilon$ be the kernel of the counit $\epsilon
:H\rightarrow\mathbf{k}$ of $H$. Then, $H\cong\operatorname*{Sym}\left(
H^{+}/\left(  H^{+}\right)  ^{2}\right)  $ as graded $\mathbf{k}$-algebras.

From what I understand, Milnor and Moore claim to prove this theorem in the
particular case when $\mathbf{k}$ is a field. Specifically, it appears to
follow from Theorem 4.6 in [A] and from Theorem 7.5 in [B].
(Notice that the notations in [A] are different from mine. In particular,
associativity and coassociativity are not required by default from Hopf
algebras, but rather required only when explicitly stated. If they wouldn't
require $\mathbf{k}$ to be a field, their results would hence be more general
than what I call Leray's theorem. Also notice that they are using the
notations $I\left(  H\right)  $ for $H^{+}$, as well as $Q\left(  H\right)  $
for $\mathbf{k}\otimes_{H}H^{+}\cong H^{+}/\left(  H^{+}\right)  ^{2}$, and
finally $A\left(  V\right)  $ for the symmetric algebra $\operatorname*{Sym}
V$, at least when we are working with evenly graded algebras.)
What I don't understand is how they prove all this. Their proof relies on a
lemma (Lemma 4.3 in [A], resp. Proposition 4.17 in [B]), which states (at
least in the particular case we care about) that in the situation of Leray's
theorem, if we further assume that $\mathbf{k}$ is a field, the natural
morphism $\left\{  \text{primitive elements of }H\right\}  \rightarrow
H^{+}/\left(  H^{+}\right)  ^{2}$ (which is well-defined since primitive
elements of $H$ always lie in $H^{+}$) is a monomorphism. In other words, the
only primitive element in $\left(  H^{+}\right)  ^{2}$ is $0$. The proof of
this lemma relies on some argument where $H$ is assumed to be finitely
generated, and then an induction is done on the number of generators,
presenting $H$ as a some-sort-of-extension of a Hopf subalgebra $A^{\prime}$
with one less generator by a quotient-of-sorts $A^{\prime\prime}$ with one
generator. ("Generator" always mean algebra generator.) This looks highly
suspicious to me, since I don't think that Hopf algebras can be deconstructed
in such a simple way. I also have never seen arguments like this ever after
Milnor's and Moore's work. Thus, the first question: Is it correct?
I am currently writing up my own proof of Leray's theorem, which uses the
Eulerian idempotent and is probably common knowledge in the Hopf-combinatorics
crowd. Thus, the second question: What should I be referencing?
 A: I forgot to give this question some closure. Basically, it was answered by @JohnPalmieri in his comment; let me just expand this answer.
The proof of Proposition 4.17 in the Milnor/Moore paper [B] is correct (at least the part that I was having troubles with). The argument is rather surprising and seriously uses the assumption that the base field is a field! Here are the main ideas (of the proof of Proposition 4.17, not of the proof of Leray's theorem):


*

*We want to prove that if $A$ is a commutative connected graded Hopf algebra over a field $K$ of characteristic $0$, then the natural morphism $P\left(A\right) \to Q\left(A\right)$ (where, we recall, $P\left(A\right)$ denotes the primitive elements of $A$, whereas $Q\left(A\right) = \left(\ker \varepsilon\right) / \left(\ker \varepsilon\right)^2$) is injective. (This is not the whole statement of Proposition 4.17, but the only part I care about here.)

*We can show that $A$ is a direct limit of Hopf subalgebras that are finitely generated as $K$-algebras. (This is the first place where we use that $K$ is a field.) So we WLOG assume that $A$ is finitely generated as a $K$-algebra (by abstract nonsense).

*Thus, $A = K\left[x_1, x_2, \ldots, x_{m+1}\right]$ for some homogeneous elements $x_1, x_2, \ldots, x_{m+1}$ of $A$ having positive degree. Assume WLOG that $x_{m+1}$ has the highest degree among these elements $x_1, x_2, \ldots, x_{m+1}$.

*Now, the $K$-subalgebra $A' := K\left[x_1, x_2, \ldots, x_m\right]$ of $A$ is a Hopf subalgebra. To see this, notice that the coproducts $\Delta x_i$ for $i \leq m$ all belong to $A' \otimes A'$ (because $\Delta x_i - x_i \otimes 1 - 1 \otimes x_i$ is a sum of tensors whose tensor factors have smaller degree than $x_i$, which entails that these factors cannot use $x_{m+1}$ because any appearance of $x_{m+1}$ would raise their degree higher than it can go).

*Now, the ideal of $A$ generated by all $a' - \varepsilon\left(a'\right)$ for $a' \in A'$ is a Hopf ideal of $A$, and therefore the quotient $A''$ of $A$ by this ideal is also a commutative Hopf algebra, with only one generator (the projection of $x_{m+1}$).

*By induction over the number of generators, we can assume that the proposition is already proven for $A'$ instead of $A$ (since $A'$ needs only $m$ generators $x_1, x_2, \ldots, x_m$). Also, it is easy to show that the proposition holds for $A''$ instead of $A$ (as $A''$ has only one generator). Splicing this together via an exact-sequence argument yields the proposition for $A$.
I have not gone through the details, but this looks like a nice argument which I haven't seen elsewhere.
Meanwhile, I prove different versions of Leray's theorem in different ways (based on ideas by Patras, Loday, etc.):


*

*If $K$ is any commutative $\mathbb{Q}$-algebra (not necessarily a field!), and if $A$ is a commutative connected graded $K$-Hopf algebra, then $A \cong \operatorname{Sym}\left(Q\left(A\right)\right)$ as algebras (where $Q\left(A\right) = \left(\ker \varepsilon\right) / \left(\ker \varepsilon\right)^2$ as before). This is (currently) Theorem 1.7.29 (e) in Darij Grinberg and Victor Reiner, Hopf algebras in Combinatorics (this will be on the arXiv soon, once I've added a few more things). Note that this version of Leray's theorem does not require $K$ to be a field, but (unlike Theorem 7.5 in [B]) only provides one isomorphism $\operatorname{Sym}\left(Q\left(A\right)\right) \to A$, whereas Theorem 7.5 in [B] gives an infinite family thereof. Roughly speaking, the isomorphism it provides comes from an "exponential of the Eulerian idempotent". Note also that (unlike Milnor and Moore) I only consider evenly graded algebras (i.e., no superalgebras), and I require coassociativity.

*In Theorem 40.13 of On the logarithm of the identity on
connected filtered bialgebras, I replicate the whole infinite family of isomorphisms from Theorem 7.5 of [B] (though still only for evenly graded algebras with coassociativity). The proof is a long and painful mess (although it doesn't help that I haven't tried much to streamline it, but written it up as it evolved). It seems that the generality of $K$ not being a field is cutting off many useful shortcuts here; the fieldness of $K$ is used in [B] many times (apart from the uses mentioned above, I think it is used in making $E^0\left(A\right)$ a Hopf algebra).
Note that I am still a bit skeptical about whether Theorem 7.5 in [B] really does not require the associativity and the coassociativity of $A$. I do not care much about this, but somehow it strikes me as more of a miracle than I would have expected -- then again, the Milnor/Moore paper has its share of miracles...
