Theorem: sumset_contains_n (LeanCamCombi/Mathlib/Combinatorics/Schnirelmann.lean)

State before:
A B : Set ℕ
n : ℕ
hA : 0 ∈ A
hB : 0 ∈ B
hc : n ≤ countelements A n + countelements B n
⊢ n ∈ A + B
Tactic:
by_contra! h
State after:
A B : Set ℕ
n : ℕ
hA : 0 ∈ A
hB : 0 ∈ B
hc : n ≤ countelements A n + countelements B n
h : n ∉ A + B
⊢ False

State before:
A B : Set ℕ
n : ℕ
hA : 0 ∈ A
hB : 0 ∈ B
hc : n ≤ countelements A n + countelements B n
h : n ∉ A + B
⊢ False
Tactic:
have hnA : n ∉ A := Set.not_mem_subset (Set.subset_add_left _ hB) h
State after:
A B : Set ℕ
n : ℕ
hA : 0 ∈ A
hB : 0 ∈ B
hc : n ≤ countelements A n + countelements B n
h : n ∉ A + B
hnA : n ∉ A
⊢ False

State before:
A B : Set ℕ
n : ℕ
hA : 0 ∈ A
hB : 0 ∈ B
hc : n ≤ countelements A n + countelements B n
h : n ∉ A + B
hnA : n ∉ A
⊢ False
Tactic:
have hnB : n ∉ B := Set.not_mem_subset (Set.subset_add_right _ hA) h
State after:
A B : Set ℕ
n : ℕ
hA : 0 ∈ A
hB : 0 ∈ B
hc : n ≤ countelements A n + countelements B n
h : n ∉ A + B
hnA : n ∉ A
hnB : n ∉ B
⊢ False

State before:
A B : Set ℕ
n : ℕ
hA : 0 ∈ A
hB : 0 ∈ B
hc : n ≤ countelements A n + countelements B n
h : n ∉ A + B
hnA : n ∉ A
hnB : n ∉ B
⊢ False
Tactic:
have hca : countelements A (n - 1) = countelements A n := countelements_pred hnA
State after:
A B : Set ℕ
n : ℕ
hA : 0 ∈ A
hB : 0 ∈ B
hc : n ≤ countelements A n + countelements B n
h : n ∉ A + B
hnA : n ∉ A
hnB : n ∉ B
hca : countelements A (n - 1) = countelements A n
⊢ False

State before:
A B : Set ℕ
n : ℕ
hA : 0 ∈ A
hB : 0 ∈ B
hc : n ≤ countelements A n + countelements B n
h : n ∉ A + B
hnA : n ∉ A
hnB : n ∉ B
hca : countelements A (n - 1) = countelements A n
⊢ False
Tactic:
have hcb : countelements B (n - 1) = countelements B n := countelements_pred hnB
State after:
A B : Set ℕ
n : ℕ
hA : 0 ∈ A
hB : 0 ∈ B
hc : n ≤ countelements A n + countelements B n
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
⊢ False

State before:
A B : Set ℕ
n : ℕ
hA : 0 ∈ A
hB : 0 ∈ B
hc : n ≤ countelements A n + countelements B n
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
⊢ False
Tactic:
obtain rfl | hn1 := n.eq_zero_or_pos
State after:
case inl
A B : Set ℕ
hA : 0 ∈ A
hB : 0 ∈ B
hc : 0 ≤ countelements A 0 + countelements B 0
h : 0 ∉ A + B
hnA : 0 ∉ A
hnB : 0 ∉ B
hca : countelements A (0 - 1) = countelements A 0
hcb : countelements B (0 - 1) = countelements B 0
⊢ False

case inr
A B : Set ℕ
n : ℕ
hA : 0 ∈ A
hB : 0 ∈ B
hc : n ≤ countelements A n + countelements B n
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
⊢ False

