no goals
X : Type ?u.9177
α : Type u_1
α' : Type ?u.9183
β : Type u_2
γ : Type ?u.9189
δ : Type ?u.9192
M : Type ?u.9195
E : Type ?u.9198
R : Type ?u.9201
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace α'
inst✝³ : One β
inst✝² : One γ
inst✝¹ : One δ
g : β → γ
f : α → β
f₂ : α → γ
m : β → γ → δ
x : α
inst✝ : T2Space α
⊢ (∃ K, IsCompact K ∧ ∀ (x : α), ¬x ∈ K → f x = 1) ↔ HasCompactMulSupport f
simp_rw [← nmem_mulSupport, ← mem_compl_iff, ← subset_def, compl_subset_compl,
  hasCompactMulSupport_def, exists_compact_superset_iff]