internlm/Lean-Github huggingface dataset:
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 : ℕ
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
Tactic:
rw [Set.mem_inter_iff] at 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 | x ∈ A + B ∧ x ≤ next_elm A ⟨i, ⋯⟩ n}
⊢ x ∈ A + B
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 : ℕ
hi : i ∈ A
x : ℕ
hx : x ∈ {x | x ∈ A + B ∧ i < x} ∧ x ∈ {x | x ∈ A + B ∧ x ≤ next_elm A ⟨i, ⋯⟩ n}
⊢ x ∈ A + B
Tactic:
simp only [Set.mem_setOf_eq] at 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 ∈ A + B ∧ i < x) ∧ x ∈ A + B ∧ x ≤ next_elm A ⟨i, ⋯⟩ n
⊢ x ∈ A + B
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 : ℕ
hi : i ∈ A
x : ℕ
hx : (x ∈ A + B ∧ i < x) ∧ x ∈ A + B ∧ x ≤ next_elm A ⟨i, ⋯⟩ n
⊢ x ∈ A + B
Tactic:
exact hx.1.1
Proof state after:
no goals
Theorem: le_schnirelmannDensity_add
Proof state before:
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
Tactic:
rcases i.eq_zero_or_pos with i0 | i1
Proof state after:
case right.left.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 - β) + β = α + β - α * β
n : ℕ
n1 : n > 0
i : ℕ
hi : i ∈ A
x : ℕ
hx : (x ∈ A + B ∧ i < x) ∧ x ∈ A + B ∧ x ≤ next_elm A ⟨i, ⋯⟩ n
i0 : i = 0
⊢ 1 ≤ x

case right.left.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
i : ℕ
hi : i ∈ A
x : ℕ
hx : (x ∈ A + B ∧ i < x) ∧ x ∈ A + B ∧ x ≤ next_elm A ⟨i, ⋯⟩ n
i1 : i > 0
⊢ 1 ≤ x
Theorem: le_schnirelmannDensity_add
Proof state before:
case right.left.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 - β) + β = α + β - α * β
n : ℕ
n1 : n > 0
i : ℕ
hi : i ∈ A
x : ℕ
hx : (x ∈ A + B ∧ i < x) ∧ x ∈ A + B ∧ x ≤ next_elm A ⟨i, ⋯⟩ n
i0 : i = 0
⊢ 1 ≤ x
Tactic:
rw [Nat.succ_le]
Proof state after:
case right.left.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 - β) + β = α + β - α * β
n : ℕ
n1 : n > 0
i : ℕ
hi : i ∈ A
x : ℕ
hx : (x ∈ A + B ∧ i < x) ∧ x ∈ A + B ∧ x ≤ next_elm A ⟨i, ⋯⟩ n
i0 : i = 0
⊢ 0 < x
Theorem: le_schnirelmannDensity_add
Proof state before:
case right.left.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 - β) + β = α + β - α * β
n : ℕ
n1 : n > 0
i : ℕ
hi : i ∈ A
x : ℕ
hx : (x ∈ A + B ∧ i < x) ∧ x ∈ A + B ∧ x ≤ next_elm A ⟨i, ⋯⟩ n
i0 : i = 0
⊢ 0 < x
Tactic:
rw [← i0]
Proof state after:
case right.left.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 - β) + β = α + β - α * β
n : ℕ
n1 : n > 0
i : ℕ
hi : i ∈ A
x : ℕ
hx : (x ∈ A + B ∧ i < x) ∧ x ∈ A + B ∧ x ≤ next_elm A ⟨i, ⋯⟩ n
i0 : i = 0
⊢ i < x
Theorem: le_schnirelmannDensity_add
Proof state before:
case right.left.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 - β) + β = α + β - α * β
n : ℕ
n1 : n > 0
i : ℕ
hi : i ∈ A
x : ℕ
hx : (x ∈ A + B ∧ i < x) ∧ x ∈ A + B ∧ x ≤ next_elm A ⟨i, ⋯⟩ n
i0 : i = 0
⊢ i < x
Tactic:
exact hx.1.2
Proof state after:
no goals
Theorem: le_schnirelmannDensity_add
Proof state before:
case right.left.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
i : ℕ
hi : i ∈ A
x : ℕ
hx : (x ∈ A + B ∧ i < x) ∧ x ∈ A + B ∧ x ≤ next_elm A ⟨i, ⋯⟩ n
i1 : i > 0
⊢ 1 ≤ x
Tactic:
rw [Nat.succ_le]
Proof state after:
case right.left.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
i : ℕ
hi : i ∈ A
x : ℕ
hx : (x ∈ A + B ∧ i < x) ∧ x ∈ A + B ∧ x ≤ next_elm A ⟨i, ⋯⟩ n
i1 : i > 0
⊢ 0 < x
Theorem: le_schnirelmannDensity_add
Proof state before:
case right.left.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
i : ℕ
hi : i ∈ A
x : ℕ
hx : (x ∈ A + B ∧ i < x) ∧ x ∈ A + B ∧ x ≤ next_elm A ⟨i, ⋯⟩ n
i1 : i > 0
⊢ 0 < x
Tactic:
apply lt_trans i1 hx.1.2
Proof state after:
no goals
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
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
Tactic:
exact hx3.trans (mem_Ioc.1 (mem_filter.1 $ min'_mem _ _).1).2
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
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
Tactic:
simpa using hx3
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)
⊢ countelements (⋃ a, {c | c ∈ A + B ∧ 0 < c - ↑a ∧ c ≤ next_elm A a n}) n ≤ countelements (A + B) n
Tactic:
rw [countelements, countelements]
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)
⊢ (filter (fun x => x ∈ ⋃ a, {c | c ∈ A + B ∧ 0 < c - ↑a ∧ c ≤ next_elm A a n}) (Icc 1 n)).card ≤
    (filter (fun x => x ∈ A + B) (Icc 1 n)).card
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)
⊢ (filter (fun x => x ∈ ⋃ a, {c | c ∈ A + B ∧ 0 < c - ↑a ∧ c ≤ next_elm A a n}) (Icc 1 n)).card ≤
    (filter (fun x => x ∈ A + B) (Icc 1 n)).card
