Status of !4#2526 `Combinatorics.SimpleGraph.Coloring`

Stream: mathlib4

[Arien Malec]

Fixed a number of issues here, but have three remaining, two instance/coercion issues and one where I have a proof that "works" but fails in a bizarre way (documented in the PR comments)

[Kyle Miller]

@Arien Malec Fixed them. They mostly had to do with how Lean 4 doesn't like to find typeclass instances through unification.