symmetric models and HOD Cohen's first non-AC model, the one with a Dedekind-finite infinite set $A$ of reals, can be defined in two ways, 1st, as $HOD(A)$ in a bigger generic model of ZFC (the one obtained as a generic extension of $L$ via the countable product of the Cohen forcing), and 2nd, via symmetric names. Jech notes in one of his books that both methods yield exactly same models. I wonder is there any consistent proof somewhere as a source of reference? 
 A: You might want to look at Grigorieff's paper which shows that every symmetric model is of the form $\mathrm{HOD}(V\cup X)^{V[G]}$, where $X\in V[G]$.
In the case of Cohen's model, it is easy to argue that $\mathrm{HOD}(A)$ is a submodel of the symmetric extension. From Grigorieff's paper you can extract (although not without difficulty) the needed information to get that this is exactly the symmetric model.

Grigorieff, Serge, Intermediate submodels and generic extensions in set theory, Ann. Math. (2) 101, 447-490 (1975). ZBL0308.02060.

(Essentially the idea is that you have a set of generators, and the groups which stabilize them form a basis for the filter of subgroups; then the ordinal is used to "choose a name" and give some sort of "partial interpretation". So in the case of Cohen's model, this would be fixing finitely many reals.)
I can offer another route, though, since we start over $L$ and the Cohen forcing is homogeneous, you might as well consider this as $L(A)$ instead. That would be the Halpern-Levy model, which one can show even "more by hand" that it is equivalent to the symmetric extension. Simply because every $x$ in $L(A)$ is definable from some finitely many elements of $A$, and $A$ itself. And that just tells you what is the support and the name in the symmetric extension.
This is [very] implicit in Jech's proof of the fact the model is linearly ordered in his Axiom of Choice book (Ch. 5), and in many papers of Gordon P. Monro, and others from that era (e.g. Felgner's book and more).
