internlm/Lean-Github huggingface dataset:
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 : ℕ
n1 : n > 0
lem : ⋃ a, {c | c ∈ A + B ∧ 0 < c - ↑a ∧ c ≤ next_elm A a n} ⊆ (A + B) ∩ ↑(Icc 1 n)
aux : countelements (⋃ a, {c | c ∈ A + B ∧ 0 < c - ↑a ∧ c ≤ next_elm A a n}) n ≤ countelements (A + B) n
a : ↑A
⊢ 1 + countelements B (next_elm A a n - ↑a - 1) ≤ countelements {c | c ∈ A + B ∧ 0 < c - ↑a ∧ c ≤ next_elm A a n} n
Tactic:
sorry
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 - β) + β = α + β - α * β
n : ℕ
n1 : n > 0
lem : ⋃ a, {c | c ∈ A + B ∧ 0 < c - ↑a ∧ c ≤ next_elm A a n} ⊆ (A + B) ∩ ↑(Icc 1 n)
aux : countelements (⋃ a, {c | c ∈ A + B ∧ 0 < c - ↑a ∧ c ≤ next_elm A a n}) n ≤ countelements (A + B) n
hcc :
  ∀ (a : ↑A),
    1 + countelements B (next_elm A a n - ↑a - 1) ≤ countelements {c | c ∈ A + B ∧ 0 < c - ↑a ∧ c ≤ next_elm A a n} n
a x : ↑A
hh : a ≠ x
⊢ {c | c ∈ A + B ∧ 0 < c - ↑a ∧ c ≤ next_elm A a n} ∩ {c | c ∈ A + B ∧ 0 < c - ↑x ∧ c ≤ next_elm A x n} = ∅
Tactic:
sorry
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 - β) + β = α + β - α * β
n : ℕ
n1 : n > 0
lem : ⋃ a, {c | c ∈ A + B ∧ 0 < c - ↑a ∧ c ≤ next_elm A a n} ⊆ (A + B) ∩ ↑(Icc 1 n)
aux : countelements (⋃ a, {c | c ∈ A + B ∧ 0 < c - ↑a ∧ c ≤ next_elm A a n}) n ≤ countelements (A + B) n
claim :
  ↑(countelements A n) + β * (↑n - ↑(countelements A n)) ≤
    ↑(countelements (⋃ a, {c | c ∈ A + B ∧ 0 < c - ↑a ∧ c ≤ next_elm A a n}) n)
⊢ ↑(countelements A n) + β * (↑n - ↑(countelements A n)) ≤ ↑(countelements (A + B) n)
Tactic:
apply le_trans claim _
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 : ℕ
n1 : n > 0
lem : ⋃ a, {c | c ∈ A + B ∧ 0 < c - ↑a ∧ c ≤ next_elm A a n} ⊆ (A + B) ∩ ↑(Icc 1 n)
aux : countelements (⋃ a, {c | c ∈ A + B ∧ 0 < c - ↑a ∧ c ≤ next_elm A a n}) n ≤ countelements (A + B) n
claim :
  ↑(countelements A n) + β * (↑n - ↑(countelements A n)) ≤
    ↑(countelements (⋃ a, {c | c ∈ A + B ∧ 0 < c - ↑a ∧ c ≤ next_elm A a n}) n)
⊢ ↑(countelements (⋃ a, {c | c ∈ A + B ∧ 0 < c - ↑a ∧ c ≤ next_elm A a n}) 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 : ℕ
n1 : n > 0
lem : ⋃ a, {c | c ∈ A + B ∧ 0 < c - ↑a ∧ c ≤ next_elm A a n} ⊆ (A + B) ∩ ↑(Icc 1 n)
aux : countelements (⋃ a, {c | c ∈ A + B ∧ 0 < c - ↑a ∧ c ≤ next_elm A a n}) n ≤ countelements (A + B) n
claim :
  ↑(countelements A n) + β * (↑n - ↑(countelements A n)) ≤
    ↑(countelements (⋃ a, {c | c ∈ A + B ∧ 0 < c - ↑a ∧ c ≤ next_elm A a n}) n)
⊢ ↑(countelements (⋃ a, {c | c ∈ A + B ∧ 0 < c - ↑a ∧ c ≤ next_elm A a n}) n) ≤ ↑(countelements (A + B) n)
Tactic:
norm_cast
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 - β) + β = α + β - α * β
n : ℕ
n1 : n > 0
lem : ⋃ a, {c | c ∈ A + B ∧ 0 < c - ↑a ∧ c ≤ next_elm A a n} ⊆ (A + B) ∩ ↑(Icc 1 n)
aux : countelements (⋃ a, {c | c ∈ A + B ∧ 0 < c - ↑a ∧ c ≤ next_elm A a n}) n ≤ countelements (A + B) n
claim :
  ↑(countelements A n) + β * (↑n - ↑(countelements A n)) ≤
    ↑(countelements (⋃ a, {c | c ∈ A + B ∧ 0 < c - ↑a ∧ c ≤ next_elm A a n}) n)
