ι : Type ?u.102009
α : Type u_1
β : Type ?u.102015
M : Type ?u.102018
N : Type ?u.102021
G : Type ?u.102024
k : Type ?u.102027
R : Type ?u.102030
inst✝ : DecidableEq α
s : Finset α
B : Finset (Finset α)
n : ℕ
h : ∀ (a : α), a ∈ s → card (filter ((fun x x_1 => x ∈ x_1) a) B) ≤ n
⊢ ∑ t in B, card (s ∩ t) ≤ ∑ x in s, card (filter ((fun x x_1 => x ∈ x_1) x) B)
ι : Type ?u.102009
α : Type u_1
β : Type ?u.102015
M : Type ?u.102018
N : Type ?u.102021
G : Type ?u.102024
k : Type ?u.102027
R : Type ?u.102030
inst✝ : DecidableEq α
s : Finset α
B : Finset (Finset α)
n : ℕ
h : ∀ (a : α), a ∈ s → card (filter ((fun x x_1 => x ∈ x_1) a) B) ≤ n
⊢ ∑ t in B, card (s ∩ t) ≤ card s * n
refine' le_trans _ (s.sum_le_card_nsmul _ _ h)
ι : Type ?u.102009
α : Type u_1
β : Type ?u.102015
M : Type ?u.102018
N : Type ?u.102021
G : Type ?u.102024
k : Type ?u.102027
R : Type ?u.102030
inst✝ : DecidableEq α
s : Finset α
B : Finset (Finset α)
n : ℕ
h : ∀ (a : α), a ∈ s → card (filter ((fun x x_1 => x ∈ x_1) a) B) ≤ n
⊢ (∑ x in B, ∑ a in s, if a ∈ x then 1 else 0) ≤ ∑ x in s, ∑ a in B, if x ∈ a then 1 else 0
ι : Type ?u.102009
α : Type u_1
β : Type ?u.102015
M : Type ?u.102018
N : Type ?u.102021
G : Type ?u.102024
k : Type ?u.102027
R : Type ?u.102030
inst✝ : DecidableEq α
s : Finset α
B : Finset (Finset α)
n : ℕ
h : ∀ (a : α), a ∈ s → card (filter ((fun x x_1 => x ∈ x_1) a) B) ≤ n
⊢ ∑ t in B, card (s ∩ t) ≤ ∑ x in s, card (filter ((fun x x_1 => x ∈ x_1) x) B)
simp_rw [← filter_mem_eq_inter, card_eq_sum_ones, sum_filter]
no goals
ι : Type ?u.102009
α : Type u_1
β : Type ?u.102015
M : Type ?u.102018
N : Type ?u.102021
G : Type ?u.102024
k : Type ?u.102027
R : Type ?u.102030
inst✝ : DecidableEq α
s : Finset α
B : Finset (Finset α)
n : ℕ
h : ∀ (a : α), a ∈ s → card (filter ((fun x x_1 => x ∈ x_1) a) B) ≤ n
⊢ (∑ x in B, ∑ a in s, if a ∈ x then 1 else 0) ≤ ∑ x in s, ∑ a in B, if x ∈ a then 1 else 0
exact sum_comm.le