obtain rfl | ht := t.eq_empty_or_nonempty
case inr
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
hs : s.Nonempty
⊢ min (s.card + s.mulStab.card) (t.card + t.mulStab.card) ≤ (s ∪ t).card + (s ∪ t).mulStab.card
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

case inr.inr
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
⊢ min (s.card + s.mulStab.card) (t.card + t.mulStab.card) ≤ (s ∪ t).card + (s ∪ t).mulStab.card