internlm/Lean-Github huggingface dataset:
Theorem: le_schnirelmannDensity_add
Proof state before:
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)
Tactic:
ring_nf
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 - β) + β = α + β - α * β
⊢ 0 ≤ ↑(countelements (A + B) 0)
Theorem: le_schnirelmannDensity_add
Proof state before:
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 - β) + β = α + β - α * β
⊢ 0 ≤ ↑(countelements (A + B) 0)
Tactic:
positivity
Proof state after:
no goals
Theorem: le_schnirelmannDensity_add
Proof state before:
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
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
⊢ (α * (1 - β) + β) * ↑n ≤ ↑(countelements (A + B) n)
Tactic:
have claim : countelements A n + β * (n - countelements A n) ≤
  countelements (⋃ a : A, {c ∈ A + B | 0 < c - a ∧ (c : ℕ) ≤ (next_elm A a n)}) n := by
  have hcc (a : A) :
    1 + countelements B (next_elm A a n - a - 1) ≤
    countelements {c ∈ A + B | 0 < c - a ∧ (c : ℕ) ≤ (next_elm A a n)} n := by
    sorry
  have hax (a x : A) (hh : a ≠ x) :
    {c ∈ A + B | 0 < c - a ∧ (c : ℕ) ≤ (next_elm A a n)} ∩
    {c ∈ A + B | 0 < c - x ∧ (c : ℕ) ≤ next_elm A x n} = ∅ := by sorry
    sorry
Proof state after:
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
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)
⊢ (α * (1 - β) + β) * ↑n ≤ ↑(countelements (A + B) n)
Theorem: le_schnirelmannDensity_add
Proof state before:
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
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)
⊢ (α * (1 - β) + β) * ↑n ≤ ↑(countelements (A + B) n)
Tactic:
have ht : countelements A n + β * (n - countelements A n) ≤ countelements (A + B) n := by
  apply le_trans claim _
  norm_cast
Proof state after:
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
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)
⊢ (α * (1 - β) + β) * ↑n ≤ ↑(countelements (A + B) n)
Theorem: le_schnirelmannDensity_add
Proof state before:
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
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)
⊢ (α * (1 - β) + β) * ↑n ≤ ↑(countelements (A + B) n)
Tactic:
have hc1 : countelements A n * (1 - β) + β * n =
  countelements A n + β * (n - countelements A n) := by ring_nf
Proof state after:
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
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))
⊢ (α * (1 - β) + β) * ↑n ≤ ↑(countelements (A + B) n)
Theorem: le_schnirelmannDensity_add
Proof state before:
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
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))
hc2 : α * ↑n * (1 - β) + β * ↑n ≤ ↑(countelements A n) * (1 - β) + β * ↑n
⊢ (α * (1 - β) + β) * ↑n ≤ ↑(countelements (A + B) n)
Tactic:
have hc3 : α * n * (1 - β) + β * n = (α * (1 - β) + β) * n := by ring_nf
Proof state after:
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
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))
hc2 : α * ↑n * (1 - β) + β * ↑n ≤ ↑(countelements A n) * (1 - β) + β * ↑n
hc3 : α * ↑n * (1 - β) + β * ↑n = (α * (1 - β) + β) * ↑n
⊢ (α * (1 - β) + β) * ↑n ≤ ↑(countelements (A + B) n)
Theorem: le_schnirelmannDensity_add
Proof state before:
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
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))
hc2 : α * ↑n * (1 - β) + β * ↑n ≤ ↑(countelements A n) * (1 - β) + β * ↑n
hc3 : α * ↑n * (1 - β) + β * ↑n = (α * (1 - β) + β) * ↑n
⊢ (α * (1 - β) + β) * ↑n ≤ ↑(countelements (A + B) n)
Tactic:
rw [hc1] at hc2
Proof state after:
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
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))
hc2 : α * ↑n * (1 - β) + β * ↑n ≤ ↑(countelements A n) + β * (↑n - ↑(countelements A n))
hc3 : α * ↑n * (1 - β) + β * ↑n = (α * (1 - β) + β) * ↑n
⊢ (α * (1 - β) + β) * ↑n ≤ ↑(countelements (A + B) n)
Theorem: le_schnirelmannDensity_add
Proof state before:
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
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))
hc2 : α * ↑n * (1 - β) + β * ↑n ≤ ↑(countelements A n) + β * (↑n - ↑(countelements A n))
hc3 : α * ↑n * (1 - β) + β * ↑n = (α * (1 - β) + β) * ↑n
⊢ (α * (1 - β) + β) * ↑n ≤ ↑(countelements (A + B) n)
Tactic:
rw [hc3] at hc2
Proof state after:
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
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))
hc2 : (α * (1 - β) + β) * ↑n ≤ ↑(countelements A n) + β * (↑n - ↑(countelements A n))
hc3 : α * ↑n * (1 - β) + β * ↑n = (α * (1 - β) + β) * ↑n
⊢ (α * (1 - β) + β) * ↑n ≤ ↑(countelements (A + B) n)
Theorem: le_schnirelmannDensity_add
Proof state before:
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
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))
hc2 : (α * (1 - β) + β) * ↑n ≤ ↑(countelements A n) + β * (↑n - ↑(countelements A n))
hc3 : α * ↑n * (1 - β) + β * ↑n = (α * (1 - β) + β) * ↑n
⊢ (α * (1 - β) + β) * ↑n ≤ ↑(countelements (A + B) n)
Tactic:
exact le_trans hc2 ht
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
⊢ ⋃ a, {c | c ∈ A + B ∧ 0 < c - ↑a ∧ c ≤ next_elm A a n} ⊆ (A + B) ∩ ↑(Icc 1 n)
Tactic:
simp only [tsub_pos_iff_lt, Set.sep_and, Set.iUnion_coe_set, Nat.lt_one_iff, coe_Icc, not_le,
  Set.subset_inter_iff, Set.iUnion_subset_iff]
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
⊢ (∀ (i : ℕ) (i_1 : i ∈ A), {x | x ∈ A + B ∧ i < x} ∩ {x | x ∈ A + B ∧ x ≤ next_elm A ⟨i, ⋯⟩ n} ⊆ A + B) ∧
    ∀ (i : ℕ) (i_1 : i ∈ A), {x | x ∈ A + B ∧ i < x} ∩ {x | x ∈ A + B ∧ x ≤ next_elm A ⟨i, ⋯⟩ n} ⊆ Set.Icc 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