ht : ↑(countelements A n) + β * (↑n - ↑(countelements A n)) ≤ ↑(countelements (A + B) n)
⊢ ↑(countelements A n) * (1 - β) + β * ↑n = ↑(countelements A n) + β * (↑n - ↑(countelements A n))
Tactic:
ring_nf
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 - β) + β = α + β - α * β
n : ℕ
n1 : n > 0
lem : ⋃ a, {c | c ∈ A + B ∧ 0 < c - ↑a ∧ c ≤ next_elm A a n} ⊆ (A + B) ∩ ↑(Icc 1 n)
aux : countelements (⋃ a, {c | c ∈ A + B ∧ 0 < c - ↑a ∧ c ≤ next_elm A a n}) n ≤ countelements (A + B) n
claim :
  ↑(countelements A n) + β * (↑n - ↑(countelements A n)) ≤
    ↑(countelements (⋃ a, {c | c ∈ A + B ∧ 0 < c - ↑a ∧ c ≤ next_elm A a n}) n)
ht : ↑(countelements A n) + β * (↑n - ↑(countelements A n)) ≤ ↑(countelements (A + B) n)
hc1 : ↑(countelements A n) * (1 - β) + β * ↑n = ↑(countelements A n) + β * (↑n - ↑(countelements A n))
⊢ α * ↑n * (1 - β) + β * ↑n ≤ ↑(countelements A n) * (1 - β) + β * ↑n
Tactic:
rw [halpha]
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 : ℕ
n1 : n > 0
lem : ⋃ a, {c | c ∈ A + B ∧ 0 < c - ↑a ∧ c ≤ next_elm A a n} ⊆ (A + B) ∩ ↑(Icc 1 n)
aux : countelements (⋃ a, {c | c ∈ A + B ∧ 0 < c - ↑a ∧ c ≤ next_elm A a n}) n ≤ countelements (A + B) n
claim :
  ↑(countelements A n) + β * (↑n - ↑(countelements A n)) ≤
    ↑(countelements (⋃ a, {c | c ∈ A + B ∧ 0 < c - ↑a ∧ c ≤ next_elm A a n}) n)
ht : ↑(countelements A n) + β * (↑n - ↑(countelements A n)) ≤ ↑(countelements (A + B) n)
hc1 : ↑(countelements A n) * (1 - β) + β * ↑n = ↑(countelements A n) + β * (↑n - ↑(countelements A n))
⊢ schnirelmannDensity A * ↑n * (1 - β) + β * ↑n ≤ ↑(countelements A n) * (1 - β) + β * ↑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 : ℕ
n1 : n > 0
lem : ⋃ a, {c | c ∈ A + B ∧ 0 < c - ↑a ∧ c ≤ next_elm A a n} ⊆ (A + B) ∩ ↑(Icc 1 n)
aux : countelements (⋃ a, {c | c ∈ A + B ∧ 0 < c - ↑a ∧ c ≤ next_elm A a n}) n ≤ countelements (A + B) n
claim :
  ↑(countelements A n) + β * (↑n - ↑(countelements A n)) ≤
    ↑(countelements (⋃ a, {c | c ∈ A + B ∧ 0 < c - ↑a ∧ c ≤ next_elm A a n}) n)
