Theorem: Complex.iteratedDeriv_exp_real_smul_I (ForML/Trigonometric.lean)

State before:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAlgebra 𝕜 ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
x : ℝ
⊢ iteratedDeriv n (fun x => cexp (x • I)) x = I ^ n * cexp (x • I)
Tactic:
induction n with
| zero => simp
| succ n hi =>
  rw [iteratedDeriv_succ', pow_succ]
  conv => lhs; arg 2; intro x; rw [deriv_exp_real_smul_I]
  rw [iteratedDeriv_const_mul_apply I contDiff_exp_real_smul_I]
  rw [hi, mul_assoc]
State after:
no goals

State before:
case zero
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAlgebra 𝕜 ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : ℝ
⊢ iteratedDeriv Nat.zero (fun x => cexp (x • I)) x = I ^ Nat.zero * cexp (x • I)
Tactic:
simp
State after:
no goals

State before:
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 (Nat.succ n) (fun x => cexp (x • I)) x = I ^ Nat.succ n * cexp (x • I)
Tactic:
rw [iteratedDeriv_succ', pow_succ]
State after:
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)

State before:
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)
Tactic:
conv => lhs; arg 2; intro x; rw [deriv_exp_real_smul_I]
State after:
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)

State before:
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)
Tactic:
rw [iteratedDeriv_const_mul_apply I contDiff_exp_real_smul_I]
State after:
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)
⊢ I * iteratedDeriv n (fun x => cexp (x • I)) x = I * I ^ n * cexp (x • I)

State before:
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)
⊢ I * iteratedDeriv n (fun x => cexp (x • I)) x = I * I ^ n * cexp (x • I)
Tactic:
rw [hi, mul_assoc]
State after:
no goals