internlm/Lean-Github huggingface dataset:
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 - 1 < n
⊢ False
Tactic:
apply 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
⊢ n - 1 < n
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 - 1 < n
⊢ n - 1 < n
Tactic:
rw [propext (Nat.lt_iff_le_pred hn1)]
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)
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
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
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
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)
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
Proof state after:
no goals
Theorem: sum_schnirelmannDensity_ge_one_sumset_nat
Proof state before:
A B : Set ℕ
n : ℕ
hA : 0 ∈ A
hB : 0 ∈ B
hAB : 1 ≤ schnirelmannDensity A + schnirelmannDensity B
⊢ A + B = Set.univ
Tactic:
refine Set.eq_univ_of_forall $ fun n ↦ sumset_contains_n hA hB ?_
Proof state after:
A B : Set ℕ
n✝ : ℕ
hA : 0 ∈ A
hB : 0 ∈ B
hAB : 1 ≤ schnirelmannDensity A + schnirelmannDensity B
n : ℕ
⊢ n ≤ countelements A n + countelements B n
Theorem: sum_schnirelmannDensity_ge_one_sumset_nat
Proof state before:
A B : Set ℕ
n✝ : ℕ
hA : 0 ∈ A
hB : 0 ∈ B
hAB : 1 ≤ schnirelmannDensity A + schnirelmannDensity B
n : ℕ
⊢ n ≤ countelements A n + countelements B n
Tactic:
obtain rfl | hn := eq_or_ne n 0
Proof state after:
case inl
A B : Set ℕ
n : ℕ
hA : 0 ∈ A
hB : 0 ∈ B
hAB : 1 ≤ schnirelmannDensity A + schnirelmannDensity B
⊢ 0 ≤ countelements A 0 + countelements B 0

case inr
A B : Set ℕ
n✝ : ℕ
hA : 0 ∈ A
hB : 0 ∈ B
hAB : 1 ≤ schnirelmannDensity A + schnirelmannDensity B
n : ℕ
hn : n ≠ 0
⊢ n ≤ countelements A n + countelements B n
Theorem: sum_schnirelmannDensity_ge_one_sumset_nat
Proof state before:
case inr
A B : Set ℕ
n✝ : ℕ
hA : 0 ∈ A
hB : 0 ∈ B
hAB : 1 ≤ schnirelmannDensity A + schnirelmannDensity B
n : ℕ
hn : n ≠ 0
⊢ n ≤ countelements A n + countelements B n
Tactic:
rw [← Nat.cast_le (α := ℝ), ← one_le_div (by positivity)]
Proof state after:
case inr
A B : Set ℕ
n✝ : ℕ
hA : 0 ∈ A
hB : 0 ∈ B
hAB : 1 ≤ schnirelmannDensity A + schnirelmannDensity B
n : ℕ
hn : n ≠ 0
⊢ 1 ≤ ↑(countelements A n + countelements B n) / ↑n
Theorem: sum_schnirelmannDensity_ge_one_sumset_nat
Proof state before:
case inr
A B : Set ℕ
n✝ : ℕ
hA : 0 ∈ A
hB : 0 ∈ B
hAB : 1 ≤ schnirelmannDensity A + schnirelmannDensity B
n : ℕ
hn : n ≠ 0
⊢ 1 ≤ ↑(countelements A n + countelements B n) / ↑n
Tactic:
calc
  _ ≤ _ := hAB
  _ ≤ _ := add_le_add (schnirelmannDensity_le_div hn) (schnirelmannDensity_le_div hn)
  _ = _ := by push_cast; rw [add_div]; rfl
Proof state after:
no goals
Theorem: sum_schnirelmannDensity_ge_one_sumset_nat
Proof state before:
case inl
A B : Set ℕ
n : ℕ
hA : 0 ∈ A
hB : 0 ∈ B
hAB : 1 ≤ schnirelmannDensity A + schnirelmannDensity B
⊢ 0 ≤ countelements A 0 + countelements B 0
Tactic:
exact countelements_nonneg A 0
Proof state after:
no goals
Theorem: sum_schnirelmannDensity_ge_one_sumset_nat
Proof state before:
A B : Set ℕ
n✝ : ℕ
hA : 0 ∈ A
hB : 0 ∈ B
hAB : 1 ≤ schnirelmannDensity A + schnirelmannDensity B
n : ℕ
hn : n ≠ 0
⊢ 0 < ↑n
Tactic:
positivity
Proof state after:
no goals
Theorem: sum_schnirelmannDensity_ge_one_sumset_nat
Proof state before:
A B : Set ℕ
n✝ : ℕ
hA : 0 ∈ A
hB : 0 ∈ B
hAB : 1 ≤ schnirelmannDensity A + schnirelmannDensity B
n : ℕ
hn : n ≠ 0
⊢ ↑(filter (fun x => x ∈ A) (Ioc 0 n)).card / ↑n + ↑(filter (fun x => x ∈ B) (Ioc 0 n)).card / ↑n =
    ↑(countelements A n + countelements B n) / ↑n
