rw [mem_filter]
case refine_2
A B : Set ℕ
n : ℕ
hn : n ∉ A
x : ℕ
hx : x ∈ filter (fun x => x ∈ A) (Icc 1 n)
⊢ x ∈ filter (fun x => x ∈ A) (Icc 1 (n - 1))
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