-- Mathlib/Analysis/Fourier/FourierTransformDeriv.lean
lemma _root_.ContDiff.fourierPowSMulRight
    {f : V → E} {k : WithTop ℕ∞} (hf : ContDiff ℝ k f) (n : ℕ) :
    ContDiff ℝ k (fun v ↦ fourierPowSMulRight L f v n)

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
k : WithTop ℕ∞
hf : ContDiff ℝ k f
n : ℕ
⊢ ContDiff ℝ k fun v => VectorFourier.fourierPowSMulRight L f v n

Tactic:
simp_rw [fourierPowSMulRight_eq_comp]

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
k : WithTop ℕ∞
hf : ContDiff ℝ k f
n : ℕ
⊢ ContDiff ℝ k fun v =>
    (-(2 * ↑π * I)) ^ n •
      ((smulRightL ℝ (fun x => W) E)
          ((ContinuousMultilinearMap.mkPiAlgebra ℝ (Fin n) ℝ).compContinuousLinearMapLRight fun x => L v))
        (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
k : WithTop ℕ∞
hf : ContDiff ℝ k f
n : ℕ
⊢ ContDiff ℝ k fun x x_1 => L x

Tactic:
exact contDiff_pi.2 (fun _ ↦ L.contDiff)

Result:
no goals

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
k : WithTop ℕ∞
hf : ContDiff ℝ k f
n : ℕ
⊢ ContDiff ℝ k fun x => (ContinuousMultilinearMap.mkPiAlgebra ℝ (Fin n) ℝ).compContinuousLinearMapLRight fun x_1 => L x

Tactic:
apply (ContinuousMultilinearMap.contDiff _).comp

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
k : WithTop ℕ∞
hf : ContDiff ℝ k f
n : ℕ
⊢ ContDiff ℝ k fun x x_1 => L x

Proof state:
case hf
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
k : WithTop ℕ∞
hf : ContDiff ℝ k f
n : ℕ
⊢ ContDiff ℝ k fun y =>
    ((smulRightL ℝ (fun x => W) E)
        ((ContinuousMultilinearMap.mkPiAlgebra ℝ (Fin n) ℝ).compContinuousLinearMapLRight fun x => L y))
      (f y)

Tactic:
apply (smulRightL ℝ (fun (_ : Fin n) ↦ W) E).isBoundedBilinearMap.contDiff.comp₂ _ hf

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
k : WithTop ℕ∞
hf : ContDiff ℝ k f
n : ℕ
⊢ ContDiff ℝ k fun x => (ContinuousMultilinearMap.mkPiAlgebra ℝ (Fin n) ℝ).compContinuousLinearMapLRight fun x_1 => L x

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
k : WithTop ℕ∞
hf : ContDiff ℝ k f
n : ℕ
⊢ ContDiff ℝ k fun v =>
    (-(2 * ↑π * I)) ^ n •
      ((smulRightL ℝ (fun x => W) E)
          ((ContinuousMultilinearMap.mkPiAlgebra ℝ (Fin n) ℝ).compContinuousLinearMapLRight fun x => L v))
        (f v)

Tactic:
apply ContDiff.const_smul

Result:
case hf
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
k : WithTop ℕ∞
hf : ContDiff ℝ k f
n : ℕ
⊢ ContDiff ℝ k fun y =>
    ((smulRightL ℝ (fun x => W) E)
        ((ContinuousMultilinearMap.mkPiAlgebra ℝ (Fin n) ℝ).compContinuousLinearMapLRight fun x => L y))
      (f y)