Tactic:
push_cast
Proof state after:
A B : Set ℕ
n✝ : ℕ
hA : 0 ∈ A
hB : 0 ∈ B
hAB : 1 ≤ schnirelmannDensity A + schnirelmannDensity B
n : ℕ
hn : n ≠ 0
⊢ ↑(filter (fun x => x ∈ A) (Ioc 0 n)).card / ↑n + ↑(filter (fun x => x ∈ B) (Ioc 0 n)).card / ↑n =
    (↑(countelements A n) + ↑(countelements B n)) / ↑n
Theorem: sum_schnirelmannDensity_ge_one_sumset_nat
Proof state before:
A B : Set ℕ
n✝ : ℕ
hA : 0 ∈ A
hB : 0 ∈ B
hAB : 1 ≤ schnirelmannDensity A + schnirelmannDensity B
n : ℕ
hn : n ≠ 0
⊢ ↑(filter (fun x => x ∈ A) (Ioc 0 n)).card / ↑n + ↑(filter (fun x => x ∈ B) (Ioc 0 n)).card / ↑n =
    (↑(countelements A n) + ↑(countelements B n)) / ↑n
Tactic:
rw [add_div]
Proof state after:
A B : Set ℕ
n✝ : ℕ
hA : 0 ∈ A
hB : 0 ∈ B
hAB : 1 ≤ schnirelmannDensity A + schnirelmannDensity B
n : ℕ
hn : n ≠ 0
⊢ ↑(filter (fun x => x ∈ A) (Ioc 0 n)).card / ↑n + ↑(filter (fun x => x ∈ B) (Ioc 0 n)).card / ↑n =
    ↑(countelements A n) / ↑n + ↑(countelements B n) / ↑n
Theorem: sum_schnirelmannDensity_ge_one_sumset_nat
Proof state before:
A B : Set ℕ
n✝ : ℕ
hA : 0 ∈ A
hB : 0 ∈ B
hAB : 1 ≤ schnirelmannDensity A + schnirelmannDensity B
n : ℕ
hn : n ≠ 0
⊢ ↑(filter (fun x => x ∈ A) (Ioc 0 n)).card / ↑n + ↑(filter (fun x => x ∈ B) (Ioc 0 n)).card / ↑n =
    ↑(countelements A n) / ↑n + ↑(countelements B n) / ↑n
Tactic:
rfl
Proof state after:
no goals
Theorem: le_schnirelmannDensity_add
Proof state before:
A✝ B✝ : Set ℕ
n : ℕ
A B : Set ℕ
hA : 0 ∈ A
hB : 0 ∈ B
⊢ schnirelmannDensity A + schnirelmannDensity B - schnirelmannDensity A * schnirelmannDensity B ≤
    schnirelmannDensity (A + B)
