no goals
ι : Type ?u.105253
α : Type u_1
β : Type ?u.105259
M : Type ?u.105262
N : Type ?u.105265
G : Type ?u.105268
k : Type ?u.105271
R : Type ?u.105274
inst✝¹ : DecidableEq α
s : Finset α
B : Finset (Finset α)
n : ℕ
inst✝ : Fintype α
h : ∀ (a : α), card (filter ((fun x x_1 => x ∈ x_1) a) B) ≤ n
⊢ ∑ s in B, card s = ∑ s in B, card (univ ∩ s)
simp_rw [univ_inter]