Stabilizer of a finset

Stream: mathlib4

[Yaël Dillies]

In LeanCamCombi, @Mantas Baksys and I have a proof of Kneser's addition theorem.

[Yaël Dillies]

The statement is about pointwise addition of sets. If $A, B$ are nonempty sets in an abelian group and $H$ is the stabilizer of $A + B$ (which is finite since the stabilizer of a nonempty finite set $X$ is contained in $X - X$, hence is finite itself), then it says $|A + H| + |B + H| ≤ |A + B| + |H|$

[Yaël Dillies]

This is useful (and in fact very powerful) because it gives a lower bound on $|A + B|$ in terms of $|H|$.

[Yaël Dillies]

Now the question is how this should be stated in Lean. Currently, I use docs#Finset.card for all the cardinalities in the statement and therefore must define $H$ as a finset (called Finset.addStab in LeanCamCombi). Since the stabilizer of $∅$ is the full group (which might be infinite), I define ∅.addStab = ∅ and as a bonus my statement is now true without the non-emptiness assumption on $A$ and $B$.

[Yaël Dillies]

However, PFR has recently had some success using docs#Nat.card on subgroups, so I would like your opinion on whether you think Finset.addStab is worth having to keep the entire Kneser statement in the finset world.