Tactic:
set α := schnirelmannDensity A with halpha
Proof state after:
A✝ B✝ : Set ℕ
n : ℕ
A B : Set ℕ
hA : 0 ∈ A
hB : 0 ∈ B
α : ℝ := schnirelmannDensity A
halpha : α = schnirelmannDensity A
⊢ α + schnirelmannDensity B - α * schnirelmannDensity B ≤ schnirelmannDensity (A + B)
Theorem: le_schnirelmannDensity_add
Proof state before:
A✝ B✝ : Set ℕ
n : ℕ
A B : Set ℕ
hA : 0 ∈ A
hB : 0 ∈ B
α : ℝ := schnirelmannDensity A
halpha : α = schnirelmannDensity A
⊢ α + schnirelmannDensity B - α * schnirelmannDensity B ≤ schnirelmannDensity (A + B)
Tactic:
set β := schnirelmannDensity B with hbeta
Proof state after:
A✝ B✝ : Set ℕ
n : ℕ
A B : Set ℕ
hA : 0 ∈ A
hB : 0 ∈ B
α : ℝ := schnirelmannDensity A
halpha : α = schnirelmannDensity A
β : ℝ := schnirelmannDensity B
hbeta : β = schnirelmannDensity B
⊢ α + β - α * β ≤ schnirelmannDensity (A + B)
Theorem: le_schnirelmannDensity_add
Proof state before:
A✝ B✝ : Set ℕ
n : ℕ
A B : Set ℕ
hA : 0 ∈ A
hB : 0 ∈ B
α : ℝ := schnirelmannDensity A
halpha : α = schnirelmannDensity A
β : ℝ := schnirelmannDensity B
hbeta : β = schnirelmannDensity B
⊢ α + β - α * β ≤ schnirelmannDensity (A + B)
Tactic:
have dum : α * (1 - β) + β = α + β - α * β := by ring
Proof state after:
A✝ B✝ : Set ℕ
n : ℕ
A B : Set ℕ
hA : 0 ∈ A
hB : 0 ∈ B
α : ℝ := schnirelmannDensity A
halpha : α = schnirelmannDensity A
β : ℝ := schnirelmannDensity B
hbeta : β = schnirelmannDensity B
dum : α * (1 - β) + β = α + β - α * β
⊢ α + β - α * β ≤ schnirelmannDensity (A + B)
Theorem: le_schnirelmannDensity_add
Proof state before:
A✝ B✝ : Set ℕ
n : ℕ
A B : Set ℕ
hA : 0 ∈ A
hB : 0 ∈ B
α : ℝ := schnirelmannDensity A
halpha : α = schnirelmannDensity A
β : ℝ := schnirelmannDensity B
hbeta : β = schnirelmannDensity B
dum : α * (1 - β) + β = α + β - α * β
⊢ α + β - α * β ≤ schnirelmannDensity (A + B)
Tactic:
rw [← dum]
Proof state after:
A✝ B✝ : Set ℕ
n : ℕ
A B : Set ℕ
hA : 0 ∈ A
hB : 0 ∈ B
α : ℝ := schnirelmannDensity A
halpha : α = schnirelmannDensity A
β : ℝ := schnirelmannDensity B
hbeta : β = schnirelmannDensity B
dum : α * (1 - β) + β = α + β - α * β
⊢ α * (1 - β) + β ≤ schnirelmannDensity (A + B)
Theorem: le_schnirelmannDensity_add
Proof state before:
A✝ B✝ : Set ℕ
n : ℕ
A B : Set ℕ
hA : 0 ∈ A
hB : 0 ∈ B
α : ℝ := schnirelmannDensity A
halpha : α = schnirelmannDensity A
β : ℝ := schnirelmannDensity B
hbeta : β = schnirelmannDensity B
dum : α * (1 - β) + β = α + β - α * β
⊢ ∀ (n : ℕ), (α * (1 - β) + β) * ↑n ≤ ↑(countelements (A + B) n)
Tactic:
rintro n
Proof state after:
A✝ B✝ : Set ℕ
n✝ : ℕ
A B : Set ℕ
hA : 0 ∈ A
hB : 0 ∈ B
α : ℝ := schnirelmannDensity A
halpha : α = schnirelmannDensity A
β : ℝ := schnirelmannDensity B
hbeta : β = schnirelmannDensity B
dum : α * (1 - β) + β = α + β - α * β
n : ℕ
⊢ (α * (1 - β) + β) * ↑n ≤ ↑(countelements (A + B) n)
Theorem: le_schnirelmannDensity_add
Proof state before:
A✝ B✝ : Set ℕ
n✝ : ℕ
A B : Set ℕ
hA : 0 ∈ A
hB : 0 ∈ B
α : ℝ := schnirelmannDensity A
halpha : α = schnirelmannDensity A
β : ℝ := schnirelmannDensity B
hbeta : β = schnirelmannDensity B
dum : α * (1 - β) + β = α + β - α * β
n : ℕ
⊢ (α * (1 - β) + β) * ↑n ≤ ↑(countelements (A + B) n)
Tactic:
obtain rfl | n1 := n.eq_zero_or_pos
Proof state after:
case inl
A✝ B✝ : Set ℕ
n : ℕ
A B : Set ℕ
hA : 0 ∈ A
hB : 0 ∈ B
α : ℝ := schnirelmannDensity A
halpha : α = schnirelmannDensity A
β : ℝ := schnirelmannDensity B
hbeta : β = schnirelmannDensity B
dum : α * (1 - β) + β = α + β - α * β
⊢ (α * (1 - β) + β) * ↑0 ≤ ↑(countelements (A + B) 0)

