chore: generalise ENat.iInf_eq_zero (#23180) Previously, it had f : ι → ℕ. Also make it simp.
ENat.iInf_eq_zero
f : ι → ℕ