Theorem: hasDerivAt_e (PrimeNumberTheoremAnd/Fourier.lean)

State before:
u x : ℝ
⊢ HasDerivAt (⇑(e u)) (-2 * ↑π * ↑u * I * (e u) x) x
Tactic:
have l2 : HasDerivAt (fun v => -v * u) (-u) x := by simpa only [neg_mul_comm] using hasDerivAt_mul_const (-u)
State after:
u x : ℝ
l2 : HasDerivAt (fun v => -v * u) (-u) x
⊢ HasDerivAt (⇑(e u)) (-2 * ↑π * ↑u * I * (e u) x) x

State before:
u x : ℝ
l2 : HasDerivAt (fun v => -v * u) (-u) x
⊢ HasDerivAt (⇑(e u)) (-2 * ↑π * ↑u * I * (e u) x) x
Tactic:
convert (hasDerivAt_fourierChar (-x * u)).scomp x l2 using 1
State after:
case h.e'_7
u x : ℝ
l2 : HasDerivAt (fun v => -v * u) (-u) x
⊢ -2 * ↑π * ↑u * I * (e u) x = -u • (2 * ↑π * I * ↑(𝐞 (-x * u)))

State before:
case h.e'_7
u x : ℝ
l2 : HasDerivAt (fun v => -v * u) (-u) x
⊢ -2 * ↑π * ↑u * I * (e u) x = -u • (2 * ↑π * I * ↑(𝐞 (-x * u)))
Tactic:
simp
State after:
case h.e'_7
u x : ℝ
l2 : HasDerivAt (fun v => -v * u) (-u) x
⊢ 2 * ↑π * ↑u * I * ↑(𝐞 (-(x * u))) = ↑u * (2 * ↑π * I * ↑(𝐞 (-(x * u))))

State before:
case h.e'_7
u x : ℝ
l2 : HasDerivAt (fun v => -v * u) (-u) x
⊢ 2 * ↑π * ↑u * I * ↑(𝐞 (-(x * u))) = ↑u * (2 * ↑π * I * ↑(𝐞 (-(x * u))))
Tactic:
ring
State after:
no goals

State before:
u x : ℝ
⊢ HasDerivAt (fun v => -v * u) (-u) x
Tactic:
simpa only [neg_mul_comm] using hasDerivAt_mul_const (-u)
State after:
no goals