have :
  ∀ b : t,
    ∃ n s' t',
      ↑b ∈ t' ∧ s ⊆ s' ∧ s' * t' ⊆ s * t ∧ s'.card + t'.card = s.card + t.card ∧ n = t'.card :=
  fun b => ⟨_, s, t, b.2, Subset.rfl, Subset.rfl, rfl, rfl⟩
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
⊢ s.card + t.card ≤ (s * t).card + (s * t).mulStab.card
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
this :
  ∀ (b : { x // x ∈ t }),
    ∃ n s' t', ↑b ∈ t' ∧ s ⊆ s' ∧ s' * t' ⊆ s * t ∧ s'.card + t'.card = s.card + t.card ∧ n = t'.card
⊢ s.card + t.card ≤ (s * t).card + (s * t).mulStab.card