refine Subset.antisymm ?_ ?_ <;> intro d hd
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N x : ℕ
hx : x ∈ range (N + 1)
⊢ filter (fun x_1 => x_1 ∈ x.divisors) (range (N + 1)) = x.divisors
case refine_1
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N x : ℕ
hx : x ∈ range (N + 1)
d : ℕ
hd : d ∈ filter (fun x_1 => x_1 ∈ x.divisors) (range (N + 1))
⊢ d ∈ x.divisors

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))