I assume there's a reason you didn't just use [DecidableEq _] here? If so, can you add it to the docstring?

DecidablePred generalizes better to other SetLike things. But I was inconsistently using DecidableEq in the rest of the file, so I just use that everywhere.

It's not clear to me what the benefit of defining this on Finset is:

I definitely want to apply this to Finset. I need to integrate over a Pi-type over this Finset at some point.

Your suggestion means that I need to coerce the Finset to Set. It also means that all lemmas I want are inconveniently stated in terms of Set-operations instead of Finset-operations. So I need to add a bunch of rewrites commuting coerions with operations. This makes it less convenient to work with.

The proper way to do this is to define this for all SetLike objects, but this is impossible at the moment, as the docstring describes.

So I need to add a bunch of rewrites commuting coercions with operations.

Shouldn't norm_cast handle this?

The proper way to do this is to define this for all SetLike objects

I'd argue this is much worse, because now you need separate lemmas about updateSet _ (s ∩ t) for Set and Finset, and another seven or so for updateSet _ (s ⊓ t) for Submonoid, Submodule, .... Then you have to repeat this for bot and iInf and sInf.

If you do it for Set you only need to write these once, because simp turns everything into the set operations for you.

I gave this an honest try to use updateSet in our work. It is in d0aa7ef but it a lot less nice.

In the theorem marginal_union I do the following calculation (s and t are Finsets):

(∫⋯∫_s ∪ t, f ∂μ) x = 
∫⁻ (y : (i : ↥(s ∪ t)) → π i), f (updateFinset x (s ∪ t) y) ∂.pi fun i' : ↥(s ∪ t) ↦ μ i'

This is true by definition when using updateFinset.

When using updateSet, I have to be very careful to use Finset-unions. If I use Set-unions, then there are multiple places where the expression becomes type-incorrect (or it becomes nontrivial to prove that it is equal to the Finset-union case).

The rest of the calculation mostly goes through the same, if I'm very careful by explicitly stating where the coercions should be added. Some lemmas I still need to formulate for Finset specifically, and sometimes I can use Set analogues.

I strongly prefer to keep updateFinset. If you don't like this operation, I'd be happy to call it marginalAux or something and move it to the Marginal file, to be PR'd later. (marginalAux was actually the original name, until I thought that this operation might be more generally useful.)

EDIT: "just use norm_cast" isn't very helpful, since updateSet is a dependently typed function: the type of argument y depends on the set s, so rewriting the set s to an equal set s' is already quite painful.