refine ⟨s', lt_of_lt_of_le ?_ (Finset.sum_le_sum (show ∀ i ∈ s', 1 ≤ f i from ?_))  ⟩
case intro.intro.intro
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
f g : α → ℕ∞
hf : (support f).Infinite
b : ℕ
hb : ↑b < ⊤
s : Set α
hss : s ⊆ support f
hsc : s.encard = ↑(b + 1)
s' : Finset α := ⋯.toFinset
⊢ ∃ i, ↑b < ∑ a ∈ i, f a
case intro.intro.intro.refine_1
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
f g : α → ℕ∞
hf : (support f).Infinite
b : ℕ
hb : ↑b < ⊤
s : Set α
hss : s ⊆ support f
hsc : s.encard = ↑(b + 1)
s' : Finset α := ⋯.toFinset
⊢ ↑b < ∑ i ∈ s', 1

case intro.intro.intro.refine_2
α : Type u_1
β : Type u_2
ι : Type u_3
s✝ : Set α
n : ℕ∞
f g : α → ℕ∞
hf : (support f).Infinite
b : ℕ
hb : ↑b < ⊤
s : Set α
hss : s ⊆ support f
hsc : s.encard = ↑(b + 1)
s' : Finset α := ⋯.toFinset
⊢ ∀ i ∈ s', 1 ≤ f i