awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
V : Type u_2
inst_2 : NormedAddCommGroup V
inst_3 : InnerProductSpace ℝ V
inst_4 : FiniteDimensional ℝ V
inst_5 : MeasurableSpace V
inst_6 : BorelSpace V
f : V → E
K N : ℕ∞
hf : ContDiff ℝ (↑N : ℕ∞ω) f
h'f :
  ∀ (k n : ℕ),
    (↑k : ℕ∞) ≤ K →
      (↑n : ℕ∞) ≤ N →
        @Integrable ℝ _ _ _ inst_5
          (fun (v : V) ↦
            ‖v‖ ^ k *
              Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin n) ↦ V) E)
                (iteratedFDeriv ℝ n f v))
          (volume : Measure V)
k : ℕ
hk : (↑k : ℕ∞) ≤ K
w : V
hn : (↑0 : ℕ∞) ≤ N
Z :
  Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin k) ↦ V) E) (iteratedFDeriv ℝ k (𝓕 f) w) ≤
    (2 * (π * Norm.norm.{u_2} (E := V →L⋆[ℝ] V →L[ℝ] ℝ) (innerSL ℝ))) ^ k *
      ∑ x ∈ Finset.range (k + 1), @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦ ‖v‖ ^ x * ‖f v‖
⊢ Norm.norm.{u_2} (E := V →L⋆[ℝ] V →L[ℝ] ℝ) (innerSL ℝ) ≤ 1

Tactic:
norm_innerSL_le _

Premises used: norm_innerSL_le
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
V : Type u_2
inst_2 : NormedAddCommGroup V
inst_3 : InnerProductSpace ℝ V
inst_4 : FiniteDimensional ℝ V
inst_5 : MeasurableSpace V
inst_6 : BorelSpace V
f : V → E
K N : ℕ∞
hf : ContDiff ℝ (↑N : ℕ∞ω) f
h'f :
  ∀ (k n : ℕ),
    (↑k : ℕ∞) ≤ K →
      (↑n : ℕ∞) ≤ N →
        @Integrable ℝ _ _ _ inst_5
          (fun (v : V) ↦
            ‖v‖ ^ k *
              Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin n) ↦ V) E)
                (iteratedFDeriv ℝ n f v))
          (volume : Measure V)
k : ℕ
hk : (↑k : ℕ∞) ≤ K
w : V
hn : (↑0 : ℕ∞) ≤ N
Z :
  Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin k) ↦ V) E) (iteratedFDeriv ℝ k (𝓕 f) w) ≤
    (2 * (π * Norm.norm.{u_2} (E := V →L⋆[ℝ] V →L[ℝ] ℝ) (innerSL ℝ))) ^ k *
      ∑ x ∈ Finset.range (k + 1), @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦ ‖v‖ ^ x * ‖f v‖
⊢ Norm.norm.{u_2} (E := V →L⋆[ℝ] V →L[ℝ] ℝ) (innerSL ℝ) ≤ 1

Tactic:
exact norm_innerSL_le _

Premises used: norm_innerSL_le
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
V : Type u_2
inst_2 : NormedAddCommGroup V
inst_3 : InnerProductSpace ℝ V
inst_4 : FiniteDimensional ℝ V
inst_5 : MeasurableSpace V
inst_6 : BorelSpace V
f : V → E
K N : ℕ∞
hf : ContDiff ℝ (↑N : ℕ∞ω) f
h'f :
  ∀ (k n : ℕ),
    (↑k : ℕ∞) ≤ K →
      (↑n : ℕ∞) ≤ N →
        @Integrable ℝ _ _ _ inst_5
          (fun (v : V) ↦
            ‖v‖ ^ k *
              Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin n) ↦ V) E)
                (iteratedFDeriv ℝ n f v))
          (volume : Measure V)
k n : ℕ
hk : (↑k : ℕ∞) ≤ K
hn_1 : (↑n : ℕ∞) ≤ N
hn : n ≠ 0
Z :
  Norm.norm.{u_2} (E := V) 0 ^ n *
      (Norm.norm.{u_2} (E := V) 0 ^ n *
        Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin k) ↦ V) E)
          (iteratedFDeriv ℝ k (𝓕 f) 0)) ≤
    Norm.norm.{u_2} (E := V) 0 ^ n *
      ((2 * (π * Norm.norm.{u_2} (E := V →L⋆[ℝ] V →L[ℝ] ℝ) (innerSL ℝ))) ^ k *
        ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 2) ^ n *
          ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1),
            @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
              ‖v‖ ^ p.1 *
                Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin p.2) ↦ V) E)
                  (iteratedFDeriv ℝ p.2 f v)))
