α : Type u
β : Type v
M : Type w
inst✝¹ : DecidableEq β
s : Finset α
t : Finset β
f : α → β
w : α → M
b : M
n : ℕ
inst✝ : LinearOrderedCommSemiring M
ht : ∑ 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 : ↑(card s) < card t • b
⊢ ∃ y, y ∈ t ∧ ↑(card (filter (fun x => f x = y) s)) < b
simp_rw [cast_card] at ht⊢
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 : ∑ a in s, 1 < card t • b
⊢ ∃ y, y ∈ t ∧ ∑ a in filter (fun x => f x = y) s, 1 < b
exact
  exists_sum_fiber_lt_of_sum_fiber_nonneg_of_sum_lt_nsmul
    (fun _ _ => sum_nonneg fun _ _ => zero_le_one) ht