State before:
case inr
A B : Set ℕ
n : ℕ
hA : 0 ∈ A
hB : 0 ∈ B
hc : n ≤ countelements A n + countelements B n
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
⊢ False
Tactic:
apply h
State after:
case inr
A B : Set ℕ
n : ℕ
hA : 0 ∈ A
hB : 0 ∈ B
hc : n ≤ countelements A n + countelements B n
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
⊢ n ∈ A + B

State before:
case inr
A B : Set ℕ
n : ℕ
hA : 0 ∈ A
hB : 0 ∈ B
hc : n ≤ countelements A n + countelements B n
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)
lem3 : (filter (fun x => x ∈ A) (Ioo 0 n) ∩ filter (fun x => x ∈ {n} - B) (Ioo 0 n)).Nonempty
⊢ n ∈ A + B
Tactic:
simp only [Nat.lt_one_iff, tsub_eq_zero_iff_le, mem_Ioo, and_imp, Set.singleton_sub,
  Set.mem_image, ne_eq] at lem3
State after:
case inr
A B : Set ℕ
n : ℕ
hA : 0 ∈ A
hB : 0 ∈ B
hc : n ≤ countelements A n + countelements B n
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)
lem3 : (filter (fun x => x ∈ A) (Ioo 0 n) ∩ filter (fun x => ∃ x_1 ∈ B, n - x_1 = x) (Ioo 0 n)).Nonempty
⊢ n ∈ A + B

State before:
case inr
A B : Set ℕ
n : ℕ
hA : 0 ∈ A
hB : 0 ∈ B
hc : n ≤ countelements A n + countelements B n
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)
lem3 : (filter (fun x => x ∈ A) (Ioo 0 n) ∩ filter (fun x => ∃ x_1 ∈ B, n - x_1 = x) (Ioo 0 n)).Nonempty
⊢ n ∈ A + B
Tactic:
have lem31 : (A ∩ ({n} - B) ∩ Set.Ioo 0 n).Nonempty := by
  rw [← filter_and, ← coe_nonempty, coe_filter, Set.setOf_and, Set.setOf_and, Set.setOf_mem_eq,
    Set.inter_comm] at lem3
  convert lem3 using 3 <;> ext <;> simp
State after:
case inr
A B : Set ℕ
n : ℕ
hA : 0 ∈ A
hB : 0 ∈ B
hc : n ≤ countelements A n + countelements B n
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)
lem3 : (filter (fun x => x ∈ A) (Ioo 0 n) ∩ filter (fun x => ∃ x_1 ∈ B, n - x_1 = x) (Ioo 0 n)).Nonempty
lem31 : (A ∩ ({n} - B) ∩ Set.Ioo 0 n).Nonempty
⊢ n ∈ A + B

State before:
case inr
A B : Set ℕ
n : ℕ
hA : 0 ∈ A
hB : 0 ∈ B
hc : n ≤ countelements A n + countelements B n
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)
lem3 : (filter (fun x => x ∈ A) (Ioo 0 n) ∩ filter (fun x => ∃ x_1 ∈ B, n - x_1 = x) (Ioo 0 n)).Nonempty
lem31 : (A ∩ ({n} - B) ∩ Set.Ioo 0 n).Nonempty
⊢ n ∈ A + B
Tactic:
obtain ⟨_, ⟨hxA, n, rfl, x, hxB, rfl⟩, hx⟩ := lem31
State after:
case inr.intro.intro.intro.intro.intro.intro.intro
A B : Set ℕ
hA : 0 ∈ A
hB : 0 ∈ B
n : ℕ
hc : n ≤ countelements A n + countelements B n
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)
lem3 : (filter (fun x => x ∈ A) (Ioo 0 n) ∩ filter (fun x => ∃ x_1 ∈ B, n - x_1 = x) (Ioo 0 n)).Nonempty
x : ℕ
hxB : x ∈ B
hxA : (fun x x_1 => x - x_1) n x ∈ A
hx : (fun x x_1 => x - x_1) n x ∈ Set.Ioo 0 n
⊢ n ∈ A + B

