refine card_le_card fun x hx ↦ ?_
case refine_2
A B : Set ℕ
n : ℕ
hn : n ∉ A
⊢ (filter (fun x => x ∈ A) (Icc 1 n)).card ≤ (filter (fun x => x ∈ A) (Icc 1 (n - 1))).card
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))