I never heard anyone claim the existence of a forcing proof of the Erdős-Rado theorem. On the other hand, yes, there are several proofs of nonindependence statements that use forcing.
One is Shelah's proof for the existence of a finite K4-free graph which, when the edges colored by 2 colors, always contains a monocolored triangle (a problem of Erdős and Hajnal). Here is the argument. He constructs a forcing extension which adds a graph X with the same property but with ℵ0 colors (this is not easy). Obviously, X has the edge-coloring property for 2 colors, as well. X must contain a finite subgraph Y with the same property. This is compactness, or, any proof for the Erdős-de Bruijn theorem gives it. As forcing cannot create new finite graphs, Y is already present in the underlying model. That is, there is a finite graph as required in any countable, transitive model of a sufficiently large part of ZFC. By Gödel, this is only possible, if ZFC proves that there is such a graph.
Another example is the original proof of the Baumgartner-Hajnal theorem: ω1→(α)2k if α<ω1, k<ω. They first deduced it from Martin's axiom, then a specific argument gives that if it holds in a cardinal preserving extension, then it holds in the original model. Therefore, it holds in every countable, transitive model of a sufficiently large fragment of ZFC, and we can finish as above.