State before:
case inr.intro.intro.intro.intro.intro.intro.intro
A B : Set ℕ
hA : 0 ∈ A
hB : 0 ∈ B
n : ℕ
hc : n ≤ countelements A n + countelements B n
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)
lem3 : (filter (fun x => x ∈ A) (Ioo 0 n) ∩ filter (fun x => ∃ x_1 ∈ B, n - x_1 = x) (Ioo 0 n)).Nonempty
x : ℕ
hxB : x ∈ B
hxA : (fun x x_1 => x - x_1) n x ∈ A
hx : (fun x x_1 => x - x_1) n x ∈ Set.Ioo 0 n
⊢ n ∈ A + B
Tactic:
simp only [Set.mem_Ioo, Nat.succ_le_iff, tsub_pos_iff_lt, tsub_le_iff_right] at hx
State after:
case inr.intro.intro.intro.intro.intro.intro.intro
A B : Set ℕ
hA : 0 ∈ A
hB : 0 ∈ B
n : ℕ
hc : n ≤ countelements A n + countelements B n
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)
lem3 : (filter (fun x => x ∈ A) (Ioo 0 n) ∩ filter (fun x => ∃ x_1 ∈ B, n - x_1 = x) (Ioo 0 n)).Nonempty
x : ℕ
hxB : x ∈ B
hxA : (fun x x_1 => x - x_1) n x ∈ A
hx : x < n ∧ n - x < n
⊢ n ∈ A + B

State before:
case inr.intro.intro.intro.intro.intro.intro.intro
A B : Set ℕ
hA : 0 ∈ A
hB : 0 ∈ B
n : ℕ
hc : n ≤ countelements A n + countelements B n
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)
lem3 : (filter (fun x => x ∈ A) (Ioo 0 n) ∩ filter (fun x => ∃ x_1 ∈ B, n - x_1 = x) (Ioo 0 n)).Nonempty
x : ℕ
hxB : x ∈ B
hxA : (fun x x_1 => x - x_1) n x ∈ A
hx : x < n ∧ n - x < n
⊢ n ∈ A + B
Tactic:
exact ⟨_, hxA, x, hxB, tsub_add_cancel_of_le hx.1.le⟩
State after:
no goals

State before:
case inl
A B : Set ℕ
hA : 0 ∈ A
hB : 0 ∈ B
hc : 0 ≤ countelements A 0 + countelements B 0
h : 0 ∉ A + B
hnA : 0 ∉ A
hnB : 0 ∉ B
hca : countelements A (0 - 1) = countelements A 0
hcb : countelements B (0 - 1) = countelements B 0
⊢ False
Tactic:
contradiction
State after:
no goals

State before:
A B : Set ℕ
n : ℕ
hA : 0 ∈ A
hB : 0 ∈ B
hc : n ≤ countelements A n + countelements B n
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
⊢ (filter (fun x => x ∈ {n} - B) (Ioo 0 n)).card = countelements B (n - 1)
Tactic:
rw [countelements]
State after:
A B : Set ℕ
n : ℕ
hA : 0 ∈ A
hB : 0 ∈ B
hc : n ≤ countelements A n + countelements B n
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
⊢ (filter (fun x => x ∈ {n} - B) (Ioo 0 n)).card = (filter (fun x => x ∈ B) (Icc 1 (n - 1))).card

State before:
A B : Set ℕ
n : ℕ
hA : 0 ∈ A
hB : 0 ∈ B
hc : n ≤ countelements A n + countelements B n
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
hfim : image (fun x => n - x) (filter (fun x => x ∈ B) (Ioo 0 n)) = filter (fun x => x ∈ {n} - B) (Ioo 0 n)
⊢ (filter (fun x => x ∈ {n} - B) (Ioo 0 n)).card = (filter (fun x => x ∈ B) (Icc 1 (n - 1))).card
Tactic:
rw [← hfim, card_image_of_injOn]
State after:
A B : Set ℕ
n : ℕ
hA : 0 ∈ A
hB : 0 ∈ B
hc : n ≤ countelements A n + countelements B n
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
hfim : image (fun x => n - x) (filter (fun x => x ∈ B) (Ioo 0 n)) = filter (fun x => x ∈ {n} - B) (Ioo 0 n)
⊢ (filter (fun x => x ∈ B) (Ioo 0 n)).card = (filter (fun x => x ∈ B) (Icc 1 (n - 1))).card

