rw [next_elm] at hx3
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
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