ι : Type ?u.106343
α : Type u_1
β : Type ?u.106349
M : Type ?u.106352
N : Type ?u.106355
G : Type ?u.106358
k : Type ?u.106361
R : Type ?u.106364
inst✝ : DecidableEq α
s : Finset α
B : Finset (Finset α)
n : ℕ
h : ∀ (a : α), a ∈ s → n ≤ card (filter ((fun x x_1 => x ∈ x_1) a) B)
⊢ ∑ x in s, card (filter ((fun x x_1 => x ∈ x_1) x) B) ≤ ∑ t in B, card (s ∩ t)
ι : Type ?u.106343
α : Type u_1
β : Type ?u.106349
M : Type ?u.106352
N : Type ?u.106355
G : Type ?u.106358
k : Type ?u.106361
R : Type ?u.106364
inst✝ : DecidableEq α
s : Finset α
B : Finset (Finset α)
n : ℕ
h : ∀ (a : α), a ∈ s → n ≤ card (filter ((fun x x_1 => x ∈ x_1) a) B)
⊢ card s * n ≤ ∑ t in B, card (s ∩ t)
apply (s.card_nsmul_le_sum _ _ h).trans
ι : Type ?u.106343
α : Type u_1
β : Type ?u.106349
M : Type ?u.106352
N : Type ?u.106355
G : Type ?u.106358
k : Type ?u.106361
R : Type ?u.106364
inst✝ : DecidableEq α
s : Finset α
B : Finset (Finset α)
n : ℕ
h : ∀ (a : α), a ∈ s → n ≤ card (filter ((fun x x_1 => x ∈ x_1) a) B)
⊢ (∑ x in s, ∑ a in B, if x ∈ a then 1 else 0) ≤ ∑ x in B, ∑ a in s, if a ∈ x then 1 else 0
ι : Type ?u.106343
α : Type u_1
β : Type ?u.106349
M : Type ?u.106352
N : Type ?u.106355
G : Type ?u.106358
k : Type ?u.106361
R : Type ?u.106364
inst✝ : DecidableEq α
s : Finset α
B : Finset (Finset α)
n : ℕ
h : ∀ (a : α), a ∈ s → n ≤ card (filter ((fun x x_1 => x ∈ x_1) a) B)
⊢ ∑ x in s, card (filter ((fun x x_1 => x ∈ x_1) x) B) ≤ ∑ t in B, card (s ∩ t)
simp_rw [← filter_mem_eq_inter, card_eq_sum_ones, sum_filter]
no goals
ι : Type ?u.106343
α : Type u_1
β : Type ?u.106349
M : Type ?u.106352
N : Type ?u.106355
G : Type ?u.106358
k : Type ?u.106361
R : Type ?u.106364
inst✝ : DecidableEq α
s : Finset α
B : Finset (Finset α)
n : ℕ
h : ∀ (a : α), a ∈ s → n ≤ card (filter ((fun x x_1 => x ∈ x_1) a) B)
⊢ (∑ x in s, ∑ a in B, if x ∈ a then 1 else 0) ≤ ∑ x in B, ∑ a in s, if a ∈ x then 1 else 0
exact sum_comm.le