α : Type u_1
β : Type ?u.374309
γ : Type ?u.374312
δ : Type ?u.374315
ι : Type ?u.374318
R : Type ?u.374321
R' : Type ?u.374324
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
inst✝ : MeasurableSpace α
hs : Set.Infinite s
n : ℕ
⊢ ↑n ≤ ↑↑count s
α : Type u_1
β : Type ?u.374309
γ : Type ?u.374312
δ : Type ?u.374315
ι : Type ?u.374318
R : Type ?u.374321
R' : Type ?u.374324
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
inst✝ : MeasurableSpace α
hs : Set.Infinite s
⊢ ↑↑count s = ⊤
refine' top_unique (le_of_tendsto' ENNReal.tendsto_nat_nhds_top fun n => _)
case intro.intro
α : Type u_1
β : Type ?u.374309
γ : Type ?u.374312
δ : Type ?u.374315
ι : Type ?u.374318
R : Type ?u.374321
R' : Type ?u.374324
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t✝ : Set α
inst✝ : MeasurableSpace α
hs : Set.Infinite s
t : Finset α
ht : ↑t ⊆ s
⊢ ↑(Finset.card t) ≤ ↑↑count s
α : Type u_1
β : Type ?u.374309
γ : Type ?u.374312
δ : Type ?u.374315
ι : Type ?u.374318
R : Type ?u.374321
R' : Type ?u.374324
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
inst✝ : MeasurableSpace α
hs : Set.Infinite s
n : ℕ
⊢ ↑n ≤ ↑↑count s
rcases hs.exists_subset_card_eq n with ⟨t, ht, rfl⟩
no goals
case intro.intro
α : Type u_1
β : Type ?u.374309
γ : Type ?u.374312
δ : Type ?u.374315
ι : Type ?u.374318
R : Type ?u.374321
R' : Type ?u.374324
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t✝ : Set α
inst✝ : MeasurableSpace α
hs : Set.Infinite s
t : Finset α
ht : ↑t ⊆ s
⊢ ↑(Finset.card t) ≤ ↑↑count s
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
no goals
α : Type u_1
β : Type ?u.374309
γ : Type ?u.374312
δ : Type ?u.374315
ι : Type ?u.374318
R : Type ?u.374321
R' : Type ?u.374324
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t✝ : Set α
inst✝ : MeasurableSpace α
hs : Set.Infinite s
t : Finset α
ht : ↑t ⊆ s
⊢ ↑(Finset.card t) = ∑ i in t, 1
simp