inr :
  0 ≤
    (2 * π) ^ k * (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 2) ^ n *
      ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1),
        @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
          ‖v‖ ^ p.1 *
            Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin p.2) ↦ V) E)
              (iteratedFDeriv ℝ p.2 f v)
⊢ Norm.norm.{u_2} (E := V) 0 ^ n *
      Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin k) ↦ V) E)
        (iteratedFDeriv ℝ k (𝓕 f) 0) ≤
    (2 * π) ^ k * (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 2) ^ n *
      ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1),
        @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
          ‖v‖ ^ p.1 *
            Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin p.2) ↦ V) E)
              (iteratedFDeriv ℝ p.2 f v)

Tactic:
simp [hn]
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
V : Type u_2
inst_2 : NormedAddCommGroup V
inst_3 : InnerProductSpace ℝ V
inst_4 : FiniteDimensional ℝ V
inst_5 : MeasurableSpace V
inst_6 : BorelSpace V
f : V → E
K N : ℕ∞
hf : ContDiff ℝ (↑N : ℕ∞ω) f
h'f :
  ∀ (k n : ℕ),
    (↑k : ℕ∞) ≤ K →
      (↑n : ℕ∞) ≤ N →
        @Integrable ℝ _ _ _ inst_5
          (fun (v : V) ↦
            ‖v‖ ^ k *
              Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin n) ↦ V) E)
                (iteratedFDeriv ℝ n f v))
          (volume : Measure V)
k n : ℕ
hk : (↑k : ℕ∞) ≤ K
hn_1 : (↑n : ℕ∞) ≤ N
hn : n ≠ 0
Z :
  Norm.norm.{u_2} (E := V) 0 ^ n *
      (Norm.norm.{u_2} (E := V) 0 ^ n *
        Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin k) ↦ V) E)
          (iteratedFDeriv ℝ k (𝓕 f) 0)) ≤
    Norm.norm.{u_2} (E := V) 0 ^ n *
      ((2 * (π * Norm.norm.{u_2} (E := V →L⋆[ℝ] V →L[ℝ] ℝ) (innerSL ℝ))) ^ k *
        ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 2) ^ n *
          ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1),
            @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
              ‖v‖ ^ p.1 *
                Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin p.2) ↦ V) E)
                  (iteratedFDeriv ℝ p.2 f v)))
⊢ 0 ≤
    (2 * π) ^ k * (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 2) ^ n *
      ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1),
        @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
          ‖v‖ ^ p.1 *
            Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin p.2) ↦ V) E)
              (iteratedFDeriv ℝ p.2 f v)

Tactic:
positivity
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
V : Type u_2
inst_2 : NormedAddCommGroup V
inst_3 : InnerProductSpace ℝ V
inst_4 : FiniteDimensional ℝ V
inst_5 : MeasurableSpace V
inst_6 : BorelSpace V
f : V → E
K N : ℕ∞
hf : ContDiff ℝ (↑N : ℕ∞ω) f
h'f :
  ∀ (k n : ℕ),
    (↑k : ℕ∞) ≤ K →
      (↑n : ℕ∞) ≤ N →
        @Integrable ℝ _ _ _ inst_5
          (fun (v : V) ↦
            ‖v‖ ^ k *
              Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin n) ↦ V) E)
                (iteratedFDeriv ℝ n f v))
          (volume : Measure V)
k n : ℕ
hk : (↑k : ℕ∞) ≤ K
hn_1 : (↑n : ℕ∞) ≤ N
w : V
Z :
  ‖w‖ ^ n *
      (‖w‖ ^ n *
        Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin k) ↦ V) E)
          (iteratedFDeriv ℝ k (𝓕 f) w)) ≤
    ‖w‖ ^ n *
      ((2 * (π * Norm.norm.{u_2} (E := V →L⋆[ℝ] V →L[ℝ] ℝ) (innerSL ℝ))) ^ k *
        ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 2) ^ n *
          ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1),
            @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
              ‖v‖ ^ p.1 *
                Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin p.2) ↦ V) E)
                  (iteratedFDeriv ℝ p.2 f v)))
hn : n ≠ 0
hw : w ≠ 0
⊢ 0 < ‖w‖

