rw [mem_filter, mem_Icc] at hx
case refine_2
A B : Set ℕ
n : ℕ
hn : n ∉ A
x : ℕ
hx : x ∈ filter (fun x => x ∈ A) (Icc 1 n)
⊢ x ∈ Icc 1 (n - 1) ∧ x ∈ A
case refine_2
A B : Set ℕ
n : ℕ
hn : n ∉ A
x : ℕ
hx : (1 ≤ x ∧ x ≤ n) ∧ x ∈ A
⊢ x ∈ Icc 1 (n - 1) ∧ x ∈ A