conv => lhs; arg 2; intro x; rw [deriv_exp_real_smul_I]
case succ
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAlgebra 𝕜 ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : ℝ
n : ℕ
hi : iteratedDeriv n (fun x => cexp (x • I)) x = I ^ n * cexp (x • I)
⊢ iteratedDeriv n (deriv fun x => cexp (x • I)) x = I * I ^ n * cexp (x • I)
case succ
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAlgebra 𝕜 ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : ℝ
n : ℕ
hi : iteratedDeriv n (fun x => cexp (x • I)) x = I ^ n * cexp (x • I)
⊢ iteratedDeriv n (fun x => I * cexp (x • I)) x = I * I ^ n * cexp (x • I)