rw [Finset.range_eq_Ico]
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → 𝕜
ε : ℝ
N : ℕ
hε : ε ≤ 1
r1 : Finset.range N = Finset.range ⌈ε * ↑N⌉₊ ∪ Finset.Ico ⌈ε * ↑N⌉₊ N
⊢ Disjoint (Finset.range ⌈ε * ↑N⌉₊) (Finset.Ico ⌈ε * ↑N⌉₊ N)
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → 𝕜
ε : ℝ
N : ℕ
hε : ε ≤ 1
r1 : Finset.range N = Finset.range ⌈ε * ↑N⌉₊ ∪ Finset.Ico ⌈ε * ↑N⌉₊ N
⊢ Disjoint (Finset.Ico 0 ⌈ε * ↑N⌉₊) (Finset.Ico ⌈ε * ↑N⌉₊ N)