swap
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAlgebra 𝕜 ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x dx : ℝ
⊢ cexp ((2 * π * x) • I) * (ContinuousLinearMap.smulRight (fderiv ℝ (fun x => 2 * π * x) x) I) dx =
    (2 * π * dx) • (I * cexp ((2 * π * x) • I))

case hc
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAlgebra 𝕜 ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x dx : ℝ
⊢ DifferentiableAt ℝ (fun x => 2 * π * x) x
case hc
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAlgebra 𝕜 ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x dx : ℝ
⊢ DifferentiableAt ℝ (fun x => 2 * π * x) x

𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAlgebra 𝕜 ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x dx : ℝ
⊢ cexp ((2 * π * x) • I) * (ContinuousLinearMap.smulRight (fderiv ℝ (fun x => 2 * π * x) x) I) dx =
    (2 * π * dx) • (I * cexp ((2 * π * x) • I))