SetLike instance for Finset

Stream: mathlib4

[Antoine Chambert-Loir]

In his review of a PR of mine, @Junyan Xu observed that there was no SetLike instance for Finset. I easily provided one in #28076, but that breaks swiftly because docs#Finset.toSet already provides a coercion mechanism, via the instance docs#Finset.instCoeTCSet
I 'm tempted to believe that this instance had been defined before docs#SetLike existed but have no serious opinion of how mathlib should be designed in this case.

[Yaël Dillies]

It's very practical being able to write .toSet when the coercion system fails to understand that the only coercion Finset α → Set ?β is when ?β := α. Apart from that, adding the SetLike instance should be no issue

[Antoine Chambert-Loir]

In practice, adding this instance brings some issues, because Lean doesn't get that te two coercions coincide, hence some previously-terminating simp don't work anymore.

[Yaël Dillies]

Yes, you would need to remove Finset.toSet

[Junyan Xu]

Do you mean to remove Finset.instCoeTCSet?

[Junyan Xu]

Let's see how many changes are needed for #28241 to pass CI ...

[Junyan Xu]

#28241 builds with 25 files changed (+54 -62) which is pretty reasonable IMO. What I did is making Finset.toSet an abbrev of SetLike.coe.

[Junyan Xu]

I had to revert one of the grind golfs back to

rintro ⟨i, hi⟩; specialize h i hi; simp_rw [sets_t', dif_pos hi] at h; exact h

and grind's output is Probability.Kernel grind failure.txt.
If anyone knows how to golf it again please do.