no goals
α : Type u_1
β : Type u_2
γ : Type ?u.39863
f✝ g : α → β
c c₁ c₂ x : α
inst✝¹ : Add α
inst✝ : CommMonoid β
ι : Type u_3
f : ι → α → β
s : Finset ι
hs : ∀ (i : ι), i ∈ s → Periodic (f i) c
⊢ ∀ (f_1 : α → β), f_1 ∈ List.map f (Finset.toList s) → Periodic f_1 c
simpa [-Periodic]