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

State before:
A✝ B✝ : Set ℕ
n : ℕ
A B : Set ℕ
hA : 0 ∈ A
hB : 0 ∈ B
⊢ schnirelmannDensity A + schnirelmannDensity B - schnirelmannDensity A * schnirelmannDensity B ≤
    schnirelmannDensity (A + B)
Tactic:
set α := schnirelmannDensity A with halpha
State after:
A✝ B✝ : Set ℕ
n : ℕ
A B : Set ℕ
hA : 0 ∈ A
hB : 0 ∈ B
α : ℝ := schnirelmannDensity A
halpha : α = schnirelmannDensity A
⊢ α + schnirelmannDensity B - α * 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 - α * schnirelmannDensity B ≤ schnirelmannDensity (A + B)
Tactic:
set β := schnirelmannDensity B with hbeta
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)

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)
Tactic:
have dum : α * (1 - β) + β = α + β - α * β := by ring
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 - β) + β = α + β - α * β
⊢ α + β - α * β ≤ 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
dum : α * (1 - β) + β = α + β - α * β
⊢ α + β - α * β ≤ schnirelmannDensity (A + B)
Tactic:
rw [← dum]
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 - β) + β = α + β - α * β
⊢ α * (1 - β) + β ≤ 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
dum : α * (1 - β) + β = α + β - α * β
⊢ ∀ (n : ℕ), (α * (1 - β) + β) * ↑n ≤ ↑(countelements (A + B) n)
Tactic:
rintro n
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 : ℕ
⊢ (α * (1 - β) + β) * ↑n ≤ ↑(countelements (A + B) n)

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 : ℕ
⊢ (α * (1 - β) + β) * ↑n ≤ ↑(countelements (A + B) n)
Tactic:
obtain rfl | n1 := n.eq_zero_or_pos
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 - β) + β = α + β - α * β
⊢ (α * (1 - β) + β) * ↑0 ≤ ↑(countelements (A + B) 0)

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
⊢ (α * (1 - β) + β) * ↑n ≤ ↑(countelements (A + B) n)

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 - β) + β = α + β - α * β
Tactic:
ring
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
dum : α * (1 - β) + β = α + β - α * β
main : ∀ (n : ℕ), (α * (1 - β) + β) * ↑n ≤ ↑(countelements (A + B) n)
⊢ α * (1 - β) + β ≤ schnirelmannDensity (A + B)
Tactic:
rw [schnirelmannDensity]
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 - β) + β = α + β - α * β
main : ∀ (n : ℕ), (α * (1 - β) + β) * ↑n ≤ ↑(countelements (A + B) n)
⊢ α * (1 - β) + β ≤ ⨅ n, ↑(filter (fun x => x ∈ A + B) (Ioc 0 ↑n)).card / ↑↑n

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 - β) + β = α + β - α * β
main : ∀ (n : ℕ), (α * (1 - β) + β) * ↑n ≤ ↑(countelements (A + B) n)
⊢ α * (1 - β) + β ≤ ⨅ n, ↑(filter (fun x => x ∈ A + B) (Ioc 0 ↑n)).card / ↑↑n
Tactic:
have : Nonempty {n // n ≠ 0} := by
  use 1
  trivial
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 - β) + β = α + β - α * β
main : ∀ (n : ℕ), (α * (1 - β) + β) * ↑n ≤ ↑(countelements (A + B) n)
this : Nonempty { n // n ≠ 0 }
⊢ α * (1 - β) + β ≤ ⨅ n, ↑(filter (fun x => x ∈ A + B) (Ioc 0 ↑n)).card / ↑↑n

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 - β) + β = α + β - α * β
main : ∀ (n : ℕ), (α * (1 - β) + β) * ↑n ≤ ↑(countelements (A + B) n)
this : Nonempty { n // n ≠ 0 }
⊢ α * (1 - β) + β ≤ ⨅ n, ↑(filter (fun x => x ∈ A + B) (Ioc 0 ↑n)).card / ↑↑n
Tactic:
apply le_ciInf
State after:
case H
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 - β) + β = α + β - α * β
main : ∀ (n : ℕ), (α * (1 - β) + β) * ↑n ≤ ↑(countelements (A + B) n)
this : Nonempty { n // n ≠ 0 }
⊢ ∀ (x : { n // 0 < n }), α * (1 - β) + β ≤ ↑(filter (fun x => x ∈ A + B) (Ioc 0 ↑x)).card / ↑↑x

State before:
case H
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 - β) + β = α + β - α * β
main : ∀ (n : ℕ), (α * (1 - β) + β) * ↑n ≤ ↑(countelements (A + B) n)
this : Nonempty { n // n ≠ 0 }
⊢ ∀ (x : { n // 0 < n }), α * (1 - β) + β ≤ ↑(filter (fun x => x ∈ A + B) (Ioc 0 ↑x)).card / ↑↑x
Tactic:
intro x
State after:
case H
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 - β) + β = α + β - α * β
main : ∀ (n : ℕ), (α * (1 - β) + β) * ↑n ≤ ↑(countelements (A + B) n)
this : Nonempty { n // n ≠ 0 }
x : { n // 0 < n }
⊢ α * (1 - β) + β ≤ ↑(filter (fun x => x ∈ A + B) (Ioc 0 ↑x)).card / ↑↑x

State before:
case H
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 - β) + β = α + β - α * β
main : ∀ (n : ℕ), (α * (1 - β) + β) * ↑n ≤ ↑(countelements (A + B) n)
this : Nonempty { n // n ≠ 0 }
x : { n // 0 < n }
⊢ α * (1 - β) + β ≤ ↑(filter (fun x => x ∈ A + B) (Ioc 0 ↑x)).card / ↑↑x
Tactic:
have hx : (x : ℝ) ≠ 0 := by aesop
State after:
case H
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 - β) + β = α + β - α * β
main : ∀ (n : ℕ), (α * (1 - β) + β) * ↑n ≤ ↑(countelements (A + B) n)
this : Nonempty { n // n ≠ 0 }
x : { n // 0 < n }
hx : ↑↑x ≠ 0
⊢ α * (1 - β) + β ≤ ↑(filter (fun x => x ∈ A + B) (Ioc 0 ↑x)).card / ↑↑x

State before:
case H
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 - β) + β = α + β - α * β
main : ∀ (n : ℕ), (α * (1 - β) + β) * ↑n ≤ ↑(countelements (A + B) n)
this : Nonempty { n // n ≠ 0 }
x : { n // 0 < n }
hx : ↑↑x ≠ 0
⊢ α * (1 - β) + β ≤ ↑(filter (fun x => x ∈ A + B) (Ioc 0 ↑x)).card / ↑↑x
Tactic:
rw [le_div_iff]
State after:
case H
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 - β) + β = α + β - α * β
main : ∀ (n : ℕ), (α * (1 - β) + β) * ↑n ≤ ↑(countelements (A + B) n)
this : Nonempty { n // n ≠ 0 }
x : { n // 0 < n }
hx : ↑↑x ≠ 0
⊢ (α * (1 - β) + β) * ↑↑x ≤ ↑(filter (fun x => x ∈ A + B) (Ioc 0 ↑x)).card

case H
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 - β) + β = α + β - α * β
main : ∀ (n : ℕ), (α * (1 - β) + β) * ↑n ≤ ↑(countelements (A + B) n)
this : Nonempty { n // n ≠ 0 }
x : { n // 0 < n }
hx : ↑↑x ≠ 0
⊢ 0 < ↑↑x

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 - β) + β = α + β - α * β
main : ∀ (n : ℕ), (α * (1 - β) + β) * ↑n ≤ ↑(countelements (A + B) n)
⊢ Nonempty { n // n ≠ 0 }
Tactic:
use 1
State after:
case property
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 - β) + β = α + β - α * β
main : ∀ (n : ℕ), (α * (1 - β) + β) * ↑n ≤ ↑(countelements (A + B) n)
⊢ 1 ≠ 0

State before:
case property
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 - β) + β = α + β - α * β
main : ∀ (n : ℕ), (α * (1 - β) + β) * ↑n ≤ ↑(countelements (A + B) n)
⊢ 1 ≠ 0
Tactic:
trivial
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
dum : α * (1 - β) + β = α + β - α * β
main : ∀ (n : ℕ), (α * (1 - β) + β) * ↑n ≤ ↑(countelements (A + B) n)
this : Nonempty { n // n ≠ 0 }
x : { n // 0 < n }
⊢ ↑↑x ≠ 0
Tactic:
aesop
State after:
no goals

State before:
case H
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 - β) + β = α + β - α * β
main : ∀ (n : ℕ), (α * (1 - β) + β) * ↑n ≤ ↑(countelements (A + B) n)
this : Nonempty { n // n ≠ 0 }
x : { n // 0 < n }
hx : ↑↑x ≠ 0
⊢ (α * (1 - β) + β) * ↑↑x ≤ ↑(filter (fun x => x ∈ A + B) (Ioc 0 ↑x)).card
Tactic:
specialize main x
State after:
case H
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 - β) + β = α + β - α * β
this : Nonempty { n // n ≠ 0 }
x : { n // 0 < n }
hx : ↑↑x ≠ 0
main : (α * (1 - β) + β) * ↑↑x ≤ ↑(countelements (A + B) ↑x)
⊢ (α * (1 - β) + β) * ↑↑x ≤ ↑(filter (fun x => x ∈ A + B) (Ioc 0 ↑x)).card

State before:
case H
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 - β) + β = α + β - α * β
this : Nonempty { n // n ≠ 0 }
x : { n // 0 < n }
hx : ↑↑x ≠ 0
main : (α * (1 - β) + β) * ↑↑x ≤ ↑(countelements (A + B) ↑x)
⊢ (α * (1 - β) + β) * ↑↑x ≤ ↑(filter (fun x => x ∈ A + B) (Ioc 0 ↑x)).card
Tactic:
exact main
State after:
no goals

State before:
case H
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 - β) + β = α + β - α * β
main : ∀ (n : ℕ), (α * (1 - β) + β) * ↑n ≤ ↑(countelements (A + B) n)
this : Nonempty { n // n ≠ 0 }
x : { n // 0 < n }
hx : ↑↑x ≠ 0
⊢ 0 < ↑↑x
Tactic:
positivity
State after:
no goals

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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