rwa [← Finset.card_pos]
A B : Set ℕ
n : ℕ
hA : 0 ∈ A
hB : 0 ∈ B
hc : n ≤ countelements A (n - 1) + countelements B (n - 1)
h : n ∉ A + B
hnA : n ∉ A
hnB : n ∉ B
hca : countelements A (n - 1) = countelements A n
hcb : countelements B (n - 1) = countelements B n
hn1 : n > 0
lem1 : (filter (fun x => x ∈ {n} - B) (Ioo 0 n)).card = countelements B (n - 1)
hun : (filter (fun x => x ∈ A) (Ioo 0 n) ∪ filter (fun x => x ∈ {n} - B) (Ioo 0 n)).card ≤ n - 1
hui :
  (filter (fun x => x ∈ A) (Ioo 0 n) ∪ filter (fun x => x ∈ {n} - B) (Ioo 0 n)).card +
      (filter (fun x => x ∈ A) (Ioo 0 n) ∩ filter (fun x => x ∈ {n} - B) (Ioo 0 n)).card =
    countelements A (n - 1) + countelements B (n - 1)
hin : 0 < (filter (fun x => x ∈ A) (Ioo 0 n) ∩ filter (fun x => x ∈ {n} - B) (Ioo 0 n)).card
⊢ (filter (fun x => x ∈ A) (Ioo 0 n) ∩ filter (fun x => x ∈ {n} - B) (Ioo 0 n)).Nonempty
no goals