no goals
α : Type u
β : Type v
M : Type w
inst✝¹ : DecidableEq β
s : Finset α
t : Finset β
f : α → β
w : α → M
b : M
n : ℕ
inst✝ : LinearOrderedCancelAddCommMonoid M
hf : ∀ (y : β), ¬y ∈ t → ∑ x in filter (fun x => f x = y) s, w x ≤ 0
ht : Finset.Nonempty t
hb : card t • b ≤ ∑ x in s, w x
⊢ ∑ _y in t, b ≤ ∑ x in s, w x
simpa