rw [this, Nat.Ioc_filter_dvd_card_eq_div]
case e_a
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N y : ℕ
x✝ : y ∈ range (N + 1)
this : filter (fun x => x ≠ 0) (range (N + 1)) = Ioc 0 N
⊢ (filter (fun a => y ∣ a) (filter (fun a => a ≠ 0) (range (N + 1)))).card = N / y
no goals