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