internlm/Lean-Github huggingface dataset:
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)
Tactic:
exact schnirelmannDensity_mul_le_card_filter
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))
hbo : ¬β = 1
⊢ 0 < 1 - schnirelmannDensity B
Tactic:
rw [hbeta] at hbo
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))
hbo : ¬schnirelmannDensity B = 1
⊢ 0 < 1 - schnirelmannDensity 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 : ℕ
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 : ¬schnirelmannDensity B = 1
⊢ 0 < 1 - schnirelmannDensity B
Tactic:
rw [lt_sub_iff_add_lt, zero_add, lt_iff_le_and_ne]
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))
hbo : ¬schnirelmannDensity B = 1
⊢ schnirelmannDensity B ≤ 1 ∧ schnirelmannDensity B ≠ 1
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))
hbo : ¬schnirelmannDensity B = 1
⊢ schnirelmannDensity B ≤ 1 ∧ schnirelmannDensity B ≠ 1
Tactic:
exact ⟨schnirelmannDensity_le_one, hbo⟩
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))
hbo : ¬β = 1
hbn : 0 < 1 - schnirelmannDensity B
⊢ (1 - schnirelmannDensity B) / (1 - schnirelmannDensity B) = 1
Tactic:
rw [div_self]
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))
hbo : ¬β = 1
hbn : 0 < 1 - schnirelmannDensity B
⊢ 1 - schnirelmannDensity B ≠ 0
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))
hbo : ¬β = 1
hbn : 0 < 1 - schnirelmannDensity B
⊢ 1 - schnirelmannDensity B ≠ 0
Tactic:
positivity
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))
hc2 : α * ↑n * (1 - β) + β * ↑n ≤ ↑(countelements A n) * (1 - β) + β * ↑n
⊢ α * ↑n * (1 - β) + β * ↑n = (α * (1 - β) + β) * ↑n
Tactic:
ring_nf
Proof state after:
no goals
Theorem: schnirelmannDensity_for_two
Proof state before:
A✝ B✝ : Set ℕ
n : ℕ
A B : Set ℕ
hA : 0 ∈ A
hB : 0 ∈ B
⊢ 1 - schnirelmannDensity (A + B) ≤ (1 - schnirelmannDensity A) * (1 - schnirelmannDensity B)
Tactic:
let α := schnirelmannDensity A
Proof state after:
A✝ B✝ : Set ℕ
n : ℕ
A B : Set ℕ
hA : 0 ∈ A
hB : 0 ∈ B
α : ℝ := schnirelmannDensity A
⊢ 1 - schnirelmannDensity (A + B) ≤ (1 - schnirelmannDensity A) * (1 - schnirelmannDensity B)
Theorem: schnirelmannDensity_for_two
Proof state before:
A✝ B✝ : Set ℕ
n : ℕ
A B : Set ℕ
hA : 0 ∈ A
hB : 0 ∈ B
α : ℝ := schnirelmannDensity A
⊢ 1 - schnirelmannDensity (A + B) ≤ (1 - schnirelmannDensity A) * (1 - schnirelmannDensity B)
Tactic:
have halpha : α = schnirelmannDensity A := rfl
Proof state after:
A✝ B✝ : Set ℕ
n : ℕ
A B : Set ℕ
hA : 0 ∈ A
hB : 0 ∈ B
α : ℝ := schnirelmannDensity A
halpha : α = schnirelmannDensity A
⊢ 1 - schnirelmannDensity (A + B) ≤ (1 - schnirelmannDensity A) * (1 - schnirelmannDensity B)
Theorem: schnirelmannDensity_for_two
Proof state before:
A✝ B✝ : Set ℕ
n : ℕ
A B : Set ℕ
hA : 0 ∈ A
hB : 0 ∈ B
α : ℝ := schnirelmannDensity A
halpha : α = schnirelmannDensity A
⊢ 1 - schnirelmannDensity (A + B) ≤ (1 - schnirelmannDensity A) * (1 - schnirelmannDensity B)
Tactic:
let β := schnirelmannDensity B
Proof state after:
A✝ B✝ : Set ℕ
n : ℕ
A B : Set ℕ
hA : 0 ∈ A
hB : 0 ∈ B
α : ℝ := schnirelmannDensity A
halpha : α = schnirelmannDensity A
β : ℝ := schnirelmannDensity B
⊢ 1 - schnirelmannDensity (A + B) ≤ (1 - schnirelmannDensity A) * (1 - schnirelmannDensity B)
Theorem: schnirelmannDensity_for_two
Proof state before:
A✝ B✝ : Set ℕ
n : ℕ
A B : Set ℕ
hA : 0 ∈ A
hB : 0 ∈ B
α : ℝ := schnirelmannDensity A
halpha : α = schnirelmannDensity A
β : ℝ := schnirelmannDensity B
⊢ 1 - schnirelmannDensity (A + B) ≤ (1 - schnirelmannDensity A) * (1 - schnirelmannDensity B)
Tactic:
have hbeta : β = schnirelmannDensity B := rfl
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
⊢ 1 - schnirelmannDensity (A + B) ≤ (1 - schnirelmannDensity A) * (1 - schnirelmannDensity B)
Theorem: schnirelmannDensity_for_two
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 - schnirelmannDensity (A + B) ≤ (1 - schnirelmannDensity A) * (1 - schnirelmannDensity B)
Tactic:
let γ := schnirelmannDensity (A + B)
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)
⊢ 1 - schnirelmannDensity (A + B) ≤ (1 - schnirelmannDensity A) * (1 - schnirelmannDensity B)
Theorem: schnirelmannDensity_for_two
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)
⊢ 1 - schnirelmannDensity (A + B) ≤ (1 - schnirelmannDensity A) * (1 - schnirelmannDensity B)
Tactic:
have hgamma : γ = schnirelmannDensity (A + B) := rfl
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)
hgamma : γ = schnirelmannDensity (A + B)
⊢ 1 - schnirelmannDensity (A + B) ≤ (1 - schnirelmannDensity A) * (1 - schnirelmannDensity B)
Theorem: schnirelmannDensity_for_two
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)
hgamma : γ = schnirelmannDensity (A + B)
⊢ 1 - schnirelmannDensity (A + B) ≤ (1 - schnirelmannDensity A) * (1 - schnirelmannDensity B)
Tactic:
rw [← halpha, ← hbeta, ← hgamma]
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)
hgamma : γ = schnirelmannDensity (A + B)
⊢ 1 - γ ≤ (1 - α) * (1 - β)
Theorem: schnirelmannDensity_for_two
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)
hgamma : γ = schnirelmannDensity (A + B)
h : 1 - γ ≤ 1 - (α + β - α * β)
⊢ 1 - γ ≤ (1 - α) * (1 - β)
Tactic:
linarith
Proof state after:
no goals
Theorem: schnirelmannDensity_for_two
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)
hgamma : γ = schnirelmannDensity (A + B)
⊢ 1 - γ ≤ 1 - (α + β - α * β)
Tactic:
rw [sub_le_iff_le_add, add_comm_sub]
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)
hgamma : γ = schnirelmannDensity (A + B)
⊢ 1 ≤ 1 + (γ - (α + β - α * β))
Theorem: schnirelmannDensity_for_two
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)
hgamma : γ = schnirelmannDensity (A + B)
⊢ 1 ≤ 1 + (γ - (α + β - α * β))
Tactic:
nth_rewrite 1 [← add_zero 1]
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)
hgamma : γ = schnirelmannDensity (A + B)
⊢ 1 + 0 ≤ 1 + (γ - (α + β - α * β))
Theorem: schnirelmannDensity_for_two
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)
hgamma : γ = schnirelmannDensity (A + B)
⊢ 1 + 0 ≤ 1 + (γ - (α + β - α * β))
Tactic:
rw [add_le_add_iff_left, le_sub_comm, sub_zero]
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)
hgamma : γ = schnirelmannDensity (A + B)
⊢ α + β - α * β ≤ γ
Theorem: schnirelmannDensity_for_two
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)
hgamma : γ = schnirelmannDensity (A + B)
⊢ α + β - α * β ≤ γ
Tactic:
rw [sub_eq_add_neg]
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)
hgamma : γ = schnirelmannDensity (A + B)
⊢ α + β + -(α * β) ≤ γ
Theorem: schnirelmannDensity_for_two
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)
hgamma : γ = schnirelmannDensity (A + B)
h0 : α + β - α * β ≤ γ
⊢ α + β + -(α * β) ≤ γ
Tactic:
exact h0
Proof state after:
no goals
Theorem: schnirelmannDensity_for_two
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)
hgamma : γ = schnirelmannDensity (A + B)
⊢ α + β - α * β ≤ γ
Tactic:
rw [halpha, hbeta, hgamma]
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)
hgamma : γ = schnirelmannDensity (A + B)
⊢ schnirelmannDensity A + schnirelmannDensity B - schnirelmannDensity A * schnirelmannDensity B ≤
    schnirelmannDensity (A + B)
