no goals
α : Type u_1
β : Type ?u.3073
ι : Type ?u.3076
M : Type u_2
N : Type ?u.3082
inst✝¹ : One M
inst✝ : One N
s t : Set α
f g : α → M
a : α
⊢ mulIndicator s f = f ↔ mulSupport f ⊆ s
simp only [funext_iff, subset_def, mem_mulSupport, mulIndicator_apply_eq_self, not_imp_comm]