A B : Set ℕ
n : ℕ
hA : 0 ∈ A
hB : 0 ∈ B
hc : n ≤ countelements A n + countelements B n
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
hfim : image (fun x => n - x) (filter (fun x => x ∈ B) (Ioo 0 n)) = filter (fun x => x ∈ {n} - B) (Ioo 0 n)
⊢ Set.InjOn (fun x => n - x) ↑(filter (fun x => x ∈ B) (Ioo 0 n))

State before:
A B : Set ℕ
n : ℕ
hA : 0 ∈ A
hB : 0 ∈ B
hc : n ≤ countelements A n + countelements B n
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
hfim : image (fun x => n - x) (filter (fun x => x ∈ B) (Ioo 0 n)) = filter (fun x => x ∈ {n} - B) (Ioo 0 n)
⊢ (filter (fun x => x ∈ B) (Ioo 0 n)).card = (filter (fun x => x ∈ B) (Icc 1 (n - 1))).card

A B : Set ℕ
n : ℕ
hA : 0 ∈ A
hB : 0 ∈ B
hc : n ≤ countelements A n + countelements B n
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
hfim : image (fun x => n - x) (filter (fun x => x ∈ B) (Ioo 0 n)) = filter (fun x => x ∈ {n} - B) (Ioo 0 n)
⊢ Set.InjOn (fun x => n - x) ↑(filter (fun x => x ∈ B) (Ioo 0 n))
Tactic:
congr
State after:
case e_s.e_s.e_b
A B : Set ℕ
n : ℕ
hA : 0 ∈ A
hB : 0 ∈ B
hc : n ≤ countelements A n + countelements B n
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
hfim : image (fun x => n - x) (filter (fun x => x ∈ B) (Ioo 0 n)) = filter (fun x => x ∈ {n} - B) (Ioo 0 n)
⊢ n = ((n - 1).add 0).succ

A B : Set ℕ
n : ℕ
hA : 0 ∈ A
hB : 0 ∈ B
hc : n ≤ countelements A n + countelements B n
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
hfim : image (fun x => n - x) (filter (fun x => x ∈ B) (Ioo 0 n)) = filter (fun x => x ∈ {n} - B) (Ioo 0 n)
⊢ Set.InjOn (fun x => n - x) ↑(filter (fun x => x ∈ B) (Ioo 0 n))

State before:
case e_s.e_s.e_b
A B : Set ℕ
n : ℕ
hA : 0 ∈ A
hB : 0 ∈ B
hc : n ≤ countelements A n + countelements B n
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
hfim : image (fun x => n - x) (filter (fun x => x ∈ B) (Ioo 0 n)) = filter (fun x => x ∈ {n} - B) (Ioo 0 n)
⊢ n = ((n - 1).add 0).succ

A B : Set ℕ
n : ℕ
hA : 0 ∈ A
hB : 0 ∈ B
hc : n ≤ countelements A n + countelements B n
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
hfim : image (fun x => n - x) (filter (fun x => x ∈ B) (Ioo 0 n)) = filter (fun x => x ∈ {n} - B) (Ioo 0 n)
⊢ Set.InjOn (fun x => n - x) ↑(filter (fun x => x ∈ B) (Ioo 0 n))
Tactic:
exact (tsub_add_cancel_of_le $ Nat.succ_le_iff.2 hn1).symm
State after:
A B : Set ℕ
n : ℕ
hA : 0 ∈ A
hB : 0 ∈ B
hc : n ≤ countelements A n + countelements B n
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
hfim : image (fun x => n - x) (filter (fun x => x ∈ B) (Ioo 0 n)) = filter (fun x => x ∈ {n} - B) (Ioo 0 n)
⊢ Set.InjOn (fun x => n - x) ↑(filter (fun x => x ∈ B) (Ioo 0 n))

