no goals
α : Type u_3
β : Type u_2
γ : Type u_1
δ : Type ?u.56247
inst✝¹ : AddCommMonoid α
inst✝ : TopologicalSpace α
f g : β → α
a b : α
s : Finset β
e : γ ≃ β
⊢ ∀ (x : β), ¬x ∈ Set.range ↑e → f x = 0
simp