Tactic:
simp [hw]
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
V : Type u_2
inst_2 : NormedAddCommGroup V
inst_3 : InnerProductSpace ℝ V
inst_4 : FiniteDimensional ℝ V
inst_5 : MeasurableSpace V
inst_6 : BorelSpace V
f : V → E
K N : ℕ∞
hf : ContDiff ℝ (↑N : ℕ∞ω) f
h'f :
  ∀ (k n : ℕ),
    (↑k : ℕ∞) ≤ K →
      (↑n : ℕ∞) ≤ N →
        @Integrable ℝ _ _ _ inst_5
          (fun (v : V) ↦
            ‖v‖ ^ k *
              Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin n) ↦ V) E)
                (iteratedFDeriv ℝ n f v))
          (volume : Measure V)
k n : ℕ
hk : (↑k : ℕ∞) ≤ K
hn_1 : (↑n : ℕ∞) ≤ N
w : V
Z :
  ‖w‖ ^ n *
      (‖w‖ ^ n *
        Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin k) ↦ V) E)
          (iteratedFDeriv ℝ k (𝓕 f) w)) ≤
    ‖w‖ ^ n *
      ((2 * (π * Norm.norm.{u_2} (E := V →L⋆[ℝ] V →L[ℝ] ℝ) (innerSL ℝ))) ^ k *
        ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 2) ^ n *
          ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1),
            @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
              ‖v‖ ^ p.1 *
                Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin p.2) ↦ V) E)
                  (iteratedFDeriv ℝ p.2 f v)))
hn : n ≠ 0
hw : w ≠ 0
⊢ ‖w‖ ^ n *
      Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin k) ↦ V) E)
        (iteratedFDeriv ℝ k (𝓕 f) w) ≤
    (2 * (π * Norm.norm.{u_2} (E := V →L⋆[ℝ] V →L[ℝ] ℝ) (innerSL ℝ))) ^ k *
      ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 2) ^ n *
        ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1),
          @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
            ‖v‖ ^ p.1 *
              Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin p.2) ↦ V) E)
                (iteratedFDeriv ℝ p.2 f v))

Tactic:
rw [mul_le_mul_iff_right₀ (pow_pos (by simp [hw]) n)] at Z

Premises used: pow_pos, mul_le_mul_iff_right₀
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
V : Type u_2
inst_2 : NormedAddCommGroup V
inst_3 : InnerProductSpace ℝ V
inst_4 : FiniteDimensional ℝ V
inst_5 : MeasurableSpace V
inst_6 : BorelSpace V
f : V → E
K N : ℕ∞
hf : ContDiff ℝ (↑N : ℕ∞ω) f
h'f :
  ∀ (k n : ℕ),
    (↑k : ℕ∞) ≤ K →
      (↑n : ℕ∞) ≤ N →
        @Integrable ℝ _ _ _ inst_5
          (fun (v : V) ↦
            ‖v‖ ^ k *
              Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin n) ↦ V) E)
                (iteratedFDeriv ℝ n f v))
          (volume : Measure V)
k n : ℕ
hk : (↑k : ℕ∞) ≤ K
hn_1 : (↑n : ℕ∞) ≤ N
w : V
Z :
  ‖w‖ ^ n *
      (‖w‖ ^ n *
        Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin k) ↦ V) E)
          (iteratedFDeriv ℝ k (𝓕 f) w)) ≤
    ‖w‖ ^ n *
      ((2 * (π * Norm.norm.{u_2} (E := V →L⋆[ℝ] V →L[ℝ] ℝ) (innerSL ℝ))) ^ k *
        ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 2) ^ n *
          ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1),
            @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
              ‖v‖ ^ p.1 *
                Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin p.2) ↦ V) E)
                  (iteratedFDeriv ℝ p.2 f v)))
hn : n ≠ 0
hw : w ≠ 0
Z₁ :
  ‖w‖ ^ n *
      Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin k) ↦ V) E)
        (iteratedFDeriv ℝ k (𝓕 f) w) ≤
    (2 * (π * Norm.norm.{u_2} (E := V →L⋆[ℝ] V →L[ℝ] ℝ) (innerSL ℝ))) ^ k *
      ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 2) ^ n *
        ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1),
          @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
            ‖v‖ ^ p.1 *
              Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin p.2) ↦ V) E)
                (iteratedFDeriv ℝ p.2 f v))
⊢ n ≠ 0

Tactic:
rw [mul_le_mul_iff_right₀ (pow_pos (by simp [hw]) n)] at Z

Premises used: pow_pos, mul_le_mul_iff_right₀
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
V : Type u_2
inst_2 : NormedAddCommGroup V
inst_3 : InnerProductSpace ℝ V
inst_4 : FiniteDimensional ℝ V
inst_5 : MeasurableSpace V
inst_6 : BorelSpace V
f : V → E
K N : ℕ∞
hf : ContDiff ℝ (↑N : ℕ∞ω) f
h'f :
  ∀ (k n : ℕ),
    (↑k : ℕ∞) ≤ K →
      (↑n : ℕ∞) ≤ N →
        @Integrable ℝ _ _ _ inst_5
          (fun (v : V) ↦
            ‖v‖ ^ k *
              Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin n) ↦ V) E)
                (iteratedFDeriv ℝ n f v))
          (volume : Measure V)