State before:
A B : Set ℕ
n : ℕ
hA : 0 ∈ A
hB : 0 ∈ B
hc : n ≤ countelements A n + countelements B n
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
⊢ image (fun x => n - x) (filter (fun x => x ∈ B) (Ioo 0 n)) = filter (fun x => x ∈ {n} - B) (Ioo 0 n)
Tactic:
ext
State after:
case a
A B : Set ℕ
n : ℕ
hA : 0 ∈ A
hB : 0 ∈ B
hc : n ≤ countelements A n + countelements B n
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
a✝ : ℕ
⊢ a✝ ∈ image (fun x => n - x) (filter (fun x => x ∈ B) (Ioo 0 n)) ↔ a✝ ∈ filter (fun x => x ∈ {n} - B) (Ioo 0 n)

State before:
case a
A B : Set ℕ
n : ℕ
hA : 0 ∈ A
hB : 0 ∈ B
hc : n ≤ countelements A n + countelements B n
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
a✝ : ℕ
⊢ a✝ ∈ image (fun x => n - x) (filter (fun x => x ∈ B) (Ioo 0 n)) ↔ a✝ ∈ filter (fun x => x ∈ {n} - B) (Ioo 0 n)
Tactic:
aesop
State after:
no goals

State before:
A B : Set ℕ
n : ℕ
hA : 0 ∈ A
hB : 0 ∈ B
hc : n ≤ countelements A n + countelements B n
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
hfim : image (fun x => n - x) (filter (fun x => x ∈ B) (Ioo 0 n)) = filter (fun x => x ∈ {n} - B) (Ioo 0 n)
⊢ Set.InjOn (fun x => n - x) ↑(filter (fun x => x ∈ B) (Ioo 0 n))
Tactic:
exact Set.InjOn.mono (fun x hx ↦ (mem_Ioo.1 (mem_filter.1 hx).1).2.le) $
  fun x hx y hy ↦ tsub_inj_right hx hy
State after:
no goals

State before:
A B : Set ℕ
n : ℕ
hA : 0 ∈ A
hB : 0 ∈ B
hc : n ≤ countelements A n + countelements B n
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)
⊢ (filter (fun x => x ∈ A) (Ioo 0 n) ∩ filter (fun x => x ∈ {n} - B) (Ioo 0 n)).Nonempty
Tactic:
rw [← hca, ← hcb] at hc
State after:
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)
⊢ (filter (fun x => x ∈ A) (Ioo 0 n) ∩ filter (fun x => x ∈ {n} - B) (Ioo 0 n)).Nonempty

State before:
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
Tactic:
rwa [← Finset.card_pos]
State after:
no goals

State before:
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)
⊢ (filter (fun x => x ∈ A) (Ioo 0 n) ∪ filter (fun x => x ∈ {n} - B) (Ioo 0 n)).card ≤ n - 1
Tactic:
rw [← filter_or, ← tsub_zero n, ← Nat.card_Ioo]
State after:
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)
⊢ (filter (fun a => a ∈ A ∨ a ∈ {n - 0} - B) (Ioo 0 (n - 0))).card ≤ (Ioo 0 n).card

State before:
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)
⊢ (filter (fun a => a ∈ A ∨ a ∈ {n - 0} - B) (Ioo 0 (n - 0))).card ≤ (Ioo 0 n).card
Tactic:
exact card_filter_le _ _
State after:
no goals

