internlm/Lean-Github huggingface dataset:
Theorem: sumset_contains_n
Proof 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]
Proof 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))
Theorem: sumset_contains_n
Proof 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
Proof 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))
Theorem: sumset_contains_n
Proof 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
Proof 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))
Theorem: sumset_contains_n
Proof 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
Proof 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)
Theorem: sumset_contains_n
Proof 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
Proof state after:
no goals
Theorem: sumset_contains_n
Proof 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
Proof state after:
no goals
Theorem: sumset_contains_n
Proof 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
Proof 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
Theorem: sumset_contains_n
Proof 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]
Proof state after:
no goals
Theorem: sumset_contains_n
Proof 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]
Proof 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
Theorem: sumset_contains_n
Proof 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 _ _
Proof state after:
no goals
Theorem: sumset_contains_n
Proof 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]
Proof 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
Theorem: sumset_contains_n
Proof 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
Proof 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
Theorem: sumset_contains_n
Proof 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
Proof state after:
no goals
Theorem: sumset_contains_n
Proof 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
Proof 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
Theorem: sumset_contains_n
Proof 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
Proof 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
Theorem: sumset_contains_n
Proof 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
Proof 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
Theorem: sumset_contains_n
Proof 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
Proof 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