convert (hasMellin_one_Ioc h).right using 1
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
s : ℂ
h : s.re > 0
⊢ 𝓜 (fun x => if 0 < x ∧ x ≤ 1 then 1 else 0) s = 1 / s
case h.e'_2
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
s : ℂ
h : s.re > 0
⊢ 𝓜 (fun x => if 0 < x ∧ x ≤ 1 then 1 else 0) s = mellin ((Ioc 0 1).indicator fun x => 1) s