simp only [deriv.ofReal_comp']
case calc_2.fderivCont
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
s : ℂ
hs : s ≠ 0
g : {s : ℂ} → ℝ → ℂ := fun {s} x => ↑x ^ s / s
gderiv : ∀ {s : ℂ}, s ≠ 0 → ∀ {x : ℝ}, x ∈ Ioi 0 → deriv g x = ↑x ^ (s - 1)
⊢ ContinuousOn (deriv fun x => ↑(Ψ x)) (Ioi 0)
case calc_2.fderivCont
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
s : ℂ
hs : s ≠ 0
g : {s : ℂ} → ℝ → ℂ := fun {s} x => ↑x ^ s / s
gderiv : ∀ {s : ℂ}, s ≠ 0 → ∀ {x : ℝ}, x ∈ Ioi 0 → deriv g x = ↑x ^ (s - 1)
⊢ ContinuousOn (fun x => ↑(deriv (fun x => Ψ x) x)) (Ioi 0)