Finpartitions of Sets and Finsets

Stream: mathlib4

[Christian Krause]

Hi,
recently I was trying to do somethings with Finpartions of Sets. I found the docs#Finpartition.part operation which returns the part of the finset that a certain element lies in. I was a bit disappointed when I realized that this is only defined for Finpartitions of Finsets. So I got to work trying to replicate the Finpartitions of Finsets Api for Finpartitions of Sets.
But most of the lemmas are essentially the same. For example this one:

lemma subset {a : Set α} (ha : a ∈ P.parts) : a ⊆ s := P.le ha

(This is a bit of a handwavy question, but) is there a way to state such a lemma once and get it for sets and finsets?

My second question is, how should I do the naming (without messing up the existing Api too much). For example the Finpartition.part Function is needed for both Finsets and Sets, but is slightly different, because it uses a different choice function. Do you have any advice how I can do this? (Or should I ask more concretly for the specific instances of my question?)

[Christian Krause]

@Yaël Dillies I think I saw a Zulip Post from 2023 of you talking about the Finpartition of Finset API but that ended quite abruptly.

[Yaël Dillies]

I don't have good answers here, sorry! The only satisfying way out is IMO to abstract out the order relation between α and Set α/Finset α, ie the former indexes atoms of the latter two.

[Christian Krause]

I tried to do this but this generality has a bunch of drawbacks. I am mainly interested in getting docs#Finpartition.part for Finpartitions of Sets. Finpartition.part for Finsets is defined using Finset.choose, which would have to be classical.choose for sets (I think). Or am I missing something which would make it possible to abstract this out without having to using classical even for finsets?

[Christian Krause]

(I am realizing that I don't fully understand how to "turn on" classical selectively, where can I read up on this?)