rw [indicator_apply_eq_zero.2 (fun h ↦ (hi h).elim)]
case neg
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
f : α → ℕ∞
i : α
hi : i ∉ support f
⊢ (support f).indicator 1 i ≤ f i
case neg
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
f : α → ℕ∞
i : α
hi : i ∉ support f
⊢ 0 ≤ f i