congr
case h.e'_2.h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
s : ℂ
h : s.re > 0
a✝¹ : ℝ
a✝ : a✝¹ ∈ Ioi 0
⊢ (↑a✝¹ ^ (s - 1) * if 0 < a✝¹ ∧ a✝¹ ≤ 1 then 1 else 0) = ↑a✝¹ ^ (s - 1) * (Ioc 0 1).indicator (fun x => 1) a✝¹
no goals