-- Mathlib/Analysis/Fourier/FourierTransformDeriv.lean
/-- The `w`-derivative of the Fourier transform integrand. -/
lemma hasFDerivAt_fourierChar_smul (v : V) (w : W) :
    HasFDerivAt (fun w' ↦ 𝐞 (-L v w') • f v) (𝐞 (-L v w) • fourierSMulRight L f v) w

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

Tactic:
rw [ContinuousLinearMap.comp_apply, ContinuousLinearMap.neg_apply,
  ContinuousLinearMap.smulRight_apply, ContinuousLinearMap.one_apply, ← smul_assoc, smul_comm,
  ← smul_assoc, real_smul, real_smul, Submonoid.smul_def, smul_eq_mul]

Result:
case h.e'_12.h.h.h
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : NormedAddCommGroup W
inst✝ : NormedSpace ℝ W
L : V →L[ℝ] W →L[ℝ] ℝ
f : V → E
v : V
w : W
ha : HasFDerivAt (fun w' => (L v) w') (L v) w
e_8✝ : SeminormedAddCommGroup.toAddCommGroup = NormedAddCommGroup.toAddCommGroup
he✝ : NormedSpace.toModule = NormedSpace.toModule
w' : W
⊢ (↑((L v) w') * (↑(𝐞 (-(L v) w)) * -(2 * ↑π * I))) • f v = (↑(-(L v) w') * (2 * ↑π * I * ↑(𝐞 (-(L v) w)))) • f v

Proof state:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : NormedAddCommGroup W
inst✝ : NormedSpace ℝ W
L : V →L[ℝ] W →L[ℝ] ℝ
f : V → E
v : V
w : W
⊢ HasFDerivAt (fun w' => 𝐞 (-(L v) w') • f v) (𝐞 (-(L v) w) • fourierSMulRight L f v) w

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

Result:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : NormedAddCommGroup W
inst✝ : NormedSpace ℝ W
L : V →L[ℝ] W →L[ℝ] ℝ
f : V → E
v : V
w : W
ha : HasFDerivAt (fun w' => (L v) w') (L v) w
⊢ HasFDerivAt (fun w' => 𝐞 (-(L v) w') • f v) (𝐞 (-(L v) w) • fourierSMulRight L f v) w

Proof state:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : NormedAddCommGroup W
inst✝ : NormedSpace ℝ W
L : V →L[ℝ] W →L[ℝ] ℝ
f : V → E
v : V
w : W
ha : HasFDerivAt (fun w' => (L v) w') (L v) w
⊢ HasFDerivAt (fun w' => 𝐞 (-(L v) w') • f v) (𝐞 (-(L v) w) • fourierSMulRight L f v) w

Tactic:
convert ((hasDerivAt_fourierChar (-L v w)).hasFDerivAt.comp w ha.neg).smul_const (f v)

Result:
case h.e'_12.h.h
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : NormedAddCommGroup W
inst✝ : NormedSpace ℝ W
L : V →L[ℝ] W →L[ℝ] ℝ
f : V → E
v : V
w : W
ha : HasFDerivAt (fun w' => (L v) w') (L v) w
e_8✝ : SeminormedAddCommGroup.toAddCommGroup = NormedAddCommGroup.toAddCommGroup
he✝ : NormedSpace.toModule = NormedSpace.toModule
⊢ 𝐞 (-(L v) w) • fourierSMulRight L f v =
    ((ContinuousLinearMap.smulRight 1 (2 * ↑π * I * ↑(𝐞 (-(L v) w)))).comp (-L v)).smulRight (f v)

Proof state:
case h.e'_12.h.h.h
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : NormedAddCommGroup W
inst✝ : NormedSpace ℝ W
L : V →L[ℝ] W →L[ℝ] ℝ
f : V → E
v : V
w : W
ha : HasFDerivAt (fun w' => (L v) w') (L v) w
e_8✝ : SeminormedAddCommGroup.toAddCommGroup = NormedAddCommGroup.toAddCommGroup
he✝ : NormedSpace.toModule = NormedSpace.toModule
w' : W
⊢ (↑((L v) w') * (↑(𝐞 (-(L v) w)) * -(2 * ↑π * I))) • f v = (-↑((L v) w') * (2 * ↑π * I * ↑(𝐞 (-(L v) w)))) • f v

Tactic:
ring_nf

Result:
no goals

