simp only [Finset.coe_Ioc, mem_image, mem_Ioc] at hx ⊢
f : ℤ → ℂ
m n : ℕ
x : ℤ
hx : x ∈ ↑(Finset.Ioc ↑m ↑n)
⊢ x ∈ (fun x => ↑x) '' ↑(Finset.Ioc m n)
f : ℤ → ℂ
m n : ℕ
x : ℤ
hx : ↑m < x ∧ x ≤ ↑n
⊢ ∃ x_1, (m < x_1 ∧ x_1 ≤ n) ∧ ↑x_1 = x