rw [Finset.sum_const, nsmul_eq_mul, mul_one,
  ← (finite_of_encard_eq_coe hsc).encard_eq_coe_toFinset_card, hsc, Nat.cast_lt]
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_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 < b + 1