∀ {ι : Type u_1} {μ : Type u_2} [inst : DecidableEq ι] [inst_1 : AddCommMonoid μ] {s : Finset ι} {f : ι → μ}
  (e : ↥s ≃ Fin s.card),
  (∀ (i : ι), f i ≠ 0 → i ∈ s) → (fun i => if hi : i ∈ s then (f ∘ Subtype.val ∘ ⇑e.symm) (e ⟨i, hi⟩) else 0) = f