⊢ (∀ (i : ℕ) (i_1 : i ∈ A), {x | x ∈ A + B ∧ i < x} ∩ {x | x ∈ A + B ∧ x ≤ next_elm A ⟨i, ⋯⟩ n} ⊆ A + B) ∧
    ∀ (i : ℕ) (i_1 : i ∈ A), {x | x ∈ A + B ∧ i < x} ∩ {x | x ∈ A + B ∧ x ≤ next_elm A ⟨i, ⋯⟩ n} ⊆ Set.Icc 1 n
Tactic:
constructor
Proof state after:
case left
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
⊢ ∀ (i : ℕ) (i_1 : i ∈ A), {x | x ∈ A + B ∧ i < x} ∩ {x | x ∈ A + B ∧ x ≤ next_elm A ⟨i, ⋯⟩ n} ⊆ A + B

case right
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
⊢ ∀ (i : ℕ) (i_1 : i ∈ A), {x | x ∈ A + B ∧ i < x} ∩ {x | x ∈ A + B ∧ x ≤ next_elm A ⟨i, ⋯⟩ n} ⊆ Set.Icc 1 n
Theorem: le_schnirelmannDensity_add
Proof state before:
case right
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
⊢ ∀ (i : ℕ) (i_1 : i ∈ A), {x | x ∈ A + B ∧ i < x} ∩ {x | x ∈ A + B ∧ x ≤ next_elm A ⟨i, ⋯⟩ n} ⊆ Set.Icc 1 n
Tactic:
intro i hi x hx
Proof state after:
case right
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
i : ℕ
hi : i ∈ A
x : ℕ
hx : x ∈ {x | x ∈ A + B ∧ i < x} ∩ {x | x ∈ A + B ∧ x ≤ next_elm A ⟨i, ⋯⟩ n}
⊢ x ∈ Set.Icc 1 n
Theorem: le_schnirelmannDensity_add
Proof state before:
case right
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
i : ℕ
hi : i ∈ A
x : ℕ
hx : x ∈ {x | x ∈ A + B ∧ i < x} ∩ {x | x ∈ A + B ∧ x ≤ next_elm A ⟨i, ⋯⟩ n}
⊢ x ∈ Set.Icc 1 n
Tactic:
simp only [Set.mem_inter_iff, Set.mem_setOf_eq] at hx
Proof state after:
case right
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
i : ℕ
hi : i ∈ A
x : ℕ
hx : (x ∈ A + B ∧ i < x) ∧ x ∈ A + B ∧ x ≤ next_elm A ⟨i, ⋯⟩ n
⊢ x ∈ Set.Icc 1 n
Theorem: le_schnirelmannDensity_add
Proof state before:
case right
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
i : ℕ
hi : i ∈ A
x : ℕ
hx : (x ∈ A + B ∧ i < x) ∧ x ∈ A + B ∧ x ≤ next_elm A ⟨i, ⋯⟩ n
⊢ x ∈ Set.Icc 1 n
Tactic:
rw [Set.mem_Icc]
Proof state after:
case right
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
i : ℕ
hi : i ∈ A
x : ℕ
hx : (x ∈ A + B ∧ i < x) ∧ x ∈ A + B ∧ x ≤ next_elm A ⟨i, ⋯⟩ n
⊢ 1 ≤ x ∧ x ≤ n
Theorem: le_schnirelmannDensity_add
Proof state before:
case right
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
i : ℕ
hi : i ∈ A
x : ℕ
hx : (x ∈ A + B ∧ i < x) ∧ x ∈ A + B ∧ x ≤ next_elm A ⟨i, ⋯⟩ n
⊢ 1 ≤ x ∧ x ≤ n
Tactic:
constructor
Proof state after:
case right.left
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
i : ℕ
hi : i ∈ A
x : ℕ
hx : (x ∈ A + B ∧ i < x) ∧ x ∈ A + B ∧ x ≤ next_elm A ⟨i, ⋯⟩ n
⊢ 1 ≤ x

