rwa [indicator_apply_eq_self.2 (fun h ↦ (h hi).elim), Pi.one_apply, ENat.one_le_iff_ne_zero]
case pos
α : Type u_1
β : Type u_2
ι : Type u_3
s : Set α
f : α → ℕ∞
i : α
hi : i ∈ support f
⊢ (support f).indicator 1 i ≤ f i
no goals