simp
case inr.inl
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t s : Finset α
hs : s.Nonempty
⊢ (s * (s * ∅).mulStab).card + (∅ * (s * ∅).mulStab).card ≤ (s * ∅).card + (s * ∅).mulStab.card
no goals