ht : ↑(countelements A n) + β * (↑n - ↑(countelements A n)) ≤ ↑(countelements (A + B) n)
hc1 : ↑(countelements A n) * (1 - β) + β * ↑n = ↑(countelements A n) + β * (↑n - ↑(countelements A n))
⊢ schnirelmannDensity A * ↑n * (1 - β) + β * ↑n ≤ ↑(countelements A n) * (1 - β) + β * ↑n
Tactic:
by_cases hbo : β = 1
Proof state after:
case pos
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
lem : ⋃ a, {c | c ∈ A + B ∧ 0 < c - ↑a ∧ c ≤ next_elm A a n} ⊆ (A + B) ∩ ↑(Icc 1 n)
aux : countelements (⋃ a, {c | c ∈ A + B ∧ 0 < c - ↑a ∧ c ≤ next_elm A a n}) n ≤ countelements (A + B) n
claim :
  ↑(countelements A n) + β * (↑n - ↑(countelements A n)) ≤
    ↑(countelements (⋃ a, {c | c ∈ A + B ∧ 0 < c - ↑a ∧ c ≤ next_elm A a n}) n)
ht : ↑(countelements A n) + β * (↑n - ↑(countelements A n)) ≤ ↑(countelements (A + B) n)
hc1 : ↑(countelements A n) * (1 - β) + β * ↑n = ↑(countelements A n) + β * (↑n - ↑(countelements A n))
hbo : β = 1
⊢ schnirelmannDensity A * ↑n * (1 - β) + β * ↑n ≤ ↑(countelements A n) * (1 - β) + β * ↑n

case neg
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
lem : ⋃ a, {c | c ∈ A + B ∧ 0 < c - ↑a ∧ c ≤ next_elm A a n} ⊆ (A + B) ∩ ↑(Icc 1 n)
aux : countelements (⋃ a, {c | c ∈ A + B ∧ 0 < c - ↑a ∧ c ≤ next_elm A a n}) n ≤ countelements (A + B) n
claim :
  ↑(countelements A n) + β * (↑n - ↑(countelements A n)) ≤
    ↑(countelements (⋃ a, {c | c ∈ A + B ∧ 0 < c - ↑a ∧ c ≤ next_elm A a n}) n)
ht : ↑(countelements A n) + β * (↑n - ↑(countelements A n)) ≤ ↑(countelements (A + B) n)
hc1 : ↑(countelements A n) * (1 - β) + β * ↑n = ↑(countelements A n) + β * (↑n - ↑(countelements A n))
hbo : ¬β = 1
⊢ schnirelmannDensity A * ↑n * (1 - β) + β * ↑n ≤ ↑(countelements A n) * (1 - β) + β * ↑n
Theorem: le_schnirelmannDensity_add
Proof state before:
case pos
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
lem : ⋃ a, {c | c ∈ A + B ∧ 0 < c - ↑a ∧ c ≤ next_elm A a n} ⊆ (A + B) ∩ ↑(Icc 1 n)
aux : countelements (⋃ a, {c | c ∈ A + B ∧ 0 < c - ↑a ∧ c ≤ next_elm A a n}) n ≤ countelements (A + B) n
claim :
  ↑(countelements A n) + β * (↑n - ↑(countelements A n)) ≤
    ↑(countelements (⋃ a, {c | c ∈ A + B ∧ 0 < c - ↑a ∧ c ≤ next_elm A a n}) n)
ht : ↑(countelements A n) + β * (↑n - ↑(countelements A n)) ≤ ↑(countelements (A + B) n)
hc1 : ↑(countelements A n) * (1 - β) + β * ↑n = ↑(countelements A n) + β * (↑n - ↑(countelements A n))
hbo : β = 1
⊢ schnirelmannDensity A * ↑n * (1 - β) + β * ↑n ≤ ↑(countelements A n) * (1 - β) + β * ↑n
Tactic:
rw [hbo]
Proof state after:
case pos
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
lem : ⋃ a, {c | c ∈ A + B ∧ 0 < c - ↑a ∧ c ≤ next_elm A a n} ⊆ (A + B) ∩ ↑(Icc 1 n)
aux : countelements (⋃ a, {c | c ∈ A + B ∧ 0 < c - ↑a ∧ c ≤ next_elm A a n}) n ≤ countelements (A + B) n
claim :
  ↑(countelements A n) + β * (↑n - ↑(countelements A n)) ≤
    ↑(countelements (⋃ a, {c | c ∈ A + B ∧ 0 < c - ↑a ∧ c ≤ next_elm A a n}) n)
