rw [mem_filter, mem_Ioc, mem_range, pos_iff_ne_zero, lt_succ, and_comm]
case a
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N y : ℕ
x✝ : y ∈ range (N + 1)
a : ℕ
⊢ a ∈ filter (fun x => x ≠ 0) (range (N + 1)) ↔ a ∈ Ioc 0 N
no goals