obtain rfl | hs := s.eq_empty_or_nonempty
case h
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
ih :
  ∀ m < (s * t).card + s.card,
    ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : DecidableEq α] (s t : Finset α),
      m = (s * t).card + s.card →
        (s * (s * t).mulStab).card + (t * (s * t).mulStab).card ≤ (s * t).card + (s * t).mulStab.card
⊢ (s * (s * t).mulStab).card + (t * (s * t).mulStab).card ≤ (s * t).card + (s * t).mulStab.card
case h.inl
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
t : Finset α
ih :
  ∀ m < (∅ * t).card + ∅.card,
    ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : DecidableEq α] (s t : Finset α),
      m = (s * t).card + s.card →
        (s * (s * t).mulStab).card + (t * (s * t).mulStab).card ≤ (s * t).card + (s * t).mulStab.card
⊢ (∅ * (∅ * t).mulStab).card + (t * (∅ * t).mulStab).card ≤ (∅ * t).card + (∅ * t).mulStab.card

case h.inr
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
ih :
  ∀ m < (s * t).card + s.card,
    ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : DecidableEq α] (s t : Finset α),
      m = (s * t).card + s.card →
        (s * (s * t).mulStab).card + (t * (s * t).mulStab).card ≤ (s * t).card + (s * t).mulStab.card
hs : s.Nonempty
⊢ (s * (s * t).mulStab).card + (t * (s * t).mulStab).card ≤ (s * t).card + (s * t).mulStab.card