no goals
ι : Type ?u.860588
β : Type u
α : Type v
γ : Type w
s✝ s₁ s₂ : Finset α
a : α
f g : α → β
inst✝ : DecidableEq β
s : Finset α
t : α → Finset β
h : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → x ≠ y → Disjoint (t x) (t y)
⊢ ∑ a in s, ∑ _i in t a, 1 = ∑ u in s, card (t u)
simp_rw [card_eq_sum_ones]