ht : ↑(countelements A n) + β * (↑n - ↑(countelements A n)) ≤ ↑(countelements (A + B) n)
hc1 : ↑(countelements A n) * (1 - β) + β * ↑n = ↑(countelements A n) + β * (↑n - ↑(countelements A n))
hbo : β = 1
⊢ schnirelmannDensity A * ↑n * (1 - 1) + 1 * ↑n ≤ ↑(countelements A n) * (1 - 1) + 1 * ↑n
Theorem: le_schnirelmannDensity_add
Proof state before:
case pos
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
lem : ⋃ a, {c | c ∈ A + B ∧ 0 < c - ↑a ∧ c ≤ next_elm A a n} ⊆ (A + B) ∩ ↑(Icc 1 n)
aux : countelements (⋃ a, {c | c ∈ A + B ∧ 0 < c - ↑a ∧ c ≤ next_elm A a n}) n ≤ countelements (A + B) n
claim :
  ↑(countelements A n) + β * (↑n - ↑(countelements A n)) ≤
    ↑(countelements (⋃ a, {c | c ∈ A + B ∧ 0 < c - ↑a ∧ c ≤ next_elm A a n}) n)
ht : ↑(countelements A n) + β * (↑n - ↑(countelements A n)) ≤ ↑(countelements (A + B) n)
hc1 : ↑(countelements A n) * (1 - β) + β * ↑n = ↑(countelements A n) + β * (↑n - ↑(countelements A n))
hbo : β = 1
⊢ schnirelmannDensity A * ↑n * (1 - 1) + 1 * ↑n ≤ ↑(countelements A n) * (1 - 1) + 1 * ↑n
Tactic:
simp only [sub_self, mul_zero, one_mul, zero_add, le_refl]
Proof state after:
no goals
Theorem: le_schnirelmannDensity_add
Proof state before:
case neg
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
lem : ⋃ a, {c | c ∈ A + B ∧ 0 < c - ↑a ∧ c ≤ next_elm A a n} ⊆ (A + B) ∩ ↑(Icc 1 n)
aux : countelements (⋃ a, {c | c ∈ A + B ∧ 0 < c - ↑a ∧ c ≤ next_elm A a n}) n ≤ countelements (A + B) n
claim :
  ↑(countelements A n) + β * (↑n - ↑(countelements A n)) ≤
    ↑(countelements (⋃ a, {c | c ∈ A + B ∧ 0 < c - ↑a ∧ c ≤ next_elm A a n}) n)
ht : ↑(countelements A n) + β * (↑n - ↑(countelements A n)) ≤ ↑(countelements (A + B) n)
hc1 : ↑(countelements A n) * (1 - β) + β * ↑n = ↑(countelements A n) + β * (↑n - ↑(countelements A n))
hbo : ¬β = 1
⊢ schnirelmannDensity A * ↑n * (1 - β) + β * ↑n ≤ ↑(countelements A n) * (1 - β) + β * ↑n
Tactic:
have hbn : 0 < (1 - schnirelmannDensity B) := by
  rw [hbeta] at hbo
  rw [lt_sub_iff_add_lt, zero_add, lt_iff_le_and_ne]
  exact ⟨schnirelmannDensity_le_one, hbo⟩
Proof state after:
case neg
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
lem : ⋃ a, {c | c ∈ A + B ∧ 0 < c - ↑a ∧ c ≤ next_elm A a n} ⊆ (A + B) ∩ ↑(Icc 1 n)
aux : countelements (⋃ a, {c | c ∈ A + B ∧ 0 < c - ↑a ∧ c ≤ next_elm A a n}) n ≤ countelements (A + B) n
claim :
  ↑(countelements A n) + β * (↑n - ↑(countelements A n)) ≤
    ↑(countelements (⋃ a, {c | c ∈ A + B ∧ 0 < c - ↑a ∧ c ≤ next_elm A a n}) n)
