[GOAL]
α : Type u_1
β : Type ?u.2132
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
s : Set α
hs : MeasurableSet s
⊢ ↑↑count s = ∑' (i : ↑s), 1
[PROOFSTEP]
simp only [count, sum_apply, hs, dirac_apply', ← tsum_subtype s (1 : α → ℝ≥0∞), Pi.one_apply]
[GOAL]
α : Type u_1
β : Type ?u.3143
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
s : Set α
⊢ ↑↑count ∅ = 0
[PROOFSTEP]
rw [count_apply MeasurableSet.empty, tsum_empty]
[GOAL]
α : Type u_1
β : Type ?u.3931
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
s✝ : Set α
s : Finset α
s_mble : MeasurableSet ↑s
⊢ ∑ i in s, 1 = ↑(Finset.card s)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type ?u.7325
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
s✝ s : Set α
s_fin : Set.Finite s
s_mble : MeasurableSet s
⊢ ↑↑count s = ↑(Finset.card (Finite.toFinset s_fin))
[PROOFSTEP]
simp [← @count_apply_finset' _ _ s_fin.toFinset (by simpa only [Finite.coe_toFinset] using s_mble)]
[GOAL]
α : Type u_1
β : Type ?u.7325
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
s✝ s : Set α
s_fin : Set.Finite s
s_mble : MeasurableSet s
⊢ MeasurableSet ↑(Finite.toFinset s_fin)
[PROOFSTEP]
simpa only [Finite.coe_toFinset] using s_mble
[GOAL]
α : Type u_1
β : Type ?u.8457
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
s✝ : Set α
inst✝ : MeasurableSingletonClass α
s : Set α
hs : Set.Finite s
⊢ ↑↑count s = ↑(Finset.card (Finite.toFinset hs))
[PROOFSTEP]
rw [← count_apply_finset, Finite.coe_toFinset]
[GOAL]
α : Type u_1
β : Type ?u.8764
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
s : Set α
hs : Set.Infinite s
⊢ ↑↑count s = ⊤
[PROOFSTEP]
refine' top_unique (le_of_tendsto' ENNReal.tendsto_nat_nhds_top fun n => _)
[GOAL]
α : Type u_1
β : Type ?u.8764
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
s : Set α
hs : Set.Infinite s
n : ℕ
⊢ ↑n ≤ ↑↑count s
[PROOFSTEP]
rcases hs.exists_subset_card_eq n with ⟨t, ht, rfl⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type ?u.8764
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
s : Set α
hs : Set.Infinite s
t : Finset α
ht : ↑t ⊆ s
⊢ ↑(Finset.card t) ≤ ↑↑count s
[PROOFSTEP]
calc
  (t.card : ℝ≥0∞) = ∑ i in t, 1 := by simp
  _ = ∑' i : (t : Set α), 1 := (t.tsum_subtype 1).symm
  _ ≤ count (t : Set α) := le_count_apply
  _ ≤ count s := measure_mono ht
[GOAL]
α : Type u_1
β : Type ?u.8764
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
s : Set α
hs : Set.Infinite s
t : Finset α
ht : ↑t ⊆ s
⊢ ↑(Finset.card t) = ∑ i in t, 1
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type ?u.12614
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
s : Set α
s_mble : MeasurableSet s
⊢ ↑↑count s = ⊤ ↔ Set.Infinite s
[PROOFSTEP]
by_cases hs : s.Finite
[GOAL]
case pos
α : Type u_1
β : Type ?u.12614
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
s : Set α
s_mble : MeasurableSet s
hs : Set.Finite s
⊢ ↑↑count s = ⊤ ↔ Set.Infinite s
[PROOFSTEP]
simp [Set.Infinite, hs, count_apply_finite' hs s_mble]
[GOAL]
case neg
α : Type u_1
β : Type ?u.12614
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
s : Set α
s_mble : MeasurableSet s
hs : ¬Set.Finite s
⊢ ↑↑count s = ⊤ ↔ Set.Infinite s
[PROOFSTEP]
change s.Infinite at hs 
[GOAL]
case neg
α : Type u_1
β : Type ?u.12614
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
s : Set α
s_mble : MeasurableSet s
hs : Set.Infinite s
⊢ ↑↑count s = ⊤ ↔ Set.Infinite s
[PROOFSTEP]
simp [hs, count_apply_infinite]
[GOAL]
α : Type u_1
β : Type ?u.13909
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
s : Set α
inst✝ : MeasurableSingletonClass α
⊢ ↑↑count s = ⊤ ↔ Set.Infinite s
[PROOFSTEP]
by_cases hs : s.Finite
[GOAL]
case pos
α : Type u_1
β : Type ?u.13909
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
s : Set α
inst✝ : MeasurableSingletonClass α
hs : Set.Finite s
⊢ ↑↑count s = ⊤ ↔ Set.Infinite s
[PROOFSTEP]
exact count_apply_eq_top' hs.measurableSet
[GOAL]
case neg
α : Type u_1
β : Type ?u.13909
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
s : Set α
inst✝ : MeasurableSingletonClass α
hs : ¬Set.Finite s
⊢ ↑↑count s = ⊤ ↔ Set.Infinite s
[PROOFSTEP]
change s.Infinite at hs 
[GOAL]
case neg
α : Type u_1
β : Type ?u.13909
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
s : Set α
inst✝ : MeasurableSingletonClass α
hs : Set.Infinite s
⊢ ↑↑count s = ⊤ ↔ Set.Infinite s
[PROOFSTEP]
simp [hs, count_apply_infinite]
[GOAL]
α : Type u_1
β : Type ?u.16312
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
s : Set α
s_mble : MeasurableSet s
hsc : ↑↑count s = 0
⊢ s = ∅
[PROOFSTEP]
have hs : s.Finite := by
  rw [← count_apply_lt_top' s_mble, hsc]
  exact WithTop.zero_lt_top
[GOAL]
α : Type u_1
β : Type ?u.16312
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
s : Set α
s_mble : MeasurableSet s
hsc : ↑↑count s = 0
⊢ Set.Finite s
[PROOFSTEP]
rw [← count_apply_lt_top' s_mble, hsc]
[GOAL]
α : Type u_1
β : Type ?u.16312
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
s : Set α
s_mble : MeasurableSet s
hsc : ↑↑count s = 0
⊢ 0 < ⊤
[PROOFSTEP]
exact WithTop.zero_lt_top
[GOAL]
α : Type u_1
β : Type ?u.16312
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
s : Set α
s_mble : MeasurableSet s
hsc : ↑↑count s = 0
hs : Set.Finite s
⊢ s = ∅
[PROOFSTEP]
simpa [count_apply_finite' hs s_mble] using hsc
[GOAL]
α : Type u_1
β : Type ?u.17964
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
s : Set α
inst✝ : MeasurableSingletonClass α
hsc : ↑↑count s = 0
⊢ s = ∅
[PROOFSTEP]
have hs : s.Finite := by
  rw [← count_apply_lt_top, hsc]
  exact WithTop.zero_lt_top
[GOAL]
α : Type u_1
β : Type ?u.17964
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
s : Set α
inst✝ : MeasurableSingletonClass α
hsc : ↑↑count s = 0
⊢ Set.Finite s
[PROOFSTEP]
rw [← count_apply_lt_top, hsc]
[GOAL]
α : Type u_1
β : Type ?u.17964
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
s : Set α
inst✝ : MeasurableSingletonClass α
hsc : ↑↑count s = 0
⊢ 0 < ⊤
[PROOFSTEP]
exact WithTop.zero_lt_top
[GOAL]
α : Type u_1
β : Type ?u.17964
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
s : Set α
inst✝ : MeasurableSingletonClass α
hsc : ↑↑count s = 0
hs : Set.Finite s
⊢ s = ∅
[PROOFSTEP]
simpa [count_apply_finite _ hs] using hsc
[GOAL]
α : Type u_1
β : Type ?u.20387
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
s : Set α
hs' : Set.Nonempty s
s_mble : MeasurableSet s
⊢ ↑↑count s ≠ 0
[PROOFSTEP]
rw [Ne.def, count_eq_zero_iff' s_mble]
[GOAL]
α : Type u_1
β : Type ?u.20387
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
s : Set α
hs' : Set.Nonempty s
s_mble : MeasurableSet s
⊢ ¬s = ∅
[PROOFSTEP]
exact hs'.ne_empty
[GOAL]
α : Type u_1
β : Type ?u.20618
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
s : Set α
inst✝ : MeasurableSingletonClass α
hs' : Set.Nonempty s
⊢ ↑↑count s ≠ 0
[PROOFSTEP]
rw [Ne.def, count_eq_zero_iff]
[GOAL]
α : Type u_1
β : Type ?u.20618
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
s : Set α
inst✝ : MeasurableSingletonClass α
hs' : Set.Nonempty s
⊢ ¬s = ∅
[PROOFSTEP]
exact hs'.ne_empty
[GOAL]
α : Type u_1
β : Type ?u.20894
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
s : Set α
a : α
ha : MeasurableSet {a}
⊢ ↑↑count {a} = 1
[PROOFSTEP]
rw [count_apply_finite' (Set.finite_singleton a) ha, Set.Finite.toFinset]
[GOAL]
α : Type u_1
β : Type ?u.20894
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
s : Set α
a : α
ha : MeasurableSet {a}
⊢ ↑(Finset.card (toFinset {a})) = 1
[PROOFSTEP]
simp [@toFinset_card _ _ (Set.finite_singleton a).fintype, @Fintype.card_unique _ _ (Set.finite_singleton a).fintype]
[GOAL]
α : Type u_2
β : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
s✝ : Set α
f : β → α
hf : Function.Injective f
s : Set β
s_mble : MeasurableSet s
fs_mble : MeasurableSet (f '' s)
⊢ ↑↑count (f '' s) = ↑↑count s
[PROOFSTEP]
by_cases hs : s.Finite
[GOAL]
case pos
α : Type u_2
β : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
s✝ : Set α
f : β → α
hf : Function.Injective f
s : Set β
s_mble : MeasurableSet s
fs_mble : MeasurableSet (f '' s)
hs : Set.Finite s
⊢ ↑↑count (f '' s) = ↑↑count s
[PROOFSTEP]
lift s to Finset β using hs
[GOAL]
case pos.intro
α : Type u_2
β : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
s✝ : Set α
f : β → α
hf : Function.Injective f
s : Finset β
s_mble : MeasurableSet ↑s
fs_mble : MeasurableSet (f '' ↑s)
⊢ ↑↑count (f '' ↑s) = ↑↑count ↑s
[PROOFSTEP]
rw [← Finset.coe_image, count_apply_finset' _, count_apply_finset' s_mble, s.card_image_of_injective hf]
[GOAL]
α : Type u_2
β : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
s✝ : Set α
f : β → α
hf : Function.Injective f
s : Finset β
s_mble : MeasurableSet ↑s
fs_mble : MeasurableSet (f '' ↑s)
⊢ MeasurableSet ↑(Finset.image f s)
[PROOFSTEP]
simpa only [Finset.coe_image] using fs_mble
[GOAL]
case neg
α : Type u_2
β : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
s✝ : Set α
f : β → α
hf : Function.Injective f
s : Set β
s_mble : MeasurableSet s
fs_mble : MeasurableSet (f '' s)
hs : ¬Set.Finite s
⊢ ↑↑count (f '' s) = ↑↑count s
[PROOFSTEP]
rw [count_apply_infinite hs]
[GOAL]
case neg
α : Type u_2
β : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
s✝ : Set α
f : β → α
hf : Function.Injective f
s : Set β
s_mble : MeasurableSet s
fs_mble : MeasurableSet (f '' s)
hs : ¬Set.Finite s
⊢ ↑↑count (f '' s) = ⊤
[PROOFSTEP]
rw [← finite_image_iff <| hf.injOn _] at hs 
[GOAL]
case neg
α : Type u_2
β : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
s✝ : Set α
f : β → α
hf : Function.Injective f
s : Set β
s_mble : MeasurableSet s
fs_mble : MeasurableSet (f '' s)
hs : ¬Set.Finite (f '' s)
⊢ ↑↑count (f '' s) = ⊤
[PROOFSTEP]
rw [count_apply_infinite hs]
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
s✝ : Set α
inst✝¹ : MeasurableSingletonClass α
inst✝ : MeasurableSingletonClass β
f : β → α
hf : Function.Injective f
s : Set β
⊢ ↑↑count (f '' s) = ↑↑count s
[PROOFSTEP]
by_cases hs : s.Finite
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
s✝ : Set α
inst✝¹ : MeasurableSingletonClass α
inst✝ : MeasurableSingletonClass β
f : β → α
hf : Function.Injective f
s : Set β
hs : Set.Finite s
⊢ ↑↑count (f '' s) = ↑↑count s
[PROOFSTEP]
exact count_injective_image' hf hs.measurableSet (Finite.image f hs).measurableSet
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
s✝ : Set α
inst✝¹ : MeasurableSingletonClass α
inst✝ : MeasurableSingletonClass β
f : β → α
hf : Function.Injective f
s : Set β
hs : ¬Set.Finite s
⊢ ↑↑count (f '' s) = ↑↑count s
[PROOFSTEP]
rw [count_apply_infinite hs]
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
s✝ : Set α
inst✝¹ : MeasurableSingletonClass α
inst✝ : MeasurableSingletonClass β
f : β → α
hf : Function.Injective f
s : Set β
hs : ¬Set.Finite s
⊢ ↑↑count (f '' s) = ⊤
[PROOFSTEP]
rw [← finite_image_iff <| hf.injOn _] at hs 
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
s✝ : Set α
inst✝¹ : MeasurableSingletonClass α
inst✝ : MeasurableSingletonClass β
f : β → α
hf : Function.Injective f
s : Set β
hs : ¬Set.Finite (f '' s)
⊢ ↑↑count (f '' s) = ⊤
[PROOFSTEP]
rw [count_apply_infinite hs]
[GOAL]
α : Type ?u.24262
β : Type ?u.24265
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
s : Set α
inst✝¹ : Finite α
inst✝ : MeasurableSpace α
⊢ ↑↑count univ < ⊤
[PROOFSTEP]
cases nonempty_fintype α
[GOAL]
case intro
α : Type ?u.24262
β : Type ?u.24265
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
s : Set α
inst✝¹ : Finite α
inst✝ : MeasurableSpace α
val✝ : Fintype α
⊢ ↑↑count univ < ⊤
[PROOFSTEP]
simpa [Measure.count_apply, tsum_fintype] using (ENNReal.nat_ne_top _).lt_top
