have : s * t = univ.sup fun b => s' b * t' b := by
  refine' le_antisymm _ (Finset.sup_le_iff.2 fun _ _ => hst' _)
  exact
    mul_subset_iff_right.2 fun b hb =>
      (smul_finset_subset_smul_finset $ hs' ⟨b, hb⟩).trans $
        (op_smul_finset_subset_mul $ hbt' ⟨b, hb⟩).trans $
          @le_sup _ _ _ _ _ (fun b => s' b * t' b) _ $ mem_univ _
α : 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' t' : { x // x ∈ t } → Finset α
hbt' : ∀ (b : { x // x ∈ t }), ↑b ∈ t' b
hs' : ∀ (b : { x // x ∈ t }), s ⊆ s' b
hst' : ∀ (b : { x // x ∈ t }), s' b * t' b ⊆ s * t
hstcard : ∀ (b : { x // x ∈ t }), (s' b).card + (t' b).card = s.card + t.card
ht' : ∀ (b : { x // x ∈ t }), Nat.find ⋯ = (t' b).card
⊢ 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' t' : { x // x ∈ t } → Finset α
hbt' : ∀ (b : { x // x ∈ t }), ↑b ∈ t' b
hs' : ∀ (b : { x // x ∈ t }), s ⊆ s' b
hst' : ∀ (b : { x // x ∈ t }), s' b * t' b ⊆ s * t
hstcard : ∀ (b : { x // x ∈ t }), (s' b).card + (t' b).card = s.card + t.card
ht' : ∀ (b : { x // x ∈ t }), Nat.find ⋯ = (t' b).card
this : s * t = univ.sup fun b => s' b * t' b
⊢ s.card + t.card ≤ (s * t).card + (s * t).mulStab.card