@[simp]

theorem ENat.prod_eq_top {ι : Type u_1} {s : Finset ι} {f : ι → ℕ∞} : ∏ i ∈ s, f i = ⊤ ↔ (∃ i ∈ s, f i = ⊤) ∧ ∀ i ∈ s, f i ≠ 0