Proof state:
case h.e'_12.h.h.h
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : NormedAddCommGroup W
inst✝ : NormedSpace ℝ W
L : V →L[ℝ] W →L[ℝ] ℝ
f : V → E
v : V
w : W
ha : HasFDerivAt (fun w' => (L v) w') (L v) w
e_8✝ : SeminormedAddCommGroup.toAddCommGroup = NormedAddCommGroup.toAddCommGroup
he✝ : NormedSpace.toModule = NormedSpace.toModule
w' : W
⊢ (𝐞 (-(L v) w) • fourierSMulRight L f v) w' =
    (((ContinuousLinearMap.smulRight 1 (2 * ↑π * I * ↑(𝐞 (-(L v) w)))).comp (-L v)).smulRight (f v)) w'

Tactic:
simp_rw [fourierSMulRight, ContinuousLinearMap.smul_apply, ContinuousLinearMap.smulRight_apply]

Result:
case h.e'_12.h.h.h
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : NormedAddCommGroup W
inst✝ : NormedSpace ℝ W
L : V →L[ℝ] W →L[ℝ] ℝ
f : V → E
v : V
w : W
ha : HasFDerivAt (fun w' => (L v) w') (L v) w
e_8✝ : SeminormedAddCommGroup.toAddCommGroup = NormedAddCommGroup.toAddCommGroup
he✝ : NormedSpace.toModule = NormedSpace.toModule
w' : W
⊢ 𝐞 (-(L v) w) • -(2 * ↑π * I) • (L v) w' • f v =
    ((ContinuousLinearMap.smulRight 1 (2 * ↑π * I * ↑(𝐞 (-(L v) w)))).comp (-L v)) w' • f v

Proof state:
case h.e'_12.h.h.h
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : NormedAddCommGroup W
inst✝ : NormedSpace ℝ W
L : V →L[ℝ] W →L[ℝ] ℝ
f : V → E
v : V
w : W
ha : HasFDerivAt (fun w' => (L v) w') (L v) w
e_8✝ : SeminormedAddCommGroup.toAddCommGroup = NormedAddCommGroup.toAddCommGroup
he✝ : NormedSpace.toModule = NormedSpace.toModule
w' : W
⊢ (↑((L v) w') * (↑(𝐞 (-(L v) w)) * -(2 * ↑π * I))) • f v = (↑(-(L v) w') * (2 * ↑π * I * ↑(𝐞 (-(L v) w)))) • f v

Tactic:
push_cast

Result:
case h.e'_12.h.h.h
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : NormedAddCommGroup W
inst✝ : NormedSpace ℝ W
L : V →L[ℝ] W →L[ℝ] ℝ
f : V → E
v : V
w : W
ha : HasFDerivAt (fun w' => (L v) w') (L v) w
e_8✝ : SeminormedAddCommGroup.toAddCommGroup = NormedAddCommGroup.toAddCommGroup
he✝ : NormedSpace.toModule = NormedSpace.toModule
w' : W
⊢ (↑((L v) w') * (↑(𝐞 (-(L v) w)) * -(2 * ↑π * I))) • f v = (-↑((L v) w') * (2 * ↑π * I * ↑(𝐞 (-(L v) w)))) • f v

Proof state:
case h.e'_12.h.h
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : NormedAddCommGroup W
inst✝ : NormedSpace ℝ W
L : V →L[ℝ] W →L[ℝ] ℝ
f : V → E
v : V
w : W
ha : HasFDerivAt (fun w' => (L v) w') (L v) w
e_8✝ : SeminormedAddCommGroup.toAddCommGroup = NormedAddCommGroup.toAddCommGroup
he✝ : NormedSpace.toModule = NormedSpace.toModule
⊢ 𝐞 (-(L v) w) • fourierSMulRight L f v =
    ((ContinuousLinearMap.smulRight 1 (2 * ↑π * I * ↑(𝐞 (-(L v) w)))).comp (-L v)).smulRight (f v)

Tactic:
ext w' : 1

Result:
case h.e'_12.h.h.h
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : NormedAddCommGroup W
inst✝ : NormedSpace ℝ W
L : V →L[ℝ] W →L[ℝ] ℝ
f : V → E
v : V
w : W
ha : HasFDerivAt (fun w' => (L v) w') (L v) w
e_8✝ : SeminormedAddCommGroup.toAddCommGroup = NormedAddCommGroup.toAddCommGroup
he✝ : NormedSpace.toModule = NormedSpace.toModule
w' : W
⊢ (𝐞 (-(L v) w) • fourierSMulRight L f v) w' =
    (((ContinuousLinearMap.smulRight 1 (2 * ↑π * I * ↑(𝐞 (-(L v) w)))).comp (-L v)).smulRight (f v)) w'