case right.right
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
i : ℕ
hi : i ∈ A
x : ℕ
hx : (x ∈ A + B ∧ i < x) ∧ x ∈ A + B ∧ x ≤ next_elm A ⟨i, ⋯⟩ n
⊢ x ≤ n
Theorem: le_schnirelmannDensity_add
Proof state before:
case right.right
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
i : ℕ
hi : i ∈ A
x : ℕ
hx : (x ∈ A + B ∧ i < x) ∧ x ∈ A + B ∧ x ≤ next_elm A ⟨i, ⋯⟩ n
⊢ x ≤ n
Tactic:
obtain ⟨hx1, hx2, hx3⟩ := hx
Proof state after:
case right.right.intro.intro
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
i : ℕ
hi : i ∈ A
x : ℕ
hx1 : x ∈ A + B ∧ i < x
hx2 : x ∈ A + B
hx3 : x ≤ next_elm A ⟨i, ⋯⟩ n
⊢ x ≤ n
Theorem: le_schnirelmannDensity_add
Proof state before:
case right.right.intro.intro
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
i : ℕ
hi : i ∈ A
x : ℕ
hx1 : x ∈ A + B ∧ i < x
hx2 : x ∈ A + B
hx3 : x ≤ next_elm A ⟨i, ⋯⟩ n
⊢ x ≤ n
Tactic:
rw [next_elm] at hx3
Proof state after:
case right.right.intro.intro
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
i : ℕ
hi : i ∈ A
x : ℕ
hx1 : x ∈ A + B ∧ i < x
hx2 : x ∈ A + B
hx3 :
  x ≤
    if h : (filter (fun x => x ∈ A) (Ioc (↑⟨i, ⋯⟩) n)).Nonempty then (filter (fun x => x ∈ A) (Ioc (↑⟨i, ⋯⟩) n)).min' h
    else n
⊢ x ≤ n
Theorem: le_schnirelmannDensity_add
Proof state before:
case right.right.intro.intro
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
i : ℕ
hi : i ∈ A
x : ℕ
hx1 : x ∈ A + B ∧ i < x
hx2 : x ∈ A + B
hx3 :
  x ≤
    if h : (filter (fun x => x ∈ A) (Ioc (↑⟨i, ⋯⟩) n)).Nonempty then (filter (fun x => x ∈ A) (Ioc (↑⟨i, ⋯⟩) n)).min' h
    else n
⊢ x ≤ n
Tactic:
simp only [mem_Ioc, and_imp, ne_eq, ite_not] at hx3
Proof state after:
case right.right.intro.intro
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
i : ℕ
hi : i ∈ A
x : ℕ
hx1 : x ∈ A + B ∧ i < x
hx2 : x ∈ A + B
hx3 : x ≤ if h : (filter (fun x => x ∈ A) (Ioc i n)).Nonempty then (filter (fun x => x ∈ A) (Ioc i n)).min' ⋯ else n
⊢ x ≤ n
Theorem: le_schnirelmannDensity_add
Proof state before:
case right.right.intro.intro
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
i : ℕ
hi : i ∈ A
x : ℕ
hx1 : x ∈ A + B ∧ i < x
hx2 : x ∈ A + B
hx3 : x ≤ if h : (filter (fun x => x ∈ A) (Ioc i n)).Nonempty then (filter (fun x => x ∈ A) (Ioc i n)).min' ⋯ else n
⊢ x ≤ n
Tactic:
split_ifs at hx3 with h
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
i : ℕ
hi : i ∈ A
x : ℕ
hx1 : x ∈ A + B ∧ i < x
hx2 : x ∈ A + B
h : (filter (fun x => x ∈ A) (Ioc i n)).Nonempty
hx3 : x ≤ (filter (fun x => x ∈ A) (Ioc i n)).min' ⋯
⊢ x ≤ 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
i : ℕ
hi : i ∈ A
x : ℕ
hx1 : x ∈ A + B ∧ i < x
hx2 : x ∈ A + B
h : ¬(filter (fun x => x ∈ A) (Ioc i n)).Nonempty
hx3 : x ≤ n
⊢ x ≤ n
Theorem: le_schnirelmannDensity_add
Proof state before:
case left
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
⊢ ∀ (i : ℕ) (i_1 : i ∈ A), {x | x ∈ A + B ∧ i < x} ∩ {x | x ∈ A + B ∧ x ≤ next_elm A ⟨i, ⋯⟩ n} ⊆ A + B
Tactic:
intro i hi x hx
Proof state after:
case left
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
i : ℕ
hi : i ∈ A
x : ℕ
hx : x ∈ {x | x ∈ A + B ∧ i < x} ∩ {x | x ∈ A + B ∧ x ≤ next_elm A ⟨i, ⋯⟩ n}
⊢ x ∈ A + B