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