Theorem: schnirelmannDensity_for_two
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)
hgamma : γ = schnirelmannDensity (A + B)
⊢ schnirelmannDensity A + schnirelmannDensity B - schnirelmannDensity A * schnirelmannDensity B ≤
    schnirelmannDensity (A + B)
Tactic:
apply le_schnirelmannDensity_add A B
Proof state after:
case hA
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)
hgamma : γ = schnirelmannDensity (A + B)
⊢ 0 ∈ A

case hB
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)
hgamma : γ = schnirelmannDensity (A + B)
⊢ 0 ∈ B
Theorem: schnirelmannDensity_for_two
Proof state before:
case hA
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)
hgamma : γ = schnirelmannDensity (A + B)
⊢ 0 ∈ A
Tactic:
exact hA
Proof state after:
no goals
Theorem: schnirelmannDensity_for_two
Proof state before:
case hB
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)
hgamma : γ = schnirelmannDensity (A + B)
⊢ 0 ∈ B
Tactic:
exact hB
Proof state after:
no goals
Theorem: mannTheorem
Proof state before:
A✝ B✝ : Set ℕ
n : ℕ
A B : Set ℕ
⊢ min 1 (schnirelmannDensity A + schnirelmannDensity B) ≤ schnirelmannDensity (A + B)
Tactic:
sorry
Proof state after:
no goals
Theorem: Sublattice.prod_top
Proof state before:
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : Lattice α
inst✝¹ : Lattice β
inst✝ : Lattice γ
L✝ M : Sublattice α
f : LatticeHom α β
s t : Set α
a✝ : α
L : Sublattice α
a : α × β
⊢ a ∈ L.prod ⊤ ↔ a ∈ comap (LatticeHom.fst α β) L
Tactic:
simp [mem_prod, LatticeHom.coe_fst]
Proof state after:
no goals
Theorem: Sublattice.top_prod
Proof state before:
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : Lattice α
inst✝¹ : Lattice β
inst✝ : Lattice γ
L✝ M : Sublattice α
f : LatticeHom α β
s t : Set α
a✝ : α
L : Sublattice β
a : α × β
⊢ a ∈ ⊤.prod L ↔ a ∈ comap (LatticeHom.snd α β) L
Tactic:
simp [mem_prod, LatticeHom.coe_snd]
Proof state after:
no goals
Theorem: Sublattice.le_prod_iff
Proof state before:
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : Lattice α
inst✝¹ : Lattice β
inst✝ : Lattice γ
L M✝ : Sublattice α
f : LatticeHom α β
s t : Set α
a : α
M : Sublattice β
N : Sublattice (α × β)
⊢ N ≤ L.prod M ↔ N ≤ comap (LatticeHom.fst α β) L ∧ N ≤ comap (LatticeHom.snd α β) M
Tactic:
simp [SetLike.le_def, forall_and]
Proof state after:
no goals
Theorem: Sublattice.prod_eq_bot
Proof state before:
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : Lattice α
inst✝¹ : Lattice β
inst✝ : Lattice γ
L M✝ : Sublattice α
f : LatticeHom α β
s t : Set α
a : α
M : Sublattice β
⊢ L.prod M = ⊥ ↔ L = ⊥ ∨ M = ⊥
Tactic:
simpa only [← coe_inj] using Set.prod_eq_empty_iff
Proof state after:
no goals
Theorem: Sublattice.prod_eq_top
Proof state before:
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁴ : Lattice α
inst✝³ : Lattice β
inst✝² : Lattice γ
L M✝ : Sublattice α
f : LatticeHom α β
s t : Set α
a : α
inst✝¹ : Nonempty α
inst✝ : Nonempty β
M : Sublattice β
⊢ L.prod M = ⊤ ↔ L = ⊤ ∧ M = ⊤
Tactic:
simpa only [← coe_inj] using Set.prod_eq_univ
Proof state after:
no goals
Theorem: Sublattice.pi_empty
Proof state before:
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : Lattice α
inst✝² : Lattice β
inst✝¹ : Lattice γ
L✝ M : Sublattice α
f : LatticeHom α β
s t : Set α
a✝ : α
κ : Type u_5
π : κ → Type u_6
inst✝ : (i : κ) → Lattice (π i)
L : (i : κ) → Sublattice (π i)
a : (i : κ) → π i
⊢ a ∈ pi ∅ L ↔ a ∈ ⊤
Tactic:
simp [mem_pi]
Proof state after:
no goals
Theorem: Sublattice.pi_top
Proof state before:
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : Lattice α
inst✝² : Lattice β
inst✝¹ : Lattice γ
L M : Sublattice α
f : LatticeHom α β
s✝ t : Set α
a✝ : α
κ : Type u_5
π : κ → Type u_6
inst✝ : (i : κ) → Lattice (π i)
s : Set κ
a : (i : κ) → π i
⊢ (a ∈ pi s fun i => ⊤) ↔ a ∈ ⊤
Tactic:
simp [mem_pi]
Proof state after:
no goals
Theorem: Sublattice.pi_bot
Proof state before:
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁴ : Lattice α
inst✝³ : Lattice β
inst✝² : Lattice γ
L M : Sublattice α
f : LatticeHom α β
s t : Set α
a✝ : α
κ : Type u_5
π : κ → Type u_6
inst✝¹ : (i : κ) → Lattice (π i)
inst✝ : Nonempty κ
a : (i : κ) → π i
⊢ (a ∈ pi univ fun i => ⊥) ↔ a ∈ ⊥
Tactic:
simp [mem_pi]
Proof state after:
no goals
Theorem: Sublattice.le_pi
Proof state before:
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : Lattice α
inst✝² : Lattice β
inst✝¹ : Lattice γ
L✝ M✝ : Sublattice α
f : LatticeHom α β
s✝ t : Set α
a : α
κ : Type u_5
π : κ → Type u_6
inst✝ : (i : κ) → Lattice (π i)
s : Set κ
L : (i : κ) → Sublattice (π i)
M : Sublattice ((i : κ) → π i)
⊢ M ≤ pi s L ↔ ∀ i ∈ s, M ≤ comap (Pi.evalLatticeHom π i) (L i)
Tactic:
simp [SetLike.le_def]
Proof state after:
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : Lattice α
inst✝² : Lattice β
inst✝¹ : Lattice γ
L✝ M✝ : Sublattice α
f : LatticeHom α β
s✝ t : Set α
a : α
κ : Type u_5
π : κ → Type u_6
inst✝ : (i : κ) → Lattice (π i)
s : Set κ
L : (i : κ) → Sublattice (π i)
M : Sublattice ((i : κ) → π i)
⊢ (∀ ⦃x : (i : κ) → π i⦄, x ∈ M → ∀ i ∈ s, x i ∈ L i) ↔ ∀ i ∈ s, ∀ ⦃x : (i : κ) → π i⦄, x ∈ M → x i ∈ L i