k n : ℕ
hk : (↑k : ℕ∞) ≤ K
hn_1 : (↑n : ℕ∞) ≤ N
w : V
Z :
  ‖w‖ ^ n *
      (‖w‖ ^ n *
        Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin k) ↦ V) E)
          (iteratedFDeriv ℝ k (𝓕 f) w)) ≤
    ‖w‖ ^ n *
      ((2 * (π * Norm.norm.{u_2} (E := V →L⋆[ℝ] V →L[ℝ] ℝ) (innerSL ℝ))) ^ k *
        ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 2) ^ n *
          ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1),
            @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
              ‖v‖ ^ p.1 *
                Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin p.2) ↦ V) E)
                  (iteratedFDeriv ℝ p.2 f v)))
hn : n ≠ 0
hw : w ≠ 0
Z₁ :
  ‖w‖ ^ n *
      Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin k) ↦ V) E)
        (iteratedFDeriv ℝ k (𝓕 f) w) ≤
    (2 * (π * Norm.norm.{u_2} (E := V →L⋆[ℝ] V →L[ℝ] ℝ) (innerSL ℝ))) ^ k *
      ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 2) ^ n *
        ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1),
          @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
            ‖v‖ ^ p.1 *
              Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin p.2) ↦ V) E)
                (iteratedFDeriv ℝ p.2 f v))
hn₁ : n ≠ 0
⊢ w ≠ 0

Tactic:
rw [mul_le_mul_iff_right₀ (pow_pos (by simp [hw]) n)] at Z

Premises used: pow_pos, mul_le_mul_iff_right₀
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
V : Type u_2
inst_2 : NormedAddCommGroup V
inst_3 : InnerProductSpace ℝ V
inst_4 : FiniteDimensional ℝ V
inst_5 : MeasurableSpace V
inst_6 : BorelSpace V
f : V → E
K N : ℕ∞
hf : ContDiff ℝ (↑N : ℕ∞ω) f
h'f :
  ∀ (k n : ℕ),
    (↑k : ℕ∞) ≤ K →
      (↑n : ℕ∞) ≤ N →
        @Integrable ℝ _ _ _ inst_5
          (fun (v : V) ↦
            ‖v‖ ^ k *
              Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin n) ↦ V) E)
                (iteratedFDeriv ℝ n f v))
          (volume : Measure V)
k n : ℕ
hk : (↑k : ℕ∞) ≤ K
hn_1 : (↑n : ℕ∞) ≤ N
w : V
Z :
  ‖w‖ ^ n *
      Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin k) ↦ V) E)
        (iteratedFDeriv ℝ k (𝓕 f) w) ≤
    (2 * (π * Norm.norm.{u_2} (E := V →L⋆[ℝ] V →L[ℝ] ℝ) (innerSL ℝ))) ^ k *
      ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 2) ^ n *
        ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1),
          @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
            ‖v‖ ^ p.1 *
              Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin p.2) ↦ V) E)
                (iteratedFDeriv ℝ p.2 f v))
hn : n ≠ 0
hw : w ≠ 0
inr :
  (2 * (π * Norm.norm.{u_2} (E := V →L⋆[ℝ] V →L[ℝ] ℝ) (innerSL ℝ))) ^ k *
      ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 2) ^ n *
        ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1),
          @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
            ‖v‖ ^ p.1 *
              Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin p.2) ↦ V) E)
                (iteratedFDeriv ℝ p.2 f v)) ≤
    (2 * π) ^ k * (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 2) ^ n *
      ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1),
        @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
          ‖v‖ ^ p.1 *
            Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin p.2) ↦ V) E)
              (iteratedFDeriv ℝ p.2 f v)
⊢ ‖w‖ ^ n *
      Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin k) ↦ V) E)
        (iteratedFDeriv ℝ k (𝓕 f) w) ≤
    (2 * π) ^ k * (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 2) ^ n *
      ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1),
        @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
          ‖v‖ ^ p.1 *
            Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin p.2) ↦ V) E)
              (iteratedFDeriv ℝ p.2 f v)

Tactic:
apply Z.trans

