α : Type ?u.303162
β : Type ?u.303165
γ : Type ?u.303168
a✝ b c✝ d : ℝ≥0∞
r p q : ℝ≥0
x y z ε✝ ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
f g : α → ℝ≥0∞
ι : Type u_1
a : ι → ℝ≥0∞
c : ℝ≥0∞
c_ne_top : c ≠ ⊤
tsum_le_c : (∑' (i : ι), a i) ≤ c
ε : ℝ≥0∞
ε_ne_zero : ε ≠ 0
hf : Set.Finite {i | ε ≤ a i}
⊢ ∃ hf, ↑(Finset.card (Finite.toFinset hf)) ≤ c / ε
α : Type ?u.303162
β : Type ?u.303165
γ : Type ?u.303168
a✝ b c✝ d : ℝ≥0∞
r p q : ℝ≥0
x y z ε✝ ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
f g : α → ℝ≥0∞
ι : Type u_1
a : ι → ℝ≥0∞
c : ℝ≥0∞
c_ne_top : c ≠ ⊤
tsum_le_c : (∑' (i : ι), a i) ≤ c
ε : ℝ≥0∞
ε_ne_zero : ε ≠ 0
⊢ ∃ hf, ↑(Finset.card (Finite.toFinset hf)) ≤ c / ε
have hf : { i : ι | ε ≤ a i }.Finite :=
  finite_const_le_of_tsum_ne_top (ne_top_of_le_ne_top c_ne_top tsum_le_c) ε_ne_zero
α : Type ?u.303162
β : Type ?u.303165
γ : Type ?u.303168
a✝ b c✝ d : ℝ≥0∞
r p q : ℝ≥0
x y z ε✝ ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
f g : α → ℝ≥0∞
ι : Type u_1
a : ι → ℝ≥0∞
c : ℝ≥0∞
c_ne_top : c ≠ ⊤
tsum_le_c : (∑' (i : ι), a i) ≤ c
ε : ℝ≥0∞
ε_ne_zero : ε ≠ 0
hf : Set.Finite {i | ε ≤ a i}
⊢ ↑(Finset.card (Finite.toFinset hf)) * ε ≤ c
α : Type ?u.303162
β : Type ?u.303165
γ : Type ?u.303168
a✝ b c✝ d : ℝ≥0∞
r p q : ℝ≥0
x y z ε✝ ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
f g : α → ℝ≥0∞
ι : Type u_1
a : ι → ℝ≥0∞
c : ℝ≥0∞
c_ne_top : c ≠ ⊤
tsum_le_c : (∑' (i : ι), a i) ≤ c
ε : ℝ≥0∞
ε_ne_zero : ε ≠ 0
hf : Set.Finite {i | ε ≤ a i}
⊢ ∃ hf, ↑(Finset.card (Finite.toFinset hf)) ≤ c / ε
refine ⟨hf, (ENNReal.le_div_iff_mul_le (.inl ε_ne_zero) (.inr c_ne_top)).2 ?_⟩
no goals
α : Type ?u.303162
β : Type ?u.303165
γ : Type ?u.303168
a✝ b c✝ d : ℝ≥0∞
r p q : ℝ≥0
x y z ε✝ ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
f g : α → ℝ≥0∞
ι : Type u_1
a : ι → ℝ≥0∞
c : ℝ≥0∞
c_ne_top : c ≠ ⊤
tsum_le_c : (∑' (i : ι), a i) ≤ c
ε : ℝ≥0∞
ε_ne_zero : ε ≠ 0
hf : Set.Finite {i | ε ≤ a i}
⊢ ↑(Finset.card (Finite.toFinset hf)) * ε ≤ c
calc ↑hf.toFinset.card * ε = ∑ _i in hf.toFinset, ε := by rw [Finset.sum_const, nsmul_eq_mul]
  _ ≤ ∑ i in hf.toFinset, a i := Finset.sum_le_sum fun i => hf.mem_toFinset.1
  _ ≤ ∑' i, a i := ENNReal.sum_le_tsum _
  _ ≤ c := tsum_le_c
no goals
α : Type ?u.303162
β : Type ?u.303165
γ : Type ?u.303168
a✝ b c✝ d : ℝ≥0∞
r p q : ℝ≥0
x y z ε✝ ε₁ ε₂ : ℝ≥0∞
s : Set ℝ≥0∞
f g : α → ℝ≥0∞
ι : Type u_1
a : ι → ℝ≥0∞
c : ℝ≥0∞
c_ne_top : c ≠ ⊤
tsum_le_c : (∑' (i : ι), a i) ≤ c
ε : ℝ≥0∞
ε_ne_zero : ε ≠ 0
hf : Set.Finite {i | ε ≤ a i}
⊢ ↑(Finset.card (Finite.toFinset hf)) * ε = ∑ _i in Finite.toFinset hf, ε
rw [Finset.sum_const, nsmul_eq_mul]