no goals
ι : Type ?u.111164
α : Type u_1
β : Type ?u.111170
M : Type ?u.111173
N : Type ?u.111176
G : Type ?u.111179
k : Type ?u.111182
R : Type ?u.111185
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 = Fintype.card α * n
simp_rw [Fintype.card, ← sum_card_inter fun a _ ↦ h a, univ_inter]