Infinite graph ramsey

theorem infinite_graph_ramsey :    ∃ c : Color, ∃ s : Set Vertex, s.Infinite ∧      ∀ e : Finset Vertex, e.card = 2 → ↑e ⊆ s → color e = c := by  classical  obtain ⟨vs, v, c, h_sel⟩ := good_selections_exist color  simp only [forall_and] at h_sel  obtain ⟨h_vs, h_v, h_c⟩ := h_sel  have : ∀ m n, m < n → v n ∈ vs m := by    intro m n h_mn    suffices h1 : (⋂ m < n, vs m) ⊆ vs m by grind    exact biInter_subset_of_mem h_mn  obtain ⟨c', s', h_s'_inf, h_s'_col⟩ :      ∃ c' : Color, ∃ s' : Set ℕ, s'.Infinite ∧ ∀ n ∈ s', c n = c' := by    obtain ⟨c', s', h_s'_inf, _, h_s'col⟩ := infinite_pigeonhole_principle c infinite_univ    use c', s'  use c', (v '' s')  have h_v_inj : Injective v := by    intro _ _    grind  split_ands  · exact Infinite.image (injOn_of_injective h_v_inj (s := s')) h_s'_inf  · simp only [Finset.card_eq_two]    grind [Finset.pair_comm, Finset.coe_insert, Finset.coe_singleton]