ht : ↑(countelements A n) + β * (↑n - ↑(countelements A n)) ≤ ↑(countelements (A + B) n)
hc1 : ↑(countelements A n) * (1 - β) + β * ↑n = ↑(countelements A n) + β * (↑n - ↑(countelements A n))
hbo : ¬β = 1
hbn : 0 < 1 - schnirelmannDensity B
⊢ schnirelmannDensity A * ↑n * (1 - β) + β * ↑n ≤ ↑(countelements A n) * (1 - β) + β * ↑n
Theorem: le_schnirelmannDensity_add
Proof state before:
case neg
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
lem : ⋃ a, {c | c ∈ A + B ∧ 0 < c - ↑a ∧ c ≤ next_elm A a n} ⊆ (A + B) ∩ ↑(Icc 1 n)
aux : countelements (⋃ a, {c | c ∈ A + B ∧ 0 < c - ↑a ∧ c ≤ next_elm A a n}) n ≤ countelements (A + B) n
claim :
  ↑(countelements A n) + β * (↑n - ↑(countelements A n)) ≤
    ↑(countelements (⋃ a, {c | c ∈ A + B ∧ 0 < c - ↑a ∧ c ≤ next_elm A a n}) n)
ht : ↑(countelements A n) + β * (↑n - ↑(countelements A n)) ≤ ↑(countelements (A + B) n)
hc1 : ↑(countelements A n) * (1 - β) + β * ↑n = ↑(countelements A n) + β * (↑n - ↑(countelements A n))
hbo : ¬β = 1
hbn : 0 < 1 - schnirelmannDensity B
⊢ schnirelmannDensity A * ↑n * (1 - β) + β * ↑n ≤ ↑(countelements A n) * (1 - β) + β * ↑n
Tactic:
simp only [add_le_add_iff_right, sub_pos, sub_neg]
Proof state after:
case neg
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
lem : ⋃ a, {c | c ∈ A + B ∧ 0 < c - ↑a ∧ c ≤ next_elm A a n} ⊆ (A + B) ∩ ↑(Icc 1 n)
aux : countelements (⋃ a, {c | c ∈ A + B ∧ 0 < c - ↑a ∧ c ≤ next_elm A a n}) n ≤ countelements (A + B) n
claim :
  ↑(countelements A n) + β * (↑n - ↑(countelements A n)) ≤
    ↑(countelements (⋃ a, {c | c ∈ A + B ∧ 0 < c - ↑a ∧ c ≤ next_elm A a n}) n)
ht : ↑(countelements A n) + β * (↑n - ↑(countelements A n)) ≤ ↑(countelements (A + B) n)
hc1 : ↑(countelements A n) * (1 - β) + β * ↑n = ↑(countelements A n) + β * (↑n - ↑(countelements A n))
hbo : ¬β = 1
hbn : 0 < 1 - schnirelmannDensity B
⊢ schnirelmannDensity A * ↑n * (1 - β) ≤ ↑(countelements A n) * (1 - β)
Theorem: le_schnirelmannDensity_add
Proof state before:
case neg
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
lem : ⋃ a, {c | c ∈ A + B ∧ 0 < c - ↑a ∧ c ≤ next_elm A a n} ⊆ (A + B) ∩ ↑(Icc 1 n)
aux : countelements (⋃ a, {c | c ∈ A + B ∧ 0 < c - ↑a ∧ c ≤ next_elm A a n}) n ≤ countelements (A + B) n
claim :
  ↑(countelements A n) + β * (↑n - ↑(countelements A n)) ≤
    ↑(countelements (⋃ a, {c | c ∈ A + B ∧ 0 < c - ↑a ∧ c ≤ next_elm A a n}) n)
ht : ↑(countelements A n) + β * (↑n - ↑(countelements A n)) ≤ ↑(countelements (A + B) n)
hc1 : ↑(countelements A n) * (1 - β) + β * ↑n = ↑(countelements A n) + β * (↑n - ↑(countelements A n))
hbo : ¬β = 1
hbn : 0 < 1 - schnirelmannDensity B
⊢ schnirelmannDensity A * ↑n * (1 - β) ≤ ↑(countelements A n) * (1 - β)
Tactic:
rw [← le_div_iff (hbn)]
Proof state after:
case neg
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
lem : ⋃ a, {c | c ∈ A + B ∧ 0 < c - ↑a ∧ c ≤ next_elm A a n} ⊆ (A + B) ∩ ↑(Icc 1 n)
aux : countelements (⋃ a, {c | c ∈ A + B ∧ 0 < c - ↑a ∧ c ≤ next_elm A a n}) n ≤ countelements (A + B) n
claim :
  ↑(countelements A n) + β * (↑n - ↑(countelements A n)) ≤
    ↑(countelements (⋃ a, {c | c ∈ A + B ∧ 0 < c - ↑a ∧ c ≤ next_elm A a n}) n)
