obtain rfl | hs := s.eq_empty_or_nonempty
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
⊢ min (s.card + s.mulStab.card) (t.card + t.mulStab.card) ≤ (s ∪ t).card + (s ∪ t).mulStab.card
case inl
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
t : Finset α
⊢ min (∅.card + ∅.mulStab.card) (t.card + t.mulStab.card) ≤ (∅ ∪ t).card + (∅ ∪ t).mulStab.card

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