obtain ⟨a, rfl⟩ | ⟨a, ha, b, hb, hab⟩ := hs.exists_eq_singleton_or_nontrivial
case h.inr.inr.inr
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
hstab : (s * t).mulStab = 1
ih :
  ∀ (s' t' : Finset α),
    (s' * t').card + s'.card < (s * t).card + s.card →
      (s' * (s' * t').mulStab).card + (t' * (s' * t').mulStab).card ≤ (s' * t').card + (s' * t').mulStab.card
⊢ s.card + t.card ≤ (s * t).card + 1
case h.inr.inr.inr.inl.intro
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
t : Finset α
ht : t.Nonempty
a : α
hs : {a}.Nonempty
hstab : ({a} * t).mulStab = 1
ih :
  ∀ (s' t' : Finset α),
    (s' * t').card + s'.card < ({a} * t).card + {a}.card →
      (s' * (s' * t').mulStab).card + (t' * (s' * t').mulStab).card ≤ (s' * t').card + (s' * t').mulStab.card
⊢ {a}.card + t.card ≤ ({a} * t).card + 1

case h.inr.inr.inr.inr.intro.intro.intro.intro
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
hstab : (s * t).mulStab = 1
ih :
  ∀ (s' t' : Finset α),
    (s' * t').card + s'.card < (s * t).card + s.card →
      (s' * (s' * t').mulStab).card + (t' * (s' * t').mulStab).card ≤ (s' * t').card + (s' * t').mulStab.card
a : α
ha : a ∈ ↑s
b : α
hb : b ∈ ↑s
hab : a ≠ b
⊢ s.card + t.card ≤ (s * t).card + 1