obtain rfl | hs := s.eq_empty_or_nonempty
case cons
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t : Finset α
ι : Type u_2
f : ι → Finset α
i : ι
s : Finset ι
hi : i ∉ s
ih : ∀ (hs : s.Nonempty), (s.inf' hs fun i => (f i).card + (f i).mulStab.card) ≤ (s.sup f).card + (s.sup f).mulStab.card
hs : (cons i s hi).Nonempty
⊢ ((cons i s hi).inf' hs fun i => (f i).card + (f i).mulStab.card) ≤
    ((cons i s hi).sup f).card + ((cons i s hi).sup f).mulStab.card
case cons.inl
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
ι : Type u_2
f : ι → Finset α
i : ι
hi : i ∉ ∅
ih : ∀ (hs : ∅.Nonempty), (∅.inf' hs fun i => (f i).card + (f i).mulStab.card) ≤ (∅.sup f).card + (∅.sup f).mulStab.card
hs : (cons i ∅ hi).Nonempty
⊢ ((cons i ∅ hi).inf' hs fun i => (f i).card + (f i).mulStab.card) ≤
    ((cons i ∅ hi).sup f).card + ((cons i ∅ hi).sup f).mulStab.card

case cons.inr
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t : Finset α
ι : Type u_2
f : ι → Finset α
i : ι
s : Finset ι
hi : i ∉ s
ih : ∀ (hs : s.Nonempty), (s.inf' hs fun i => (f i).card + (f i).mulStab.card) ≤ (s.sup f).card + (s.sup f).mulStab.card
hs✝ : (cons i s hi).Nonempty
hs : s.Nonempty
⊢ ((cons i s hi).inf' hs✝ fun i => (f i).card + (f i).mulStab.card) ≤
    ((cons i s hi).sup f).card + ((cons i s hi).sup f).mulStab.card