α : Type u_1
β : Type ?u.384735
γ : Type ?u.384738
δ : Type ?u.384741
ι : Type ?u.384744
R : Type ?u.384747
R' : Type ?u.384750
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
hs' : Set.Nonempty s
⊢ ¬s = ∅
α : Type u_1
β : Type ?u.384735
γ : Type ?u.384738
δ : Type ?u.384741
ι : Type ?u.384744
R : Type ?u.384747
R' : Type ?u.384750
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
hs' : Set.Nonempty s
⊢ ↑↑count s ≠ 0
rw [Ne.def, count_eq_zero_iff]
no goals
α : Type u_1
β : Type ?u.384735
γ : Type ?u.384738
δ : Type ?u.384741
ι : Type ?u.384744
R : Type ?u.384747
R' : Type ?u.384750
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
hs' : Set.Nonempty s
⊢ ¬s = ∅
exact hs'.ne_empty