Erdős Problem 1176

Reference: erdosproblems.com/1176

theorem Erdos1176.erdos_1176 : sorry ↔ ∀ {V : Type u_1} (G : SimpleGraph V), G.chromaticCardinal = Cardinal.aleph 1 → ∃ (EColor : Type) (_ : Cardinal.mk EColor = Cardinal.aleph 1) (c_edge : ↑G.edgeSet → EColor), ∀ (VColor : Type), Cardinal.mk VColor ≤ Cardinal.aleph 0 → ∀ (c_vert : V → VColor), ∃ (vc : VColor), ∀ (ec : EColor), ∃ (u : V) (v : V) (h : G.Adj u v), c_vert u = vc ∧ c_vert v = vc ∧ c_edge ⟨s(u, v), h⟩ = ec

Let $G$ be a graph with chromatic number $\aleph_1$. Is it true that there is a colouring of the edges with $\aleph_1$ many colours such that, in any countable colouring of the vertices, there exists a vertex colour containing all edge colours?

A problem of Erdős, Galvin, and Hajnal. The consistency of this was proved by Hajnal and Komjáth.