no goals
α : Type u_2
β : Type ?u.6623
ι : Type ?u.6626
M : Type u_1
N : Type ?u.6632
inst✝¹ : One M
inst✝ : One N
s t : Set α
f g : α → M
a✝ a : α
⊢ mulIndicator s f a ≠ 1 ↔ a ∈ s ∩ mulSupport f
simp only [Ne.def, mulIndicator_apply_eq_one, not_imp, mem_inter_iff, mem_mulSupport]