simp_rw [mem_divisors, and_comm (b := _ ≠ 0), ← filter_filter]
case e_a
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N y : ℕ
x✝ : y ∈ range (N + 1)
⊢ (filter (fun x => y ∈ x.divisors) (range (N + 1))).card = N / y
case e_a
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N y : ℕ
x✝ : y ∈ range (N + 1)
⊢ (filter (fun a => y ∣ a) (filter (fun a => a ≠ 0) (range (N + 1)))).card = N / y