no goals
G : Type ?u.78809
M : Type ?u.78812
α : Type u_1
s : Set α
m : MeasurableSpace α
inst✝⁸ : Group G
inst✝⁷ : MulAction G α
inst✝⁶ : MeasurableSpace G
inst✝⁵ : MeasurableSMul G α
c : G
μ : Measure α
inst✝⁴ : SMulInvariantMeasure G α μ
inst✝³ : TopologicalSpace α
inst✝² : ContinuousConstSMul G α
inst✝¹ : MulAction.IsMinimal G α
K U : Set α
inst✝ : Regular μ
hμ : μ ≠ 0
hU : IsOpen U
⊢ ↑↑μ U = 0 ↔ U = ∅
rw [← not_iff_not, ← Ne.def, ← pos_iff_ne_zero,
  measure_pos_iff_nonempty_of_smulInvariant G hμ hU, nonempty_iff_ne_empty]