Theorem: schnirelmannDensity_for_two (LeanCamCombi/Mathlib/Combinatorics/Schnirelmann.lean)

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
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)

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
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)

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
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)

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
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)

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)
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)

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
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)

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]
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 - β)

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
State after:
no goals

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]
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 + (γ - (α + β - α * β))

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]
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 + (γ - (α + β - α * β))

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]
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)
⊢ α + β - α * β ≤ γ

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]
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)
⊢ α + β + -(α * β) ≤ γ

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
State after:
no goals

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]
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)

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
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

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
State after:
no goals

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
State after:
no goals