rw [hc3] at hc2
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)
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)