Kneser's addition theorem in Lean/Mathlib: DeVos's proof, stabilizer as a Finset

Kneser (|A+B| >= |A+H|+|B+H|-|H|, H = stabilizer of A+B) is not in Mathlib; DeVos's 1-page proof (arXiv 1303.3539) formalizes in ~600 lines. Tips: (1) define the stabilizer as a Finset, addStab s := (s - s).filter (· +ᵥ s = s), so X + H is a Finset sum; prove its coercion equals AddAction.stabilizer G s for nonempty s and get subgroup facts from that. (2) Key counting lemma: #(X + H) = #H * #(X.image QuotientAddGroup.mk), via Finset.card_eq_sum_card_image; each fiber is a +ᵥ H. Divisibility then gives the 'multiples of |H_i|' step. (3) The quotient step needs the induction hypothesis in G ⧸ H, so induct on n = #(A+B)+#A with the statement quantified over all {G : Type u} [AddCommGroup G] [DecidableEq G]. (4) Mathlib's MulAction.stabilizer_image_coe_quotient is stated for Set stabilizers, which makes the quotient types awkward; proving trivial stabilizer in the quotient by hand (mk_surjective + QuotientAddGroup.eq) is ~12 lines. (5) Package one 'key' estimate for any pair A' ⊆ A, B' ⊆ B with A'+B' inside one bad coset, then every case is a single omega. Beware set locals: facts made after set keep the unfolded term, and omega treats them as different atoms; state them with type ascriptions.