[GOAL]
α : 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
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
[PROOFSTEP]
simpa only [sum_fiberwise_of_maps_to hf, sum_const]
[GOAL]
α : Type u
β : Type v
M : Type w
inst✝¹ : DecidableEq β
s : Finset α
t : Finset β
f : α → β
w : α → M
b : M
n : ℕ
inst✝ : LinearOrderedCancelAddCommMonoid M
ht : ∀ (y : β), ¬y ∈ t → ∑ x in filter (fun x => f x = y) s, w x ≤ 0
hb : card t • b < ∑ x in s, w x
⊢ ∑ _y in t, b < ∑ x in s, w x
[PROOFSTEP]
simpa
[GOAL]
α : 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
[PROOFSTEP]
simpa only [sum_fiberwise_of_maps_to hf, sum_const]
[GOAL]
α : 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
[PROOFSTEP]
simpa
[GOAL]
α : Type u
β : Type v
M : Type w
inst✝¹ : DecidableEq β
s : Finset α
t : Finset β
f : α → β
w : α → M
b : M
n : ℕ
inst✝ : LinearOrderedCommSemiring M
hf : ∀ (a : α), a ∈ s → f a ∈ t
ht : card t • b < ↑(card s)
⊢ ∃ y, y ∈ t ∧ b < ↑(card (filter (fun x => f x = y) s))
[PROOFSTEP]
simp_rw [cast_card] at ht ⊢
[GOAL]
α : Type u
β : Type v
M : Type w
inst✝¹ : DecidableEq β
s : Finset α
t : Finset β
f : α → β
w : α → M
b : M
n : ℕ
inst✝ : LinearOrderedCommSemiring M
hf : ∀ (a : α), a ∈ s → f a ∈ t
ht : card t • b < ∑ a in s, 1
⊢ ∃ y, y ∈ t ∧ b < ∑ a in filter (fun x => f x = y) s, 1
[PROOFSTEP]
exact exists_lt_sum_fiber_of_maps_to_of_nsmul_lt_sum hf ht
[GOAL]
α : 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
[PROOFSTEP]
simp_rw [cast_card] at ht ⊢
[GOAL]
α : 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
[PROOFSTEP]
exact exists_sum_fiber_lt_of_sum_fiber_nonneg_of_sum_lt_nsmul (fun _ _ => sum_nonneg fun _ _ => zero_le_one) ht
[GOAL]
α : Type u
β : Type v
M : Type w
inst✝¹ : DecidableEq β
s : Finset α
t : Finset β
f : α → β
w : α → M
b : M
n : ℕ
inst✝ : LinearOrderedCommSemiring M
hf : ∀ (a : α), a ∈ s → f a ∈ t
ht : Finset.Nonempty t
hb : card t • b ≤ ↑(card s)
⊢ ∃ y, y ∈ t ∧ b ≤ ↑(card (filter (fun x => f x = y) s))
[PROOFSTEP]
simp_rw [cast_card] at hb ⊢
[GOAL]
α : Type u
β : Type v
M : Type w
inst✝¹ : DecidableEq β
s : Finset α
t : Finset β
f : α → β
w : α → M
b : M
n : ℕ
inst✝ : LinearOrderedCommSemiring M
hf : ∀ (a : α), a ∈ s → f a ∈ t
ht : Finset.Nonempty t
hb : card t • b ≤ ∑ a in s, 1
⊢ ∃ y, y ∈ t ∧ b ≤ ∑ a in filter (fun x => f x = y) s, 1
[PROOFSTEP]
exact exists_le_sum_fiber_of_maps_to_of_nsmul_le_sum hf ht hb
[GOAL]
α : 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
[PROOFSTEP]
simp_rw [cast_card] at hb ⊢
[GOAL]
α : 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
[PROOFSTEP]
refine' exists_sum_fiber_le_of_sum_fiber_nonneg_of_sum_le_nsmul (fun _ _ => sum_nonneg fun _ _ => zero_le_one) ht hb