ht : ↑(countelements A n) + β * (↑n - ↑(countelements A n)) ≤ ↑(countelements (A + B) n)
hc1 : ↑(countelements A n) * (1 - β) + β * ↑n = ↑(countelements A n) + β * (↑n - ↑(countelements A n))
hbo : ¬β = 1
hbn : 0 < 1 - schnirelmannDensity B
⊢ schnirelmannDensity A * ↑n ≤ ↑(countelements A n) * (1 - β) / (1 - schnirelmannDensity B)
Theorem: le_schnirelmannDensity_add
Proof state before:
case neg
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
lem : ⋃ a, {c | c ∈ A + B ∧ 0 < c - ↑a ∧ c ≤ next_elm A a n} ⊆ (A + B) ∩ ↑(Icc 1 n)
aux : countelements (⋃ a, {c | c ∈ A + B ∧ 0 < c - ↑a ∧ c ≤ next_elm A a n}) n ≤ countelements (A + B) n
claim :
  ↑(countelements A n) + β * (↑n - ↑(countelements A n)) ≤
    ↑(countelements (⋃ a, {c | c ∈ A + B ∧ 0 < c - ↑a ∧ c ≤ next_elm A a n}) n)
ht : ↑(countelements A n) + β * (↑n - ↑(countelements A n)) ≤ ↑(countelements (A + B) n)
hc1 : ↑(countelements A n) * (1 - β) + β * ↑n = ↑(countelements A n) + β * (↑n - ↑(countelements A n))
hbo : ¬β = 1
hbn : 0 < 1 - schnirelmannDensity B
⊢ schnirelmannDensity A * ↑n ≤ ↑(countelements A n) * (1 - β) / (1 - schnirelmannDensity B)
Tactic:
rw [mul_div_assoc]
Proof state after:
case neg
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
lem : ⋃ a, {c | c ∈ A + B ∧ 0 < c - ↑a ∧ c ≤ next_elm A a n} ⊆ (A + B) ∩ ↑(Icc 1 n)
aux : countelements (⋃ a, {c | c ∈ A + B ∧ 0 < c - ↑a ∧ c ≤ next_elm A a n}) n ≤ countelements (A + B) n
claim :
  ↑(countelements A n) + β * (↑n - ↑(countelements A n)) ≤
    ↑(countelements (⋃ a, {c | c ∈ A + B ∧ 0 < c - ↑a ∧ c ≤ next_elm A a n}) n)
ht : ↑(countelements A n) + β * (↑n - ↑(countelements A n)) ≤ ↑(countelements (A + B) n)
hc1 : ↑(countelements A n) * (1 - β) + β * ↑n = ↑(countelements A n) + β * (↑n - ↑(countelements A n))
hbo : ¬β = 1
hbn : 0 < 1 - schnirelmannDensity B
⊢ schnirelmannDensity A * ↑n ≤ ↑(countelements A n) * ((1 - β) / (1 - schnirelmannDensity B))
Theorem: le_schnirelmannDensity_add
Proof state before:
case neg
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
lem : ⋃ a, {c | c ∈ A + B ∧ 0 < c - ↑a ∧ c ≤ next_elm A a n} ⊆ (A + B) ∩ ↑(Icc 1 n)
aux : countelements (⋃ a, {c | c ∈ A + B ∧ 0 < c - ↑a ∧ c ≤ next_elm A a n}) n ≤ countelements (A + B) n
claim :
  ↑(countelements A n) + β * (↑n - ↑(countelements A n)) ≤
    ↑(countelements (⋃ a, {c | c ∈ A + B ∧ 0 < c - ↑a ∧ c ≤ next_elm A a n}) n)
