have h : d ≤ x := by
  rw [divisors, mem_filter] at hd
  exact lt_succ.mp (mem_Ico.mp hd.left).right
case refine_2
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N x : ℕ
hx : x ∈ range (N + 1)
d : ℕ
hd : d ∈ x.divisors
⊢ d ∈ filter (fun x_1 => x_1 ∈ x.divisors) (range (N + 1))
case refine_2
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N x : ℕ
hx : x ∈ range (N + 1)
d : ℕ
hd : d ∈ x.divisors
h : d ≤ x
⊢ d ∈ filter (fun x_1 => x_1 ∈ x.divisors) (range (N + 1))