exact fun x hx ↦ ofReal_mem_slitPlane.mpr <| xpos_of_uIcc ha hx
s : ℂ
s_ne_zero : s ≠ 0
a b : ℕ
ha : a ∈ Ioo 0 b
this : EqOn (fun x => deriv (fun t => 1 / ↑t ^ s) x) (fun t => -s * ↑t ^ (-(s + 1))) [[↑a, ↑b]]
⊢ ∀ a_1 ∈ [[↑a, ↑b]], ↑a_1 ∈ slitPlane
no goals