α : Type u_1
β : Type ?u.382504
γ : Type ?u.382507
δ : Type ?u.382510
ι : Type ?u.382513
R : Type ?u.382516
R' : Type ?u.382519
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
hsc : ↑↑count s = 0
hs : Set.Finite s
⊢ s = ∅
α : Type u_1
β : Type ?u.382504
γ : Type ?u.382507
δ : Type ?u.382510
ι : Type ?u.382513
R : Type ?u.382516
R' : Type ?u.382519
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
hsc : ↑↑count s = 0
⊢ s = ∅
have hs : s.Finite := by
  rw [← count_apply_lt_top, hsc]
  exact WithTop.zero_lt_top
no goals
α : Type u_1
β : Type ?u.382504
γ : Type ?u.382507
δ : Type ?u.382510
ι : Type ?u.382513
R : Type ?u.382516
R' : Type ?u.382519
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
hsc : ↑↑count s = 0
hs : Set.Finite s
⊢ s = ∅
simpa [count_apply_finite _ hs] using hsc
α : Type u_1
β : Type ?u.382504
γ : Type ?u.382507
δ : Type ?u.382510
ι : Type ?u.382513
R : Type ?u.382516
R' : Type ?u.382519
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
hsc : ↑↑count s = 0
⊢ 0 < ⊤
α : Type u_1
β : Type ?u.382504
γ : Type ?u.382507
δ : Type ?u.382510
ι : Type ?u.382513
R : Type ?u.382516
R' : Type ?u.382519
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
hsc : ↑↑count s = 0
⊢ Set.Finite s
rw [← count_apply_lt_top, hsc]
no goals
α : Type u_1
β : Type ?u.382504
γ : Type ?u.382507
δ : Type ?u.382510
ι : Type ?u.382513
R : Type ?u.382516
R' : Type ?u.382519
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
hsc : ↑↑count s = 0
⊢ 0 < ⊤
exact WithTop.zero_lt_top