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:
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?