cases not_nonempty_empty hs
case empty
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
ι : Type u_2
f : ι → Finset α
hs : ∅.Nonempty
⊢ (∅.inf' hs fun i => (f i).card + (f i).mulStab.card) ≤ (∅.sup f).card + (∅.sup f).mulStab.card
no goals