have : Finset.Ico 0 N \ Finset.Ico 1 N = Finset.range 1 := by
  ext a
  simp only [Nat.Ico_zero_eq_range, Finset.mem_sdiff, Finset.mem_range, Finset.mem_Ico, not_and,
    not_lt, Finset.range_one, Finset.mem_singleton]
  exact ⟨fun _ ↦ by omega, fun ha ↦ ⟨by simp [ha, Npos], by omega⟩⟩
N : ℕ
Npos : 0 < N
this : Finset.Ico 1 N ⊆ Finset.Ico 0 N
⊢ ∑ x ∈ Finset.Ico 0 N \ Finset.Ico 1 N, (↑x)⁻¹ + ∑ x ∈ Finset.Ico 1 N, (↑x)⁻¹ = ∑ x ∈ Finset.Ico 1 N, (↑x)⁻¹
N : ℕ
Npos : 0 < N
this✝ : Finset.Ico 1 N ⊆ Finset.Ico 0 N
this : Finset.Ico 0 N \ Finset.Ico 1 N = Finset.range 1
⊢ ∑ x ∈ Finset.Ico 0 N \ Finset.Ico 1 N, (↑x)⁻¹ + ∑ x ∈ Finset.Ico 1 N, (↑x)⁻¹ = ∑ x ∈ Finset.Ico 1 N, (↑x)⁻¹