Tactic:
apply card_le_card
Proof state after:
case a
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)
⊢ filter (fun x => x ∈ ⋃ a, {c | c ∈ A + B ∧ 0 < c - ↑a ∧ c ≤ next_elm A a n}) (Icc 1 n) ⊆
    filter (fun x => x ∈ A + B) (Icc 1 n)
Theorem: le_schnirelmannDensity_add
Proof state before:
case a
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)
⊢ filter (fun x => x ∈ ⋃ a, {c | c ∈ A + B ∧ 0 < c - ↑a ∧ c ≤ next_elm A a n}) (Icc 1 n) ⊆
    filter (fun x => x ∈ A + B) (Icc 1 n)
Tactic:
intro y
Proof state after:
case a
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)
y : ℕ
⊢ y ∈ filter (fun x => x ∈ ⋃ a, {c | c ∈ A + B ∧ 0 < c - ↑a ∧ c ≤ next_elm A a n}) (Icc 1 n) →
    y ∈ filter (fun x => x ∈ A + B) (Icc 1 n)
Theorem: le_schnirelmannDensity_add
Proof state before:
case a
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)
y : ℕ
⊢ y ∈ filter (fun x => x ∈ ⋃ a, {c | c ∈ A + B ∧ 0 < c - ↑a ∧ c ≤ next_elm A a n}) (Icc 1 n) →
    y ∈ filter (fun x => x ∈ A + B) (Icc 1 n)
Tactic:
repeat rw [mem_filter]
Proof state after:
case a
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)
y : ℕ
⊢ y ∈ Icc 1 n ∧ y ∈ ⋃ a, {c | c ∈ A + B ∧ 0 < c - ↑a ∧ c ≤ next_elm A a n} → y ∈ Icc 1 n ∧ y ∈ A + B
Theorem: le_schnirelmannDensity_add
Proof state before:
case a
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)
y : ℕ
⊢ y ∈ Icc 1 n ∧ y ∈ ⋃ a, {c | c ∈ A + B ∧ 0 < c - ↑a ∧ c ≤ next_elm A a n} → y ∈ Icc 1 n ∧ y ∈ A + B
Tactic:
intro hy
Proof state after:
case a
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)
y : ℕ
hy : y ∈ Icc 1 n ∧ y ∈ ⋃ a, {c | c ∈ A + B ∧ 0 < c - ↑a ∧ c ≤ next_elm A a n}
⊢ y ∈ Icc 1 n ∧ y ∈ A + B
Theorem: le_schnirelmannDensity_add
Proof state before:
case a
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)
y : ℕ
hy : y ∈ Icc 1 n ∧ y ∈ ⋃ a, {c | c ∈ A + B ∧ 0 < c - ↑a ∧ c ≤ next_elm A a n}
⊢ y ∈ Icc 1 n ∧ y ∈ A + B
Tactic:
constructor
Proof state after:
case a.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
lem : ⋃ a, {c | c ∈ A + B ∧ 0 < c - ↑a ∧ c ≤ next_elm A a n} ⊆ (A + B) ∩ ↑(Icc 1 n)
y : ℕ
hy : y ∈ Icc 1 n ∧ y ∈ ⋃ a, {c | c ∈ A + B ∧ 0 < c - ↑a ∧ c ≤ next_elm A a n}
⊢ y ∈ Icc 1 n