State before:
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
⊢ (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)
Tactic:
rw [card_union_add_card_inter, ← lem1, countelements]
State after:
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
⊢ (filter (fun x => x ∈ A) (Ioo 0 n)).card + (filter (fun x => x ∈ {n} - B) (Ioo 0 n)).card =
    (filter (fun x => x ∈ A) (Icc 1 (n - 1))).card + (filter (fun x => x ∈ {n} - B) (Ioo 0 n)).card

State before:
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
⊢ (filter (fun x => x ∈ A) (Ioo 0 n)).card + (filter (fun x => x ∈ {n} - B) (Ioo 0 n)).card =
    (filter (fun x => x ∈ A) (Icc 1 (n - 1))).card + (filter (fun x => x ∈ {n} - B) (Ioo 0 n)).card
Tactic:
congr
State after:
case e_a.e_s.e_s.e_b
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
⊢ n = ((n - 1).add 0).succ

State before:
case e_a.e_s.e_s.e_b
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
⊢ n = ((n - 1).add 0).succ
Tactic:
exact (tsub_add_cancel_of_le $ Nat.succ_le_iff.2 hn1).symm
State after:
no goals

State before:
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)
⊢ 0 < (filter (fun x => x ∈ A) (Ioo 0 n) ∩ filter (fun x => x ∈ {n} - B) (Ioo 0 n)).card
Tactic:
rw [← hui] at hc
State after:
A B : Set ℕ
n : ℕ
hA : 0 ∈ A
hB : 0 ∈ B
hc :
  n ≤
    (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
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)
⊢ 0 < (filter (fun x => x ∈ A) (Ioo 0 n) ∩ filter (fun x => x ∈ {n} - B) (Ioo 0 n)).card

