α : Type u
β : Type v
M : Type w
inst✝¹ : DecidableEq β
s : Finset α
t : Finset β
f : α → β
w : α → M
b : M
n : ℕ
inst✝ : LinearOrderedCommSemiring M
ht : Finset.Nonempty t
hb : ∑ a in s, 1 ≤ card t • b
⊢ ∃ y, y ∈ t ∧ ∑ a in filter (fun x => f x = y) s, 1 ≤ b
α : Type u
β : Type v
M : Type w
inst✝¹ : DecidableEq β
s : Finset α
t : Finset β
f : α → β
w : α → M
b : M
n : ℕ
inst✝ : LinearOrderedCommSemiring M
ht : Finset.Nonempty t
hb : ↑(card s) ≤ card t • b
⊢ ∃ y, y ∈ t ∧ ↑(card (filter (fun x => f x = y) s)) ≤ b
simp_rw [cast_card] at hb⊢
no goals
α : Type u
β : Type v
M : Type w
inst✝¹ : DecidableEq β
s : Finset α
t : Finset β
f : α → β
w : α → M
b : M
n : ℕ
inst✝ : LinearOrderedCommSemiring M
ht : Finset.Nonempty t
hb : ∑ a in s, 1 ≤ card t • b
⊢ ∃ y, y ∈ t ∧ ∑ a in filter (fun x => f x = y) s, 1 ≤ b
refine'
  exists_sum_fiber_le_of_sum_fiber_nonneg_of_sum_le_nsmul
    (fun _ _ => sum_nonneg fun _ _ => zero_le_one) ht hb