Ramsey THeory

Stream: graph theory

[Hunter Monroe]

@Bhavik Mehta would you be willing to update your finite and infinite Ramsey proofs to work with the current mathlib? I tried that with the finite version and fixed a problem exists_mem_of_ne_empty with the finite version (see my fix using calc) but could not work out how to fix insert_empty_eq_singleton. It would be good to get some version of your proofs into mathlib which can later be improved upon and generalized.

[Bhavik Mehta]

I can have a go at updating the infinite Ramsey proof, that's pretty much in a maximal generality. For the finite Ramsey proof, I think the approach isn't quite right, and that it would actually be easier to go straight for a more general version