-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst_2 : NormedAddCommGroup V
inst_3 : NormedSpace ℝ V
inst_4 : NormedAddCommGroup W
inst_5 : NormedSpace ℝ W
L : ContinuousLinearMap.{0, 0, u_2, u_3} (RingHom.id ℝ) V (W →L[ℝ] ℝ)
f : V → E
K : ℕ∞ω
C : ℝ
hf : ContDiff ℝ K f
n k : ℕ
hk : (↑k : ℕ∞ω) ≤ K
v : V
hv :
  ∀ i ≤ k,
    ∀ j ≤ n,
      ‖v‖ ^ j *
          Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin i) ↦ V) E)
            (iteratedFDeriv ℝ i f v) ≤
        C
T : ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ W →L[ℝ] ℝ) (ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ W) ℝ) :=
  compContinuousLinearMapLRight (E := fun (i : Fin n) ↦ W) (E₁ := fun (i : Fin n) ↦ ℝ)
    (ContinuousMultilinearMap.mkPiAlgebra ℝ (Fin n) ℝ)
I₁ :
  ∀ (m : ℕ),
    Norm.norm (E :=
        ContinuousMultilinearMap ℝ (fun (i : Fin m) ↦ (i : Fin n) → W →L[ℝ] ℝ)
          (ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ W) ℝ))
        (iteratedFDeriv ℝ m (⇑T : (a : (i : Fin n) → W →L[ℝ] ℝ) → ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ W) ℝ)
          fun (x : Fin n) ↦ (L : (a : V) → W →L[ℝ] ℝ) v) ≤
      HMul.hMul (α := ℝ) (↑(n.descFactorial m) : ℝ) 1 * (‖L‖ * ‖v‖) ^ (n - m)
I₂ :
  ∀ (m : ℕ),
    Norm.norm (E :=
        ContinuousMultilinearMap.{0, 0, u_2, u_3} ℝ (fun (i : Fin m) ↦ V)
          (ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ W) ℝ))
        (iteratedFDeriv ℝ m
          (Function.comp (β := (i : Fin n) → W →L[ℝ] ℝ)
            (⇑T : (a : (i : Fin n) → W →L[ℝ] ℝ) → ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ W) ℝ)
            (⇑(ContinuousLinearMap.pi (φ := fun (x : Fin n) ↦ W →L[ℝ] ℝ) fun (x : Fin n) ↦ L) :
              (a : V) → (i : Fin n) → W →L[ℝ] ℝ))
          v) ≤
      HMul.hMul (α := ℝ) (↑(n.descFactorial m) : ℝ) 1 * (‖L‖ * ‖v‖) ^ (n - m) * ‖L‖ ^ m
I₃ :
  ∀ (m : ℕ),
    Norm.norm (E :=
        ContinuousMultilinearMap.{0, 0, u_2, u_3} ℝ (fun (i : Fin m) ↦ V)
          (ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ W) ℝ))
        (iteratedFDeriv ℝ m
          (Function.comp (β := (i : Fin n) → W →L[ℝ] ℝ)
            (⇑T : (a : (i : Fin n) → W →L[ℝ] ℝ) → ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ W) ℝ)
            (⇑(ContinuousLinearMap.pi (φ := fun (x : Fin n) ↦ W →L[ℝ] ℝ) fun (x : Fin n) ↦ L) :
              (a : V) → (i : Fin n) → W →L[ℝ] ℝ))
          v) ≤
      (↑(n.descFactorial m) : ℝ) * ‖L‖ ^ n * ‖v‖ ^ (n - m)
A :
  ContDiff.{0, u_2, u_3} ℝ (F := ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ W) ℝ) K fun (y : V) ↦
    (T : (a : (i : Fin n) → W →L[ℝ] ℝ) → ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ W) ℝ) fun (x : Fin n) ↦
      (L : (a : V) → W →L[ℝ] ℝ) y
simp :
  (2 * π) ^ n *
      Norm.norm (E :=
        ContinuousMultilinearMap ℝ (fun (i : Fin k) ↦ V)
          (ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin n) ↦ W) E))
        (iteratedFDeriv ℝ k
            (fun (x : V) ↦
              smulRight (M₁ := fun (x : Fin n) ↦ W)
                ((T : (a : (i : Fin n) → W →L[ℝ] ℝ) → ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ W) ℝ)
                  fun (x_1 : Fin n) ↦ (L : (a : V) → W →L[ℝ] ℝ) x)
                (f x))
            v :
          ContinuousMultilinearMap ℝ (fun (i : Fin k) ↦ V)
            (ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (x : Fin n) ↦ W) E)) ≤
    (2 * π) ^ n * ((HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2) ^ k * (‖L‖ ^ n * C))
⊢ ‖(-(2 * (↑π : ℂ) * I)) ^ n‖ *
      Norm.norm (E :=
        ContinuousMultilinearMap ℝ (fun (i : Fin k) ↦ V)
          (ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin n) ↦ W) E))
        (iteratedFDeriv ℝ k
            (fun (x : V) ↦
              ((((smulRightL ℝ (fun (x : Fin n) ↦ W) E :
                          ContinuousMultilinearMap ℝ (fun (x : Fin n) ↦ W) ℝ →L[ℝ]
                            E →L[ℝ] ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (x : Fin n) ↦ W) E) :
                        (a : ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ W) ℝ) →
                          E →L[ℝ] ContinuousMultilinearMap ℝ (fun (x : Fin n) ↦ W) E)
                      ((T : (a : (i : Fin n) → W →L[ℝ] ℝ) → ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ W) ℝ)
                            fun (x_1 : Fin n) ↦ (L : (a : V) → W →L[ℝ] ℝ) x,
                          f x).1 :
                    E →L[ℝ] ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (x : Fin n) ↦ W) E) :
                  (a : E) → ContinuousMultilinearMap ℝ (fun (x : Fin n) ↦ W) E)
                (((T : (a : (i : Fin n) → W →L[ℝ] ℝ) → ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ W) ℝ)
                        fun (x_1 : Fin n) ↦ (L : (a : V) → W →L[ℝ] ℝ) x,
                      f x) :
                    Prod.{u_3, u_1} (ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ W) ℝ) E).2)
            v :
          ContinuousMultilinearMap ℝ (fun (i : Fin k) ↦ V)
            (ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (x : Fin n) ↦ W) E)) ≤
    (2 * π) ^ n * (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 2) ^ k * ‖L‖ ^ n * C

Tactic:
simp only [mul_assoc, norm_pow, norm_neg, Complex.norm_mul, Complex.norm_ofNat, norm_real,
    Real.norm_eq_abs, abs_of_nonneg pi_nonneg, norm_I, mul_one, smulRightL_apply, ge_iff_le]

Premises used: Real.pi_nonneg, norm_pow, ge_iff_le, mul_assoc, Complex.norm_real, Complex.norm_ofNat, norm_neg, Complex.norm_I, abs_of_nonneg, ContinuousMultilinearMap.smulRightL_apply, mul_one, Complex.norm_mul, Real.norm_eq_abs