α : Type u_1
β : Type ?u.381469
γ : Type ?u.381472
δ : Type ?u.381475
ι : Type ?u.381478
R : Type ?u.381481
R' : Type ?u.381484
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
inst✝ : MeasurableSpace α
s_mble : MeasurableSet s
hsc : ↑↑count s = 0
hs : Set.Finite s
⊢ s = ∅
α : Type u_1
β : Type ?u.381469
γ : Type ?u.381472
δ : Type ?u.381475
ι : Type ?u.381478
R : Type ?u.381481
R' : Type ?u.381484
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
inst✝ : MeasurableSpace α
s_mble : MeasurableSet s
hsc : ↑↑count s = 0
⊢ s = ∅
have hs : s.Finite := by
  rw [← count_apply_lt_top' s_mble, hsc]
  exact WithTop.zero_lt_top
no goals
α : Type u_1
β : Type ?u.381469
γ : Type ?u.381472
δ : Type ?u.381475
ι : Type ?u.381478
R : Type ?u.381481
R' : Type ?u.381484
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
inst✝ : MeasurableSpace α
s_mble : MeasurableSet s
hsc : ↑↑count s = 0
hs : Set.Finite s
⊢ s = ∅
simpa [count_apply_finite' hs s_mble] using hsc
α : Type u_1
β : Type ?u.381469
γ : Type ?u.381472
δ : Type ?u.381475
ι : Type ?u.381478
R : Type ?u.381481
R' : Type ?u.381484
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
inst✝ : MeasurableSpace α
s_mble : MeasurableSet s
hsc : ↑↑count s = 0
⊢ 0 < ⊤
α : Type u_1
β : Type ?u.381469
γ : Type ?u.381472
δ : Type ?u.381475
ι : Type ?u.381478
R : Type ?u.381481
R' : Type ?u.381484
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
inst✝ : MeasurableSpace α
s_mble : MeasurableSet s
hsc : ↑↑count s = 0
⊢ Set.Finite s
rw [← count_apply_lt_top' s_mble, hsc]
no goals
α : Type u_1
β : Type ?u.381469
γ : Type ?u.381472
δ : Type ?u.381475
ι : Type ?u.381478
R : Type ?u.381481
R' : Type ?u.381484
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
inst✝ : MeasurableSpace α
s_mble : MeasurableSet s
hsc : ↑↑count s = 0
⊢ 0 < ⊤
exact WithTop.zero_lt_top