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 : ∀ (a : α), a ∈ s → f a ∈ t
ht : Finset.Nonempty t
hb : card t • b ≤ ∑ x in s, w x
⊢ ∑ i in t, b ≤ ∑ i in t, ∑ x in filter (fun x => f x = i) s, w x
simpa only [sum_fiberwise_of_maps_to hf, sum_const]