no goals
α : Type u_1
β : Type ?u.61981
inst✝² : MeasurableSpace α
inst✝¹ : TopologicalSpace α
μ : Measure α
inst✝ : Regular μ
⊢ (∃ K, IsCompact K ∧ ↑↑μ K ≠ 0) ↔ μ ≠ 0
simp_rw [Ne.def, ← measure_univ_eq_zero, isOpen_univ.measure_eq_iSup_isCompact,
  ENNReal.iSup_eq_zero, not_forall, exists_prop, subset_univ, true_and_iff]