lift b to ℕ using hb.ne
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
n : ℕ∞
f g : α → ℕ∞
hf : (support f).Infinite
b : ℕ∞
hb : b < ⊤
⊢ ∃ i, b < ∑ a ∈ i, f a
case intro
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
n : ℕ∞
f g : α → ℕ∞
hf : (support f).Infinite
b : ℕ
hb : ↑b < ⊤
⊢ ∃ i, ↑b < ∑ a ∈ i, f a