-- Mathlib/Analysis/Fourier/FourierTransformDeriv.lean
lemma hasFDerivAt_fourierChar_neg_bilinear_right (v : V) (w : W) :
    HasFDerivAt (fun w ↦ (𝐞 (-L v w) : ℂ))
      ((-2 * π * I * 𝐞 (-L v w)) • (ofRealCLM ∘L (L v))) w

Proof state:
V : Type u_1
W : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : NormedAddCommGroup W
inst✝ : NormedSpace ℝ W
L : V →L[ℝ] W →L[ℝ] ℝ
v : V
w : W
⊢ HasFDerivAt (fun w => ↑(𝐞 (-(L v) w))) ((-2 * ↑π * I * ↑(𝐞 (-(L v) w))) • ofRealCLM.comp (L v)) w

Tactic:
have ha : HasFDerivAt (fun w' : W ↦ L v w') (L v) w := ContinuousLinearMap.hasFDerivAt (L v)

Result:
V : Type u_1
W : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : NormedAddCommGroup W
inst✝ : NormedSpace ℝ W
L : V →L[ℝ] W →L[ℝ] ℝ
v : V
w : W
ha : HasFDerivAt (fun w' => (L v) w') (L v) w
⊢ HasFDerivAt (fun w => ↑(𝐞 (-(L v) w))) ((-2 * ↑π * I * ↑(𝐞 (-(L v) w))) • ofRealCLM.comp (L v)) w

Proof state:
case h.e'_12.h
V : Type u_1
W : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : NormedAddCommGroup W
inst✝ : NormedSpace ℝ W
L : V →L[ℝ] W →L[ℝ] ℝ
v : V
w : W
ha : HasFDerivAt (fun w' => (L v) w') (L v) w
y : W
⊢ ((-2 * ↑π * I * ↑(𝐞 (-(L v) w))) • ofRealCLM.comp (L v)) y =
    ((ContinuousLinearMap.smulRight 1 (2 * ↑π * I * ↑(𝐞 (-(L v) w)))).comp (-L v)) y

Tactic:
simp only [neg_mul, ContinuousLinearMap.coe_smul', ContinuousLinearMap.coe_comp', Pi.smul_apply,
  Function.comp_apply, ofRealCLM_apply, smul_eq_mul, ContinuousLinearMap.comp_neg,
  ContinuousLinearMap.neg_apply, ContinuousLinearMap.smulRight_apply,
  ContinuousLinearMap.one_apply, real_smul, neg_inj]

Result:
case h.e'_12.h
V : Type u_1
W : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : NormedAddCommGroup W
inst✝ : NormedSpace ℝ W
L : V →L[ℝ] W →L[ℝ] ℝ
v : V
w : W
ha : HasFDerivAt (fun w' => (L v) w') (L v) w
y : W
⊢ 2 * ↑π * I * ↑(𝐞 (-(L v) w)) * ↑((L v) y) = ↑((L v) y) * (2 * ↑π * I * ↑(𝐞 (-(L v) w)))

Proof state:
case h.e'_12.h
V : Type u_1
W : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : NormedAddCommGroup W
inst✝ : NormedSpace ℝ W
L : V →L[ℝ] W →L[ℝ] ℝ
v : V
w : W
ha : HasFDerivAt (fun w' => (L v) w') (L v) w
y : W
⊢ 2 * ↑π * I * ↑(𝐞 (-(L v) w)) * ↑((L v) y) = ↑((L v) y) * (2 * ↑π * I * ↑(𝐞 (-(L v) w)))

Tactic:
ring

Result:
no goals

Proof state:
V : Type u_1
W : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : NormedAddCommGroup W
inst✝ : NormedSpace ℝ W
L : V →L[ℝ] W →L[ℝ] ℝ
v : V
w : W
ha : HasFDerivAt (fun w' => (L v) w') (L v) w
⊢ HasFDerivAt (fun w => ↑(𝐞 (-(L v) w))) ((-2 * ↑π * I * ↑(𝐞 (-(L v) w))) • ofRealCLM.comp (L v)) w

Tactic:
convert (hasDerivAt_fourierChar (-L v w)).hasFDerivAt.comp w ha.neg using 1

Result:
case h.e'_12
V : Type u_1
W : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : NormedAddCommGroup W
inst✝ : NormedSpace ℝ W
L : V →L[ℝ] W →L[ℝ] ℝ
v : V
w : W
ha : HasFDerivAt (fun w' => (L v) w') (L v) w
⊢ (-2 * ↑π * I * ↑(𝐞 (-(L v) w))) • ofRealCLM.comp (L v) =
    (ContinuousLinearMap.smulRight 1 (2 * ↑π * I * ↑(𝐞 (-(L v) w)))).comp (-L v)

Proof state:
case h.e'_12
V : Type u_1
W : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : NormedAddCommGroup W
inst✝ : NormedSpace ℝ W
L : V →L[ℝ] W →L[ℝ] ℝ
v : V
w : W
ha : HasFDerivAt (fun w' => (L v) w') (L v) w
⊢ (-2 * ↑π * I * ↑(𝐞 (-(L v) w))) • ofRealCLM.comp (L v) =
    (ContinuousLinearMap.smulRight 1 (2 * ↑π * I * ↑(𝐞 (-(L v) w)))).comp (-L v)

Tactic:
ext y

Result:
case h.e'_12.h
V : Type u_1
W : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : NormedAddCommGroup W
inst✝ : NormedSpace ℝ W
L : V →L[ℝ] W →L[ℝ] ℝ
v : V
w : W
ha : HasFDerivAt (fun w' => (L v) w') (L v) w
y : W
⊢ ((-2 * ↑π * I * ↑(𝐞 (-(L v) w))) • ofRealCLM.comp (L v)) y =
    ((ContinuousLinearMap.smulRight 1 (2 * ↑π * I * ↑(𝐞 (-(L v) w)))).comp (-L v)) y