If S.card > T.card then there is an element in S that is not

Stream: Is there code for X?

[Christoph Spiegel]

Hi, I couldn't find the following simple statement in mathlib: (α : Type*) (S T : Finset α) (h : S.card > T.card) : ∃ s ∈ S, s ∉ T . Did I miss anything or is it really not there? I think it can be proven somewhat quickly through Set.exists_of_ssubset but it would probably be a good idea to include this statement in Mathlib.Data.Set.Finite.Basic. If I didn't miss anything I can PR that.

[Riccardo Brasca]

We have Finset.le_card_sdiff that is very close

[Yaël Dillies]

Your lemma is kick to obtain from docs#Finset.sdiff_nonempty, but it is true that we have docs#Set.diff_nonempty_of_ncard_lt_ncard

[Christoph Spiegel]

Ah, what is the current philosophy re Set vs Finset and duplicate statements? If sth like Set.diff_nonempty_of_ncard_lt_ncard exists should I rather throw my Finset into it and let coercion work it out or is it valid to duplicate statements and also have a Finset.diff_nonempty_of_ncard_lt_ncard?

[Yaël Dillies]

Set and Finset should have as closingly matching API as possible

[Christoph Spiegel]

Alright, I take that as saying that it's a good idea to PR it? I'm teaching an introductory course on Lean right now and this came up. I could use this as a nice example of how to PR stuff in Mathlib on Friday to round out the course.

[Yaël Dillies]

Yes, I was originally going to say that we don't want it, because too close to existing lemmas, but then noticed that the corresponding Set lemma did exist

[Christoph Spiegel]

Done #23712

[Yaël Dillies]

#23712

[Christoph Spiegel]

Thanks @Yaël Dillies and @Bhavik Mehta for the quick merge. The students really appreciated seeing the life cycle of a PR!