simp [-zero_le']
case inr.inl
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s : Finset α
hs : s.Nonempty
⊢ min (s.card + s.mulStab.card) (∅.card + ∅.mulStab.card) ≤ (s ∪ ∅).card + (s ∪ ∅).mulStab.card
no goals