have : Finset.Ico 1 N ⊆ Finset.Ico 0 N := by
  intro x hx
  simp only [Finset.mem_Ico, Nat.Ico_zero_eq_range, Finset.mem_range] at hx ⊢
  exact hx.2
N : ℕ
Npos : 0 < N
⊢ ∑ x ∈ Finset.Ico 0 N, (↑x)⁻¹ = ∑ x ∈ Finset.Ico 1 N, (↑x)⁻¹
N : ℕ
Npos : 0 < N
this : Finset.Ico 1 N ⊆ Finset.Ico 0 N
⊢ ∑ x ∈ Finset.Ico 0 N, (↑x)⁻¹ = ∑ x ∈ Finset.Ico 1 N, (↑x)⁻¹