apply Finset.sum_nbij (i := (fun (x : ℕ) ↦ (x : ℤ))) ?_ ?_ ?_ fun _ _ ↦ rfl
f : ℤ → ℂ
m n : ℕ
⊢ ∑ x ∈ Finset.Ioc m n, f ↑x = ∑ x ∈ Finset.Ioc ↑m ↑n, f x
f : ℤ → ℂ
m n : ℕ
⊢ ∀ a ∈ Finset.Ioc m n, (fun x => ↑x) a ∈ Finset.Ioc ↑m ↑n

f : ℤ → ℂ
m n : ℕ
⊢ InjOn (fun x => ↑x) ↑(Finset.Ioc m n)

f : ℤ → ℂ
m n : ℕ
⊢ SurjOn (fun x => ↑x) ↑(Finset.Ioc m n) ↑(Finset.Ioc ↑m ↑n)