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 * t ≤ univ.sup fun b => s' b * t' b
no goals