ht : ↑(countelements A n) + β * (↑n - ↑(countelements A n)) ≤ ↑(countelements (A + B) n)
hc1 : ↑(countelements A n) * (1 - β) + β * ↑n = ↑(countelements A n) + β * (↑n - ↑(countelements A n))
hbo : ¬β = 1
hbn : 0 < 1 - schnirelmannDensity B
⊢ schnirelmannDensity A * ↑n ≤ ↑(countelements A n) * ((1 - β) / (1 - schnirelmannDensity B))
Tactic:
have hun : (1 - schnirelmannDensity B) / (1 - schnirelmannDensity B) = 1 := by
  rw [div_self]
  positivity
Proof state after:
case neg
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
lem : ⋃ a, {c | c ∈ A + B ∧ 0 < c - ↑a ∧ c ≤ next_elm A a n} ⊆ (A + B) ∩ ↑(Icc 1 n)
aux : countelements (⋃ a, {c | c ∈ A + B ∧ 0 < c - ↑a ∧ c ≤ next_elm A a n}) n ≤ countelements (A + B) n
claim :
  ↑(countelements A n) + β * (↑n - ↑(countelements A n)) ≤
    ↑(countelements (⋃ a, {c | c ∈ A + B ∧ 0 < c - ↑a ∧ c ≤ next_elm A a n}) n)
ht : ↑(countelements A n) + β * (↑n - ↑(countelements A n)) ≤ ↑(countelements (A + B) n)
hc1 : ↑(countelements A n) * (1 - β) + β * ↑n = ↑(countelements A n) + β * (↑n - ↑(countelements A n))
hbo : ¬β = 1
hbn : 0 < 1 - schnirelmannDensity B
hun : (1 - schnirelmannDensity B) / (1 - schnirelmannDensity B) = 1
⊢ schnirelmannDensity A * ↑n ≤ ↑(countelements A n) * ((1 - β) / (1 - schnirelmannDensity B))
Theorem: le_schnirelmannDensity_add
Proof state before:
case neg
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
lem : ⋃ a, {c | c ∈ A + B ∧ 0 < c - ↑a ∧ c ≤ next_elm A a n} ⊆ (A + B) ∩ ↑(Icc 1 n)
aux : countelements (⋃ a, {c | c ∈ A + B ∧ 0 < c - ↑a ∧ c ≤ next_elm A a n}) n ≤ countelements (A + B) n
claim :
  ↑(countelements A n) + β * (↑n - ↑(countelements A n)) ≤
    ↑(countelements (⋃ a, {c | c ∈ A + B ∧ 0 < c - ↑a ∧ c ≤ next_elm A a n}) n)
ht : ↑(countelements A n) + β * (↑n - ↑(countelements A n)) ≤ ↑(countelements (A + B) n)
hc1 : ↑(countelements A n) * (1 - β) + β * ↑n = ↑(countelements A n) + β * (↑n - ↑(countelements A n))
hbo : ¬β = 1
hbn : 0 < 1 - schnirelmannDensity B
hun : (1 - schnirelmannDensity B) / (1 - schnirelmannDensity B) = 1
⊢ schnirelmannDensity A * ↑n ≤ ↑(countelements A n) * ((1 - β) / (1 - schnirelmannDensity B))
Tactic:
rw [hun, mul_one]
Proof state after:
case neg
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
lem : ⋃ a, {c | c ∈ A + B ∧ 0 < c - ↑a ∧ c ≤ next_elm A a n} ⊆ (A + B) ∩ ↑(Icc 1 n)
aux : countelements (⋃ a, {c | c ∈ A + B ∧ 0 < c - ↑a ∧ c ≤ next_elm A a n}) n ≤ countelements (A + B) n
claim :
  ↑(countelements A n) + β * (↑n - ↑(countelements A n)) ≤
    ↑(countelements (⋃ a, {c | c ∈ A + B ∧ 0 < c - ↑a ∧ c ≤ next_elm A a n}) n)
ht : ↑(countelements A n) + β * (↑n - ↑(countelements A n)) ≤ ↑(countelements (A + B) n)
hc1 : ↑(countelements A n) * (1 - β) + β * ↑n = ↑(countelements A n) + β * (↑n - ↑(countelements A n))
hbo : ¬β = 1
hbn : 0 < 1 - schnirelmannDensity B
hun : (1 - schnirelmannDensity B) / (1 - schnirelmannDensity B) = 1
⊢ schnirelmannDensity A * ↑n ≤ ↑(countelements A n)