State before:
A B : Set ℕ
n : ℕ
hA : 0 ∈ A
hB : 0 ∈ B
hc :
  n ≤
    (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
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)
hun1 :
  (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 ≤
    n - 1 + (filter (fun x => x ∈ A) (Ioo 0 n) ∩ filter (fun x => x ∈ {n} - B) (Ioo 0 n)).card
hip0 : n ≤ n - 1 + (filter (fun x => x ∈ A) (Ioo 0 n) ∩ filter (fun x => x ∈ {n} - B) (Ioo 0 n)).card
⊢ 0 < (filter (fun x => x ∈ A) (Ioo 0 n) ∩ filter (fun x => x ∈ {n} - B) (Ioo 0 n)).card
Tactic:
by_contra! hip
State after:
A B : Set ℕ
n : ℕ
hA : 0 ∈ A
hB : 0 ∈ B
hc :
  n ≤
    (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
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)
hun1 :
  (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 ≤
    n - 1 + (filter (fun x => x ∈ A) (Ioo 0 n) ∩ filter (fun x => x ∈ {n} - B) (Ioo 0 n)).card
hip0 : n ≤ n - 1 + (filter (fun x => x ∈ A) (Ioo 0 n) ∩ filter (fun x => x ∈ {n} - B) (Ioo 0 n)).card
hip : (filter (fun x => x ∈ A) (Ioo 0 n) ∩ filter (fun x => x ∈ {n} - B) (Ioo 0 n)).card ≤ 0
⊢ False

State before:
A B : Set ℕ
n : ℕ
hA : 0 ∈ A
hB : 0 ∈ B
hc :
  n ≤
    (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
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)
hun1 :
  (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 ≤
    n - 1 + (filter (fun x => x ∈ A) (Ioo 0 n) ∩ filter (fun x => x ∈ {n} - B) (Ioo 0 n)).card
hip0 : n ≤ n - 1 + (filter (fun x => x ∈ A) (Ioo 0 n) ∩ filter (fun x => x ∈ {n} - B) (Ioo 0 n)).card
hip : (filter (fun x => x ∈ A) (Ioo 0 n) ∩ filter (fun x => x ∈ {n} - B) (Ioo 0 n)).card ≤ 0
hip1 : n - 1 + (filter (fun x => x ∈ A) (Ioo 0 n) ∩ filter (fun x => x ∈ {n} - B) (Ioo 0 n)).card ≤ n - 1
⊢ False
Tactic:
have hnn : n ≤ (n - 1) := le_trans hip0 hip1
State after:
A B : Set ℕ
n : ℕ
hA : 0 ∈ A
hB : 0 ∈ B
hc :
  n ≤
    (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
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)
hun1 :
  (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 ≤
    n - 1 + (filter (fun x => x ∈ A) (Ioo 0 n) ∩ filter (fun x => x ∈ {n} - B) (Ioo 0 n)).card
hip0 : n ≤ n - 1 + (filter (fun x => x ∈ A) (Ioo 0 n) ∩ filter (fun x => x ∈ {n} - B) (Ioo 0 n)).card
hip : (filter (fun x => x ∈ A) (Ioo 0 n) ∩ filter (fun x => x ∈ {n} - B) (Ioo 0 n)).card ≤ 0
hip1 : n - 1 + (filter (fun x => x ∈ A) (Ioo 0 n) ∩ filter (fun x => x ∈ {n} - B) (Ioo 0 n)).card ≤ n - 1
hnn : n ≤ n - 1
⊢ False

State before:
A B : Set ℕ
n : ℕ
hA : 0 ∈ A
hB : 0 ∈ B
hc :
  n ≤
    (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
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)
hun1 :
  (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 ≤
    n - 1 + (filter (fun x => x ∈ A) (Ioo 0 n) ∩ filter (fun x => x ∈ {n} - B) (Ioo 0 n)).card
hip0 : n ≤ n - 1 + (filter (fun x => x ∈ A) (Ioo 0 n) ∩ filter (fun x => x ∈ {n} - B) (Ioo 0 n)).card
hip : (filter (fun x => x ∈ A) (Ioo 0 n) ∩ filter (fun x => x ∈ {n} - B) (Ioo 0 n)).card ≤ 0
hip1 : n - 1 + (filter (fun x => x ∈ A) (Ioo 0 n) ∩ filter (fun x => x ∈ {n} - B) (Ioo 0 n)).card ≤ n - 1
hnn : n ≤ n - 1
⊢ False
Tactic:
rw [← not_lt] at hnn
State after:
A B : Set ℕ
n : ℕ
hA : 0 ∈ A
hB : 0 ∈ B
hc :
  n ≤
    (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
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)
hun1 :
  (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 ≤
    n - 1 + (filter (fun x => x ∈ A) (Ioo 0 n) ∩ filter (fun x => x ∈ {n} - B) (Ioo 0 n)).card
hip0 : n ≤ n - 1 + (filter (fun x => x ∈ A) (Ioo 0 n) ∩ filter (fun x => x ∈ {n} - B) (Ioo 0 n)).card
hip : (filter (fun x => x ∈ A) (Ioo 0 n) ∩ filter (fun x => x ∈ {n} - B) (Ioo 0 n)).card ≤ 0
hip1 : n - 1 + (filter (fun x => x ∈ A) (Ioo 0 n) ∩ filter (fun x => x ∈ {n} - B) (Ioo 0 n)).card ≤ n - 1
hnn : ¬n - 1 < n
⊢ False

State before:
A B : Set ℕ
n : ℕ
hA : 0 ∈ A
hB : 0 ∈ B
hc :
  n ≤
    (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
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)
hun1 :
  (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 ≤
    n - 1 + (filter (fun x => x ∈ A) (Ioo 0 n) ∩ filter (fun x => x ∈ {n} - B) (Ioo 0 n)).card
hip0 : n ≤ n - 1 + (filter (fun x => x ∈ A) (Ioo 0 n) ∩ filter (fun x => x ∈ {n} - B) (Ioo 0 n)).card
hip : (filter (fun x => x ∈ A) (Ioo 0 n) ∩ filter (fun x => x ∈ {n} - B) (Ioo 0 n)).card ≤ 0
hip1 : n - 1 + (filter (fun x => x ∈ A) (Ioo 0 n) ∩ filter (fun x => x ∈ {n} - B) (Ioo 0 n)).card ≤ n - 1
hnn : ¬n - 1 < n
⊢ False
Tactic:
apply hnn
State after:
A B : Set ℕ
n : ℕ
hA : 0 ∈ A
hB : 0 ∈ B
hc :
  n ≤
    (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
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)
hun1 :
  (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 ≤
    n - 1 + (filter (fun x => x ∈ A) (Ioo 0 n) ∩ filter (fun x => x ∈ {n} - B) (Ioo 0 n)).card
hip0 : n ≤ n - 1 + (filter (fun x => x ∈ A) (Ioo 0 n) ∩ filter (fun x => x ∈ {n} - B) (Ioo 0 n)).card
hip : (filter (fun x => x ∈ A) (Ioo 0 n) ∩ filter (fun x => x ∈ {n} - B) (Ioo 0 n)).card ≤ 0
hip1 : n - 1 + (filter (fun x => x ∈ A) (Ioo 0 n) ∩ filter (fun x => x ∈ {n} - B) (Ioo 0 n)).card ≤ n - 1
hnn : ¬n - 1 < n
⊢ n - 1 < n

State before:
A B : Set ℕ
n : ℕ
hA : 0 ∈ A
hB : 0 ∈ B
hc :
  n ≤
    (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
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)
hun1 :
  (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 ≤
    n - 1 + (filter (fun x => x ∈ A) (Ioo 0 n) ∩ filter (fun x => x ∈ {n} - B) (Ioo 0 n)).card
hip0 : n ≤ n - 1 + (filter (fun x => x ∈ A) (Ioo 0 n) ∩ filter (fun x => x ∈ {n} - B) (Ioo 0 n)).card
hip : (filter (fun x => x ∈ A) (Ioo 0 n) ∩ filter (fun x => x ∈ {n} - B) (Ioo 0 n)).card ≤ 0
hip1 : n - 1 + (filter (fun x => x ∈ A) (Ioo 0 n) ∩ filter (fun x => x ∈ {n} - B) (Ioo 0 n)).card ≤ n - 1
hnn : ¬n - 1 < n
⊢ n - 1 < n
Tactic:
rw [propext (Nat.lt_iff_le_pred hn1)]
State after:
no goals

State before:
A B : Set ℕ
n : ℕ
hA : 0 ∈ A
hB : 0 ∈ B
hc : n ≤ countelements A n + countelements B n
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)
lem3 : (filter (fun x => x ∈ A) (Ioo 0 n) ∩ filter (fun x => ∃ x_1 ∈ B, n - x_1 = x) (Ioo 0 n)).Nonempty
⊢ (A ∩ ({n} - B) ∩ Set.Ioo 0 n).Nonempty
Tactic:
rw [← filter_and, ← coe_nonempty, coe_filter, Set.setOf_and, Set.setOf_and, Set.setOf_mem_eq,
  Set.inter_comm] at lem3
State after:
A B : Set ℕ
n : ℕ
hA : 0 ∈ A
hB : 0 ∈ B
hc : n ≤ countelements A n + countelements B n
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)
lem3 : (A ∩ {a | ∃ x ∈ B, n - x = a} ∩ {a | a ∈ Ioo 0 n}).Nonempty
⊢ (A ∩ ({n} - B) ∩ Set.Ioo 0 n).Nonempty

State before:
A B : Set ℕ
n : ℕ
hA : 0 ∈ A
hB : 0 ∈ B
hc : n ≤ countelements A n + countelements B n
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)
lem3 : (A ∩ {a | ∃ x ∈ B, n - x = a} ∩ {a | a ∈ Ioo 0 n}).Nonempty
⊢ (A ∩ ({n} - B) ∩ Set.Ioo 0 n).Nonempty
Tactic:
convert lem3 using 3 <;> ext <;> simp
State after:
no goals