no goals
α : Type u_1
ι : Sort u_2
κ : ι → Sort u_3
A B : Set (Finset α)
r : ℕ
f : (i : ι) → κ i → Set (Finset α)
⊢ Sized r (⋃ (i : ι) (j : κ i), f i j) ↔ ∀ (i : ι) (j : κ i), Sized r (f i j)
simp only [Set.sized_iUnion]