Premises used: LE.le.trans
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
V : Type u_2
inst_2 : NormedAddCommGroup V
inst_3 : InnerProductSpace ℝ V
inst_4 : FiniteDimensional ℝ V
inst_5 : MeasurableSpace V
inst_6 : BorelSpace V
f : V → E
K N : ℕ∞
hf : ContDiff ℝ (↑N : ℕ∞ω) f
h'f :
  ∀ (k n : ℕ),
    (↑k : ℕ∞) ≤ K →
      (↑n : ℕ∞) ≤ N →
        @Integrable ℝ _ _ _ inst_5
          (fun (v : V) ↦
            ‖v‖ ^ k *
              Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin n) ↦ V) E)
                (iteratedFDeriv ℝ n f v))
          (volume : Measure V)
k n : ℕ
hk : (↑k : ℕ∞) ≤ K
hn_1 : (↑n : ℕ∞) ≤ N
w : V
Z :
  ‖w‖ ^ n *
      Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin k) ↦ V) E)
        (iteratedFDeriv ℝ k (𝓕 f) w) ≤
    (2 * (π * Norm.norm.{u_2} (E := V →L⋆[ℝ] V →L[ℝ] ℝ) (innerSL ℝ))) ^ k *
      ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 2) ^ n *
        ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1),
          @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
            ‖v‖ ^ p.1 *
              Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin p.2) ↦ V) E)
                (iteratedFDeriv ℝ p.2 f v))
hn : n ≠ 0
hw : w ≠ 0
rw :
  (2 * (π * 1)) ^ k * (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 2) ^ n *
    ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1),
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
        ‖v‖ ^ p.1 *
          Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin p.2) ↦ V) E)
            (iteratedFDeriv ℝ p.2 f v)
| (2 * π) ^ k * (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 2) ^ n *
    ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1),
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
        ‖v‖ ^ p.1 *
          Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin p.2) ↦ V) E)
            (iteratedFDeriv ℝ p.2 f v)

Tactic:
rw [← mul_one π]

Premises used: Real.pi, mul_one
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
V : Type u_2
inst_2 : NormedAddCommGroup V
inst_3 : InnerProductSpace ℝ V
inst_4 : FiniteDimensional ℝ V
inst_5 : MeasurableSpace V
inst_6 : BorelSpace V
f : V → E
K N : ℕ∞
hf : ContDiff ℝ (↑N : ℕ∞ω) f
h'f :
  ∀ (k n : ℕ),
    (↑k : ℕ∞) ≤ K →
      (↑n : ℕ∞) ≤ N →
        @Integrable ℝ _ _ _ inst_5
          (fun (v : V) ↦
            ‖v‖ ^ k *
              Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin n) ↦ V) E)
                (iteratedFDeriv ℝ n f v))
          (volume : Measure V)
k n : ℕ
hk : (↑k : ℕ∞) ≤ K
hn_1 : (↑n : ℕ∞) ≤ N
w : V
Z :
  ‖w‖ ^ n *
      Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin k) ↦ V) E)
        (iteratedFDeriv ℝ k (𝓕 f) w) ≤
    (2 * (π * Norm.norm.{u_2} (E := V →L⋆[ℝ] V →L[ℝ] ℝ) (innerSL ℝ))) ^ k *
      ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 2) ^ n *
        ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1),
          @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
            ‖v‖ ^ p.1 *
              Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin p.2) ↦ V) E)
                (iteratedFDeriv ℝ p.2 f v))
hn : n ≠ 0
hw : w ≠ 0
inr :
  (2 * (π * Norm.norm.{u_2} (E := V →L⋆[ℝ] V →L[ℝ] ℝ) (innerSL ℝ))) ^ k *
      ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 2) ^ n *
        ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1),
          @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
            ‖v‖ ^ p.1 *
              Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin p.2) ↦ V) E)
                (iteratedFDeriv ℝ p.2 f v)) ≤
    (2 * (π * 1)) ^ k * (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 2) ^ n *
      ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1),
        @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
          ‖v‖ ^ p.1 *
            Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin p.2) ↦ V) E)
              (iteratedFDeriv ℝ p.2 f v)
⊢ (2 * (π * Norm.norm.{u_2} (E := V →L⋆[ℝ] V →L[ℝ] ℝ) (innerSL ℝ))) ^ k *
      ((HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 2) ^ n *
        ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1),
          @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
            ‖v‖ ^ p.1 *
              Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin p.2) ↦ V) E)
                (iteratedFDeriv ℝ p.2 f v)) ≤
    (2 * π) ^ k * (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 2) ^ n *
      ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1),
        @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
          ‖v‖ ^ p.1 *
            Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin p.2) ↦ V) E)
              (iteratedFDeriv ℝ p.2 f v)

Tactic:
conv_rhs => rw [← mul_one π]

Premises used: Real.pi, mul_one