rw [divisors, mem_filter] at hd
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N x : ℕ
hx : x ∈ range (N + 1)
d : ℕ
hd : d ∈ x.divisors
⊢ d ≤ x
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N x : ℕ
hx : x ∈ range (N + 1)
d : ℕ
hd : d ∈ Ico 1 (x + 1) ∧ d ∣ x
⊢ d ≤ x