refine' (le_inf' ht.attach _ fun b _ => _).trans (le_card_sup_add_card_mulStab_sup _)
α : 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 ≤ (univ.sup fun b => s' b * t' b).card + (univ.sup fun b => s' b * t' b).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
b : { x // x ∈ t }
x✝ : b ∈ t.attach
⊢ s.card + t.card ≤ (s' b * t' b).card + (s' b * t' b).mulStab.card