case inr
A✝ B✝ : Set ℕ
n✝ : ℕ
A B : Set ℕ
hA : 0 ∈ A
hB : 0 ∈ B
α : ℝ := schnirelmannDensity A
halpha : α = schnirelmannDensity A
β : ℝ := schnirelmannDensity B
hbeta : β = schnirelmannDensity B
dum : α * (1 - β) + β = α + β - α * β
n : ℕ
n1 : n > 0
⊢ (α * (1 - β) + β) * ↑n ≤ ↑(countelements (A + B) n)
Theorem: le_schnirelmannDensity_add
Proof state before:
A✝ B✝ : Set ℕ
n : ℕ
A B : Set ℕ
hA : 0 ∈ A
hB : 0 ∈ B
α : ℝ := schnirelmannDensity A
halpha : α = schnirelmannDensity A
β : ℝ := schnirelmannDensity B
hbeta : β = schnirelmannDensity B
⊢ α * (1 - β) + β = α + β - α * β
Tactic:
ring
Proof state after:
no goals
Theorem: le_schnirelmannDensity_add
Proof state before:
A✝ B✝ : Set ℕ
n : ℕ
A B : Set ℕ
hA : 0 ∈ A
hB : 0 ∈ B
α : ℝ := schnirelmannDensity A
halpha : α = schnirelmannDensity A
β : ℝ := schnirelmannDensity B
hbeta : β = schnirelmannDensity B
dum : α * (1 - β) + β = α + β - α * β
main : ∀ (n : ℕ), (α * (1 - β) + β) * ↑n ≤ ↑(countelements (A + B) n)
⊢ α * (1 - β) + β ≤ schnirelmannDensity (A + B)
Tactic:
rw [schnirelmannDensity]
Proof state after:
A✝ B✝ : Set ℕ
n : ℕ
A B : Set ℕ
hA : 0 ∈ A
hB : 0 ∈ B
α : ℝ := schnirelmannDensity A
halpha : α = schnirelmannDensity A
β : ℝ := schnirelmannDensity B
hbeta : β = schnirelmannDensity B
dum : α * (1 - β) + β = α + β - α * β
main : ∀ (n : ℕ), (α * (1 - β) + β) * ↑n ≤ ↑(countelements (A + B) n)
⊢ α * (1 - β) + β ≤ ⨅ n, ↑(filter (fun x => x ∈ A + B) (Ioc 0 ↑n)).card / ↑↑n
Theorem: le_schnirelmannDensity_add
Proof state before:
A✝ B✝ : Set ℕ
n : ℕ
A B : Set ℕ
hA : 0 ∈ A
hB : 0 ∈ B
α : ℝ := schnirelmannDensity A
halpha : α = schnirelmannDensity A
β : ℝ := schnirelmannDensity B
hbeta : β = schnirelmannDensity B
dum : α * (1 - β) + β = α + β - α * β
main : ∀ (n : ℕ), (α * (1 - β) + β) * ↑n ≤ ↑(countelements (A + B) n)
⊢ α * (1 - β) + β ≤ ⨅ n, ↑(filter (fun x => x ∈ A + B) (Ioc 0 ↑n)).card / ↑↑n
Tactic:
have : Nonempty {n // n ≠ 0} := by
  use 1
  trivial
Proof state after:
A✝ B✝ : Set ℕ
n : ℕ
A B : Set ℕ
hA : 0 ∈ A
hB : 0 ∈ B
α : ℝ := schnirelmannDensity A
halpha : α = schnirelmannDensity A
β : ℝ := schnirelmannDensity B
hbeta : β = schnirelmannDensity B
dum : α * (1 - β) + β = α + β - α * β
main : ∀ (n : ℕ), (α * (1 - β) + β) * ↑n ≤ ↑(countelements (A + B) n)
this : Nonempty { n // n ≠ 0 }
⊢ α * (1 - β) + β ≤ ⨅ n, ↑(filter (fun x => x ∈ A + B) (Ioc 0 ↑n)).card / ↑↑n
Theorem: le_schnirelmannDensity_add
Proof state before:
A✝ B✝ : Set ℕ
n : ℕ
A B : Set ℕ
hA : 0 ∈ A
hB : 0 ∈ B
α : ℝ := schnirelmannDensity A
halpha : α = schnirelmannDensity A
β : ℝ := schnirelmannDensity B
hbeta : β = schnirelmannDensity B
dum : α * (1 - β) + β = α + β - α * β
main : ∀ (n : ℕ), (α * (1 - β) + β) * ↑n ≤ ↑(countelements (A + B) n)
this : Nonempty { n // n ≠ 0 }
⊢ α * (1 - β) + β ≤ ⨅ n, ↑(filter (fun x => x ∈ A + B) (Ioc 0 ↑n)).card / ↑↑n
Tactic:
apply le_ciInf
Proof state after:
case H
A✝ B✝ : Set ℕ
n : ℕ
A B : Set ℕ
hA : 0 ∈ A
hB : 0 ∈ B
α : ℝ := schnirelmannDensity A
halpha : α = schnirelmannDensity A
β : ℝ := schnirelmannDensity B
hbeta : β = schnirelmannDensity B
dum : α * (1 - β) + β = α + β - α * β
main : ∀ (n : ℕ), (α * (1 - β) + β) * ↑n ≤ ↑(countelements (A + B) n)
this : Nonempty { n // n ≠ 0 }
⊢ ∀ (x : { n // 0 < n }), α * (1 - β) + β ≤ ↑(filter (fun x => x ∈ A + B) (Ioc 0 ↑x)).card / ↑↑x
Theorem: le_schnirelmannDensity_add
Proof state before:
case H
A✝ B✝ : Set ℕ
n : ℕ
A B : Set ℕ
hA : 0 ∈ A
hB : 0 ∈ B
α : ℝ := schnirelmannDensity A
halpha : α = schnirelmannDensity A
β : ℝ := schnirelmannDensity B
hbeta : β = schnirelmannDensity B
dum : α * (1 - β) + β = α + β - α * β
main : ∀ (n : ℕ), (α * (1 - β) + β) * ↑n ≤ ↑(countelements (A + B) n)
this : Nonempty { n // n ≠ 0 }
⊢ ∀ (x : { n // 0 < n }), α * (1 - β) + β ≤ ↑(filter (fun x => x ∈ A + B) (Ioc 0 ↑x)).card / ↑↑x
Tactic:
intro x
Proof state after:
case H
A✝ B✝ : Set ℕ
n : ℕ
A B : Set ℕ
hA : 0 ∈ A
hB : 0 ∈ B
α : ℝ := schnirelmannDensity A
halpha : α = schnirelmannDensity A
β : ℝ := schnirelmannDensity B
hbeta : β = schnirelmannDensity B
dum : α * (1 - β) + β = α + β - α * β
main : ∀ (n : ℕ), (α * (1 - β) + β) * ↑n ≤ ↑(countelements (A + B) n)
this : Nonempty { n // n ≠ 0 }
x : { n // 0 < n }
⊢ α * (1 - β) + β ≤ ↑(filter (fun x => x ∈ A + B) (Ioc 0 ↑x)).card / ↑↑x
Theorem: le_schnirelmannDensity_add
Proof state before:
case H
A✝ B✝ : Set ℕ
n : ℕ
A B : Set ℕ
hA : 0 ∈ A
hB : 0 ∈ B
α : ℝ := schnirelmannDensity A
halpha : α = schnirelmannDensity A
β : ℝ := schnirelmannDensity B
hbeta : β = schnirelmannDensity B
dum : α * (1 - β) + β = α + β - α * β
main : ∀ (n : ℕ), (α * (1 - β) + β) * ↑n ≤ ↑(countelements (A + B) n)
this : Nonempty { n // n ≠ 0 }
x : { n // 0 < n }
⊢ α * (1 - β) + β ≤ ↑(filter (fun x => x ∈ A + B) (Ioc 0 ↑x)).card / ↑↑x
Tactic:
have hx : (x : ℝ) ≠ 0 := by aesop
Proof state after:
case H
A✝ B✝ : Set ℕ
n : ℕ
A B : Set ℕ
hA : 0 ∈ A
hB : 0 ∈ B
α : ℝ := schnirelmannDensity A
halpha : α = schnirelmannDensity A
β : ℝ := schnirelmannDensity B
hbeta : β = schnirelmannDensity B
dum : α * (1 - β) + β = α + β - α * β
main : ∀ (n : ℕ), (α * (1 - β) + β) * ↑n ≤ ↑(countelements (A + B) n)
this : Nonempty { n // n ≠ 0 }
x : { n // 0 < n }
hx : ↑↑x ≠ 0
⊢ α * (1 - β) + β ≤ ↑(filter (fun x => x ∈ A + B) (Ioc 0 ↑x)).card / ↑↑x
Theorem: le_schnirelmannDensity_add
Proof state before:
case H
A✝ B✝ : Set ℕ
n : ℕ
A B : Set ℕ
hA : 0 ∈ A
hB : 0 ∈ B
α : ℝ := schnirelmannDensity A
halpha : α = schnirelmannDensity A
β : ℝ := schnirelmannDensity B
hbeta : β = schnirelmannDensity B
dum : α * (1 - β) + β = α + β - α * β
main : ∀ (n : ℕ), (α * (1 - β) + β) * ↑n ≤ ↑(countelements (A + B) n)
this : Nonempty { n // n ≠ 0 }
x : { n // 0 < n }
hx : ↑↑x ≠ 0
⊢ α * (1 - β) + β ≤ ↑(filter (fun x => x ∈ A + B) (Ioc 0 ↑x)).card / ↑↑x
Tactic:
rw [le_div_iff]
Proof state after:
case H
A✝ B✝ : Set ℕ
n : ℕ
A B : Set ℕ
hA : 0 ∈ A
hB : 0 ∈ B
α : ℝ := schnirelmannDensity A
halpha : α = schnirelmannDensity A
β : ℝ := schnirelmannDensity B
hbeta : β = schnirelmannDensity B
dum : α * (1 - β) + β = α + β - α * β
main : ∀ (n : ℕ), (α * (1 - β) + β) * ↑n ≤ ↑(countelements (A + B) n)
this : Nonempty { n // n ≠ 0 }
x : { n // 0 < n }
hx : ↑↑x ≠ 0
⊢ (α * (1 - β) + β) * ↑↑x ≤ ↑(filter (fun x => x ∈ A + B) (Ioc 0 ↑x)).card

case H
A✝ B✝ : Set ℕ
n : ℕ
A B : Set ℕ
hA : 0 ∈ A
hB : 0 ∈ B
α : ℝ := schnirelmannDensity A
halpha : α = schnirelmannDensity A
β : ℝ := schnirelmannDensity B
hbeta : β = schnirelmannDensity B
dum : α * (1 - β) + β = α + β - α * β
main : ∀ (n : ℕ), (α * (1 - β) + β) * ↑n ≤ ↑(countelements (A + B) n)
this : Nonempty { n // n ≠ 0 }
x : { n // 0 < n }
hx : ↑↑x ≠ 0
⊢ 0 < ↑↑x
Theorem: le_schnirelmannDensity_add
Proof state before:
A✝ B✝ : Set ℕ
n : ℕ
A B : Set ℕ
hA : 0 ∈ A
hB : 0 ∈ B
α : ℝ := schnirelmannDensity A
halpha : α = schnirelmannDensity A
β : ℝ := schnirelmannDensity B
hbeta : β = schnirelmannDensity B
dum : α * (1 - β) + β = α + β - α * β
main : ∀ (n : ℕ), (α * (1 - β) + β) * ↑n ≤ ↑(countelements (A + B) n)
⊢ Nonempty { n // n ≠ 0 }
Tactic:
use 1
Proof state after:
case property
A✝ B✝ : Set ℕ
n : ℕ
A B : Set ℕ
hA : 0 ∈ A
hB : 0 ∈ B
α : ℝ := schnirelmannDensity A
halpha : α = schnirelmannDensity A
β : ℝ := schnirelmannDensity B
hbeta : β = schnirelmannDensity B
dum : α * (1 - β) + β = α + β - α * β
main : ∀ (n : ℕ), (α * (1 - β) + β) * ↑n ≤ ↑(countelements (A + B) n)
⊢ 1 ≠ 0
Theorem: le_schnirelmannDensity_add
Proof state before:
case property
A✝ B✝ : Set ℕ
n : ℕ
A B : Set ℕ
hA : 0 ∈ A
hB : 0 ∈ B
α : ℝ := schnirelmannDensity A
halpha : α = schnirelmannDensity A
β : ℝ := schnirelmannDensity B
hbeta : β = schnirelmannDensity B
dum : α * (1 - β) + β = α + β - α * β
main : ∀ (n : ℕ), (α * (1 - β) + β) * ↑n ≤ ↑(countelements (A + B) n)
⊢ 1 ≠ 0
Tactic:
trivial
Proof state after:
no goals
Theorem: le_schnirelmannDensity_add
Proof state before:
A✝ B✝ : Set ℕ
n : ℕ
A B : Set ℕ
hA : 0 ∈ A
hB : 0 ∈ B
α : ℝ := schnirelmannDensity A
halpha : α = schnirelmannDensity A
β : ℝ := schnirelmannDensity B
hbeta : β = schnirelmannDensity B
dum : α * (1 - β) + β = α + β - α * β
main : ∀ (n : ℕ), (α * (1 - β) + β) * ↑n ≤ ↑(countelements (A + B) n)
this : Nonempty { n // n ≠ 0 }
x : { n // 0 < n }
⊢ ↑↑x ≠ 0
Tactic:
aesop
Proof state after:
no goals
Theorem: le_schnirelmannDensity_add
Proof state before:
case H
A✝ B✝ : Set ℕ
n : ℕ
A B : Set ℕ
hA : 0 ∈ A
hB : 0 ∈ B
α : ℝ := schnirelmannDensity A
halpha : α = schnirelmannDensity A
β : ℝ := schnirelmannDensity B
hbeta : β = schnirelmannDensity B
dum : α * (1 - β) + β = α + β - α * β
main : ∀ (n : ℕ), (α * (1 - β) + β) * ↑n ≤ ↑(countelements (A + B) n)
this : Nonempty { n // n ≠ 0 }
x : { n // 0 < n }
hx : ↑↑x ≠ 0
⊢ (α * (1 - β) + β) * ↑↑x ≤ ↑(filter (fun x => x ∈ A + B) (Ioc 0 ↑x)).card
Tactic:
specialize main x
Proof state after:
case H
A✝ B✝ : Set ℕ
n : ℕ
A B : Set ℕ
hA : 0 ∈ A
hB : 0 ∈ B
α : ℝ := schnirelmannDensity A
halpha : α = schnirelmannDensity A
β : ℝ := schnirelmannDensity B
hbeta : β = schnirelmannDensity B
dum : α * (1 - β) + β = α + β - α * β
this : Nonempty { n // n ≠ 0 }
x : { n // 0 < n }
hx : ↑↑x ≠ 0
main : (α * (1 - β) + β) * ↑↑x ≤ ↑(countelements (A + B) ↑x)
⊢ (α * (1 - β) + β) * ↑↑x ≤ ↑(filter (fun x => x ∈ A + B) (Ioc 0 ↑x)).card
Theorem: le_schnirelmannDensity_add
Proof state before:
case H
A✝ B✝ : Set ℕ
n : ℕ
A B : Set ℕ
hA : 0 ∈ A
hB : 0 ∈ B
α : ℝ := schnirelmannDensity A
halpha : α = schnirelmannDensity A
β : ℝ := schnirelmannDensity B
hbeta : β = schnirelmannDensity B
dum : α * (1 - β) + β = α + β - α * β
this : Nonempty { n // n ≠ 0 }
x : { n // 0 < n }
hx : ↑↑x ≠ 0
main : (α * (1 - β) + β) * ↑↑x ≤ ↑(countelements (A + B) ↑x)
⊢ (α * (1 - β) + β) * ↑↑x ≤ ↑(filter (fun x => x ∈ A + B) (Ioc 0 ↑x)).card
Tactic:
exact main
Proof state after:
no goals
Theorem: le_schnirelmannDensity_add
Proof state before:
case H
A✝ B✝ : Set ℕ
n : ℕ
A B : Set ℕ
hA : 0 ∈ A
hB : 0 ∈ B
α : ℝ := schnirelmannDensity A
halpha : α = schnirelmannDensity A
β : ℝ := schnirelmannDensity B
hbeta : β = schnirelmannDensity B
dum : α * (1 - β) + β = α + β - α * β
main : ∀ (n : ℕ), (α * (1 - β) + β) * ↑n ≤ ↑(countelements (A + B) n)
this : Nonempty { n // n ≠ 0 }
x : { n // 0 < n }
hx : ↑↑x ≠ 0
⊢ 0 < ↑↑x
Tactic:
positivity
Proof state after:
no goals