no goals
X : Type ?u.5462
α : Type u_1
α' : Type ?u.5468
β : Type u_2
γ : Type ?u.5474
δ : Type ?u.5477
M : Type ?u.5480
E : Type ?u.5483
R : Type ?u.5486
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace α'
inst✝² : One β
inst✝¹ : One γ
inst✝ : One δ
g : β → γ
f : α → β
f₂ : α → γ
m : β → γ → δ
x : α
⊢ ¬x ∈ mulTSupport f ↔ f =ᶠ[𝓝 x] 1
simp_rw [mulTSupport, mem_closure_iff_nhds, not_forall, not_nonempty_iff_eq_empty, exists_prop,
  ← disjoint_iff_inter_eq_empty, disjoint_mulSupport_iff, eventuallyEq_iff_exists_mem]