no goals
α : Type u
β : Type v
γ : Type w
ι : Sort x
π : α → Type u_1
inst✝ : Finite α
s : (a : α) → Set (π a)
hs : ∀ (a : α), Set.Countable (s a)
⊢ Set.Countable {f | ∀ (a : α), f a ∈ s a}
simpa only [← mem_univ_pi] using countable_univ_pi hs