case a.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
lem : ⋃ a, {c | c ∈ A + B ∧ 0 < c - ↑a ∧ c ≤ next_elm A a n} ⊆ (A + B) ∩ ↑(Icc 1 n)
y : ℕ
hy : y ∈ Icc 1 n ∧ y ∈ ⋃ a, {c | c ∈ A + B ∧ 0 < c - ↑a ∧ c ≤ next_elm A a n}
⊢ y ∈ A + B
Theorem: le_schnirelmannDensity_add
Proof state before:
case a
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)
y : ℕ
⊢ y ∈ Icc 1 n ∧ y ∈ ⋃ a, {c | c ∈ A + B ∧ 0 < c - ↑a ∧ c ≤ next_elm A a n} → y ∈ filter (fun x => x ∈ A + B) (Icc 1 n)
Tactic:
rw [mem_filter]
Proof state after:
case a
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)
y : ℕ
⊢ y ∈ Icc 1 n ∧ y ∈ ⋃ a, {c | c ∈ A + B ∧ 0 < c - ↑a ∧ c ≤ next_elm A a n} → y ∈ Icc 1 n ∧ y ∈ A + B
Theorem: le_schnirelmannDensity_add
Proof state before:
case a.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
lem : ⋃ a, {c | c ∈ A + B ∧ 0 < c - ↑a ∧ c ≤ next_elm A a n} ⊆ (A + B) ∩ ↑(Icc 1 n)
y : ℕ
hy : y ∈ Icc 1 n ∧ y ∈ ⋃ a, {c | c ∈ A + B ∧ 0 < c - ↑a ∧ c ≤ next_elm A a n}
⊢ y ∈ Icc 1 n
Tactic:
exact hy.1
Proof state after:
no goals
Theorem: le_schnirelmannDensity_add
Proof state before:
case a.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
lem : ⋃ a, {c | c ∈ A + B ∧ 0 < c - ↑a ∧ c ≤ next_elm A a n} ⊆ (A + B) ∩ ↑(Icc 1 n)
y : ℕ
hy : y ∈ Icc 1 n ∧ y ∈ ⋃ a, {c | c ∈ A + B ∧ 0 < c - ↑a ∧ c ≤ next_elm A a n}
⊢ y ∈ A + B
Tactic:
obtain ⟨hy1, hy2⟩ := hy
Proof state after:
case a.right.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
lem : ⋃ a, {c | c ∈ A + B ∧ 0 < c - ↑a ∧ c ≤ next_elm A a n} ⊆ (A + B) ∩ ↑(Icc 1 n)
y : ℕ
hy1 : y ∈ Icc 1 n
hy2 : y ∈ ⋃ a, {c | c ∈ A + B ∧ 0 < c - ↑a ∧ c ≤ next_elm A a n}
⊢ y ∈ A + B
Theorem: le_schnirelmannDensity_add
Proof state before:
case a.right.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
lem : ⋃ a, {c | c ∈ A + B ∧ 0 < c - ↑a ∧ c ≤ next_elm A a n} ⊆ (A + B) ∩ ↑(Icc 1 n)
y : ℕ
hy1 : y ∈ Icc 1 n
hy2 : y ∈ ⋃ a, {c | c ∈ A + B ∧ 0 < c - ↑a ∧ c ≤ next_elm A a n}
⊢ y ∈ A + B
Tactic:
have hs : y ∈ (A + B) ∩ (Icc 1 n) := by aesop
Proof state after:
case a.right.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
lem : ⋃ a, {c | c ∈ A + B ∧ 0 < c - ↑a ∧ c ≤ next_elm A a n} ⊆ (A + B) ∩ ↑(Icc 1 n)
y : ℕ
hy1 : y ∈ Icc 1 n
hy2 : y ∈ ⋃ a, {c | c ∈ A + B ∧ 0 < c - ↑a ∧ c ≤ next_elm A a n}
hs : y ∈ (A + B) ∩ ↑(Icc 1 n)
⊢ y ∈ A + B
Theorem: le_schnirelmannDensity_add
Proof state before:
case a.right.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
lem : ⋃ a, {c | c ∈ A + B ∧ 0 < c - ↑a ∧ c ≤ next_elm A a n} ⊆ (A + B) ∩ ↑(Icc 1 n)
y : ℕ
hy1 : y ∈ Icc 1 n
hy2 : y ∈ ⋃ a, {c | c ∈ A + B ∧ 0 < c - ↑a ∧ c ≤ next_elm A a n}
hs : y ∈ (A + B) ∩ ↑(Icc 1 n)
⊢ y ∈ A + B
Tactic:
rw [Set.mem_inter_iff] at hs
Proof state after:
case a.right.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
lem : ⋃ a, {c | c ∈ A + B ∧ 0 < c - ↑a ∧ c ≤ next_elm A a n} ⊆ (A + B) ∩ ↑(Icc 1 n)
y : ℕ
hy1 : y ∈ Icc 1 n
hy2 : y ∈ ⋃ a, {c | c ∈ A + B ∧ 0 < c - ↑a ∧ c ≤ next_elm A a n}
hs : y ∈ A + B ∧ y ∈ ↑(Icc 1 n)
⊢ y ∈ A + B
Theorem: le_schnirelmannDensity_add
Proof state before:
case a.right.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
lem : ⋃ a, {c | c ∈ A + B ∧ 0 < c - ↑a ∧ c ≤ next_elm A a n} ⊆ (A + B) ∩ ↑(Icc 1 n)
y : ℕ
hy1 : y ∈ Icc 1 n
hy2 : y ∈ ⋃ a, {c | c ∈ A + B ∧ 0 < c - ↑a ∧ c ≤ next_elm A a n}
hs : y ∈ A + B ∧ y ∈ ↑(Icc 1 n)
⊢ y ∈ A + B
Tactic:
exact hs.1
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)
y : ℕ
hy1 : y ∈ Icc 1 n
hy2 : y ∈ ⋃ a, {c | c ∈ A + B ∧ 0 < c - ↑a ∧ c ≤ next_elm A a n}
⊢ y ∈ (A + B) ∩ ↑(Icc 1 n)
Tactic:
aesop
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
⊢ ↑(countelements A n) + β * (↑n - ↑(countelements A n)) ≤
    ↑(countelements (⋃ a, {c | c ∈ A + B ∧ 0 < c - ↑a ∧ c ≤ next_elm A a n}) n)
Tactic:
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
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
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
⊢ ↑(countelements A n) + β * (↑n - ↑(countelements A n)) ≤
    ↑(countelements (⋃ a, {c | c ∈ A + B ∧ 0 < c - ↑a ∧ c ≤ next_elm A a n}) 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
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
⊢ ↑(countelements A n) + β * (↑n - ↑(countelements A n)) ≤
    ↑(countelements (⋃ a, {c | c ∈ A + B ∧ 0 < c - ↑a ∧ c ≤ next_elm A a n}) n)
Tactic:
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
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
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
hax :
  ∀ (a x : ↑A),
    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} = ∅
⊢ ↑(countelements A n) + β * (↑n - ↑(countelements A n)) ≤
    ↑(countelements (⋃ a, {c | c ∈ A + B ∧ 0 < c - ↑a ∧ c ≤ next_elm A a n}) 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
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
hax :
  ∀ (a x : ↑A),
    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} = ∅
⊢ ↑(countelements A n) + β * (↑n - ↑(countelements A n)) ≤
    ↑(countelements (⋃ a, {c | c ∈ A + B ∧ 0 < c - ↑a ∧ c ≤ next_elm A a n}) n)
Tactic:
sorry
Proof state after:
no goals