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 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 * (π * 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)

Tactic:
simp only [mul_assoc]

Premises used: mul_assoc
-- 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 : Norm.norm.{u_2} (E := V →L⋆[ℝ] V →L[ℝ] ℝ) (innerSL ℝ) ≤ 1
⊢ (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))

Tactic:
gcongr
-- 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
⊢ 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 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
⊢ 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
f : ℝ → E
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
hf' : @Integrable.{u_1, 0} E _ _ _ MeasureSpace.toMeasurableSpace (fun (x : ℝ) ↦ x • f x) volume
w : ℝ
⊢ @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (v : ℝ) ↦ ‖v‖ * ‖f v‖) volume

Tactic:
simpa only [norm_smul] using hf'.norm

Premises used: norm_smul, MeasureTheory.Integrable.norm
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
hf' : @Integrable.{u_1, 0} E _ _ _ MeasureSpace.toMeasurableSpace (fun (x : ℝ) ↦ x • f x) volume
w : ℝ
⊢ @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (v : ℝ) ↦ ‖v‖ * ‖f v‖) volume

Tactic:
have hf'' : Integrable (fun v : ℝ ↦ ‖v‖ * ‖f v‖) := by simpa only [norm_smul] using hf'.norm
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
hf' : @Integrable.{u_1, 0} E _ _ _ MeasureSpace.toMeasurableSpace (fun (x : ℝ) ↦ x • f x) volume
w : ℝ
hf'' : @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (v : ℝ) ↦ ‖v‖ * ‖f v‖) volume
L : ℝ →L[ℝ] ℝ →L[ℝ] ℝ := ContinuousLinearMap.flip (ContinuousLinearMap.mul ℝ ℝ)
this :
  @Integrable.{u_1, 0} (ℝ →L[ℝ] E) _ _ _ MeasureSpace.toMeasurableSpace
    (fun (v : ℝ) ↦ ContinuousLinearMap.smulRight (S := ℝ) ((L : (a : ℝ) → ℝ →L[ℝ] ℝ) v) (f v)) volume
⊢ @Integrable.{u_1, 0} (ℝ →L[ℝ] E) _ _ _ MeasureSpace.toMeasurableSpace (fun (v : ℝ) ↦ fourierSMulRight L f v) volume

Tactic:
simpa only [fourierSMulRight, neg_smul, neg_mul, Pi.smul_apply] using this.smul (-2 * π * I)

Premises used: VectorFourier.fourierSMulRight, neg_smul, Real.pi, HMul.hMul, MeasureTheory.Integrable.smul, Complex.ofReal, neg_mul, OfNat.ofNat, Neg.neg, Complex.I, Pi.smul_apply
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
hf' : @Integrable.{u_1, 0} E _ _ _ MeasureSpace.toMeasurableSpace (fun (x : ℝ) ↦ x • f x) volume
w : ℝ
hf'' : @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (v : ℝ) ↦ ‖v‖ * ‖f v‖) volume
L : ℝ →L[ℝ] ℝ →L[ℝ] ℝ := ContinuousLinearMap.flip (ContinuousLinearMap.mul ℝ ℝ)
suffices :
  @Integrable.{u_1, 0} (ℝ →L[ℝ] E) _ _ _ MeasureSpace.toMeasurableSpace
    (fun (v : ℝ) ↦ ContinuousLinearMap.smulRight (S := ℝ) ((L : (a : ℝ) → ℝ →L[ℝ] ℝ) v) (f v)) volume
⊢ @Integrable.{u_1, 0} (ℝ →L[ℝ] E) _ _ _ MeasureSpace.toMeasurableSpace (fun (v : ℝ) ↦ fourierSMulRight L f v) volume

Tactic:
suffices Integrable fun v ↦ ContinuousLinearMap.smulRight (L v) (f v) by
      simpa only [fourierSMulRight, neg_smul, neg_mul, Pi.smul_apply] using this.smul (-2 * π * I)
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
hf' : @Integrable.{u_1, 0} E _ _ _ MeasureSpace.toMeasurableSpace (fun (x : ℝ) ↦ x • f x) volume
w : ℝ
hf'' : @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (v : ℝ) ↦ ‖v‖ * ‖f v‖) volume
L : ℝ →L[ℝ] ℝ →L[ℝ] ℝ := ContinuousLinearMap.flip (ContinuousLinearMap.mul ℝ ℝ)
⊢ @Integrable.{u_1, 0} (ℝ →L[ℝ] E) _ _ _ MeasureSpace.toMeasurableSpace
    (fun (a : ℝ) ↦
      ((↑(↑(ContinuousLinearMap.toSpanSingletonLIE ℝ E) : E ≃L[ℝ] ℝ →L[ℝ] E) : E →L[ℝ] ℝ →L[ℝ] E) : (a : E) → ℝ →L[ℝ] E)
        (a • f a))
    volume

Tactic:
((ContinuousLinearMap.toSpanSingletonLIE ℝ
      E).toContinuousLinearEquiv.toContinuousLinearMap).integrable_comp hf'

Premises used: Real, ContinuousLinearMap.integrable_comp, ContinuousLinearMap.toSpanSingletonLIE, LinearIsometryEquiv.toContinuousLinearEquiv, ContinuousLinearEquiv.toContinuousLinearMap
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
hf' : @Integrable.{u_1, 0} E _ _ _ MeasureSpace.toMeasurableSpace (fun (x : ℝ) ↦ x • f x) volume
w : ℝ
hf'' : @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (v : ℝ) ↦ ‖v‖ * ‖f v‖) volume
L : ℝ →L[ℝ] ℝ →L[ℝ] ℝ := ContinuousLinearMap.flip (ContinuousLinearMap.mul ℝ ℝ)
h :
  ∀ (v : ℝ),
    Eq (α := ℝ →L[ℝ] E) (ContinuousLinearMap.smulRight (S := ℝ) ((L : (a : ℝ) → ℝ →L[ℝ] ℝ) v) (f v))
      (((↑(↑(ContinuousLinearMap.toSpanSingletonLIE ℝ E) : E ≃L[ℝ] ℝ →L[ℝ] E) : E →L[ℝ] ℝ →L[ℝ] E) :
          (a : E) → ℝ →L[ℝ] E)
        (v • f v))
⊢ @Integrable.{u_1, 0} (ℝ →L[ℝ] E) _ _ _ MeasureSpace.toMeasurableSpace
    (fun (v : ℝ) ↦ ContinuousLinearMap.smulRight (S := ℝ) ((L : (a : ℝ) → ℝ →L[ℝ] ℝ) v) (f v)) volume

Tactic:
convert ((ContinuousLinearMap.toSpanSingletonLIE ℝ
      E).toContinuousLinearEquiv.toContinuousLinearMap).integrable_comp hf' using 2 with _ v

Premises used: Real, ContinuousLinearMap.integrable_comp, ContinuousLinearMap.toSpanSingletonLIE, LinearIsometryEquiv.toContinuousLinearEquiv, ContinuousLinearEquiv.toContinuousLinearMap
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
hf' : @Integrable.{u_1, 0} E _ _ _ MeasureSpace.toMeasurableSpace (fun (x : ℝ) ↦ x • f x) volume
w : ℝ
hf'' : @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (v : ℝ) ↦ ‖v‖ * ‖f v‖) volume
L : ℝ →L[ℝ] ℝ →L[ℝ] ℝ := ContinuousLinearMap.flip (ContinuousLinearMap.mul ℝ ℝ)
v : ℝ
h :
  Eq (α := E) ((ContinuousLinearMap.smulRight (S := ℝ) ((L : (a : ℝ) → ℝ →L[ℝ] ℝ) v) (f v) : (a : ℝ) → E) 1 : E)
    (((((↑(↑(ContinuousLinearMap.toSpanSingletonLIE ℝ E) : E ≃L[ℝ] ℝ →L[ℝ] E) : E →L[ℝ] ℝ →L[ℝ] E) :
                (a : E) → ℝ →L[ℝ] E)
              (v • f v) :
            ℝ →L[ℝ] E) :
          (a : ℝ) → E)
        1 :
      E)
⊢ Eq (α := ℝ →L[ℝ] E) (ContinuousLinearMap.smulRight (S := ℝ) ((L : (a : ℝ) → ℝ →L[ℝ] ℝ) v) (f v))
    (((↑(↑(ContinuousLinearMap.toSpanSingletonLIE ℝ E) : E ≃L[ℝ] ℝ →L[ℝ] E) : E →L[ℝ] ℝ →L[ℝ] E) : (a : E) → ℝ →L[ℝ] E)
      (v • f v))

Tactic:
apply ContinuousLinearMap.ext_ring

Premises used: ContinuousLinearMap.ext_ring
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
hf' : @Integrable.{u_1, 0} E _ _ _ MeasureSpace.toMeasurableSpace (fun (x : ℝ) ↦ x • f x) volume
w : ℝ
hf'' : @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (v : ℝ) ↦ ‖v‖ * ‖f v‖) volume
L : ℝ →L[ℝ] ℝ →L[ℝ] ℝ := ContinuousLinearMap.flip (ContinuousLinearMap.mul ℝ ℝ)
v : ℝ
h :
  v • f v =
    (HSMul.hSMul (β := ℝ →L[ℝ] E) v
          (((↑(↑(ContinuousLinearMap.toSpanSingletonLIE ℝ E) : E ≃L[ℝ] ℝ →L[ℝ] E) : E →L[ℝ] ℝ →L[ℝ] E) :
                (a : E) → ℝ →L[ℝ] E)
              (f v) :
            ℝ →L[ℝ] E) :
        (a : ℝ) → E)
      1
⊢ Eq (α := E) ((ContinuousLinearMap.smulRight (S := ℝ) ((L : (a : ℝ) → ℝ →L[ℝ] ℝ) v) (f v) : (a : ℝ) → E) 1 : E)
    (((((↑(↑(ContinuousLinearMap.toSpanSingletonLIE ℝ E) : E ≃L[ℝ] ℝ →L[ℝ] E) : E →L[ℝ] ℝ →L[ℝ] E) :
                (a : E) → ℝ →L[ℝ] E)
              (v • f v) :
            ℝ →L[ℝ] E) :
          (a : ℝ) → E)
        1 :
      E)

Tactic:
rw [ContinuousLinearMap.smulRight_apply, ContinuousLinearMap.flip_apply,
      ContinuousLinearMap.mul_apply', one_mul, map_smul]

Premises used: ContinuousLinearMap.flip_apply, ContinuousLinearMap.mul_apply', ContinuousLinearMap.smulRight_apply, one_mul, map_smul
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
hf' : @Integrable.{u_1, 0} E _ _ _ MeasureSpace.toMeasurableSpace (fun (x : ℝ) ↦ x • f x) volume
w : ℝ
hf'' : @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (v : ℝ) ↦ ‖v‖ * ‖f v‖) volume
L : ℝ →L[ℝ] ℝ →L[ℝ] ℝ := ContinuousLinearMap.flip (ContinuousLinearMap.mul ℝ ℝ)
v : ℝ
⊢ v • f v =
    (HSMul.hSMul (β := ℝ →L[ℝ] E) v
          (((↑(↑(ContinuousLinearMap.toSpanSingletonLIE ℝ E) : E ≃L[ℝ] ℝ →L[ℝ] E) : E →L[ℝ] ℝ →L[ℝ] E) :
                (a : E) → ℝ →L[ℝ] E)
              (f v) :
            ℝ →L[ℝ] E) :
        (a : ℝ) → E)
      1

Tactic:
congr_arg (fun x ↦ v • x) (one_smul ℝ (f v)).symm

Premises used: Real, one_smul, congr_arg, HSMul.hSMul, Eq.symm
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
hf' : @Integrable.{u_1, 0} E _ _ _ MeasureSpace.toMeasurableSpace (fun (x : ℝ) ↦ x • f x) volume
w : ℝ
hf'' : @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (v : ℝ) ↦ ‖v‖ * ‖f v‖) volume
L : ℝ →L[ℝ] ℝ →L[ℝ] ℝ := ContinuousLinearMap.flip (ContinuousLinearMap.mul ℝ ℝ)
v : ℝ
⊢ v • f v =
    (HSMul.hSMul (β := ℝ →L[ℝ] E) v
          (((↑(↑(ContinuousLinearMap.toSpanSingletonLIE ℝ E) : E ≃L[ℝ] ℝ →L[ℝ] E) : E →L[ℝ] ℝ →L[ℝ] E) :
                (a : E) → ℝ →L[ℝ] E)
              (f v) :
            ℝ →L[ℝ] E) :
        (a : ℝ) → E)
      1

Tactic:
exact congr_arg (fun x ↦ v • x) (one_smul ℝ (f v)).symm

Premises used: Real, one_smul, congr_arg, HSMul.hSMul, Eq.symm
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
hf' : @Integrable.{u_1, 0} E _ _ _ MeasureSpace.toMeasurableSpace (fun (x : ℝ) ↦ x • f x) volume
w : ℝ
hf'' : @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (v : ℝ) ↦ ‖v‖ * ‖f v‖) volume
L : ℝ →L[ℝ] ℝ →L[ℝ] ℝ := ContinuousLinearMap.flip (ContinuousLinearMap.mul ℝ ℝ)
⊢ @Integrable.{u_1, 0} (ℝ →L[ℝ] E) _ _ _ MeasureSpace.toMeasurableSpace (fun (v : ℝ) ↦ fourierSMulRight L f v) volume

Tactic:
have h_int : Integrable fun v ↦ fourierSMulRight L f v := by
    suffices Integrable fun v ↦ ContinuousLinearMap.smulRight (L v) (f v) by
      simpa only [fourierSMulRight, neg_smul, neg_mul, Pi.smul_apply] using this.smul (-2 * π * I)
    convert ((ContinuousLinearMap.toSpanSingletonLIE ℝ
      E).toContinuousLinearEquiv.toContinuousLinearMap).integrable_comp hf' using 2 with _ v
    apply ContinuousLinearMap.ext_ring
    rw [ContinuousLinearMap.smulRight_apply, ContinuousLinearMap.flip_apply,
      ContinuousLinearMap.mul_apply', one_mul, map_smul]
    exact congr_arg (fun x ↦ v • x) (one_smul ℝ (f v)).symm
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
hf' : @Integrable.{u_1, 0} E _ _ _ MeasureSpace.toMeasurableSpace (fun (x : ℝ) ↦ x • f x) volume
w : ℝ
hf'' : @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (v : ℝ) ↦ ‖v‖ * ‖f v‖) volume
L : ℝ →L[ℝ] ℝ →L[ℝ] ℝ := ContinuousLinearMap.flip (ContinuousLinearMap.mul ℝ ℝ)
h_int :
  @Integrable.{u_1, 0} (ℝ →L[ℝ] E) _ _ _ MeasureSpace.toMeasurableSpace (fun (v : ℝ) ↦ fourierSMulRight L f v) volume
⊢ HasDerivAt (fourierIntegral 𝐞 volume L.toLinearMap₁₂ f)
    ((fourierIntegral 𝐞 volume L.toLinearMap₁₂ (fourierSMulRight L f) w : (a : ℝ) → E) 1) w

Tactic:
(VectorFourier.hasFDerivAt_fourierIntegral L hf hf'' w).hasDerivAt

Premises used: VectorFourier.hasFDerivAt_fourierIntegral, HasFDerivAt.hasDerivAt
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
hf' : @Integrable.{u_1, 0} E _ _ _ MeasureSpace.toMeasurableSpace (fun (x : ℝ) ↦ x • f x) volume
w : ℝ
hf'' : @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (v : ℝ) ↦ ‖v‖ * ‖f v‖) volume
L : ℝ →L[ℝ] ℝ →L[ℝ] ℝ := ContinuousLinearMap.flip (ContinuousLinearMap.mul ℝ ℝ)
h_int :
  @Integrable.{u_1, 0} (ℝ →L[ℝ] E) _ _ _ MeasureSpace.toMeasurableSpace (fun (v : ℝ) ↦ fourierSMulRight L f v) volume
h :
  𝓕 (E := (x : ℝ) → E) (fun (x : ℝ) ↦ (-2 * (↑π : ℂ) * I * (↑x : ℂ)) • f x) w =
    (fourierIntegral 𝐞 volume L.toLinearMap₁₂ (fourierSMulRight L f) w : (a : ℝ) → E) 1
⊢ HasDerivAt (𝓕 f) (𝓕 (E := (x : ℝ) → E) (fun (x : ℝ) ↦ (-2 * (↑π : ℂ) * I * (↑x : ℂ)) • f x) w) w

Tactic:
convert! (VectorFourier.hasFDerivAt_fourierIntegral L hf hf'' w).hasDerivAt using 1

Premises used: VectorFourier.hasFDerivAt_fourierIntegral, HasFDerivAt.hasDerivAt
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
hf' : @Integrable.{u_1, 0} E _ _ _ MeasureSpace.toMeasurableSpace (fun (x : ℝ) ↦ x • f x) volume
w : ℝ
hf'' : @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (v : ℝ) ↦ ‖v‖ * ‖f v‖) volume
L : ℝ →L[ℝ] ℝ →L[ℝ] ℝ := ContinuousLinearMap.flip (ContinuousLinearMap.mul ℝ ℝ)
h_int :
  @Integrable.{u_1, 0} (ℝ →L[ℝ] E) _ _ _ MeasureSpace.toMeasurableSpace (fun (v : ℝ) ↦ fourierSMulRight L f v) volume
h :
  Eq.{u_1 + 1} (α := E)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : ℝ) ↦
      HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-(v * w)) : Circle) ((-2 * (↑π : ℂ) * I * (↑v : ℂ)) • f v))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : ℝ) ↦
      HSMul.hSMul (α := Circle) (β := E)
        ((𝐞 : (a : ℝ) → Circle) (-(((L.toLinearMap₁₂ : (a : ℝ) → ℝ →ₗ[ℝ] ℝ) v : ℝ →ₗ[ℝ] ℝ) : (a : ℝ) → ℝ) w) : Circle)
        ((fourierSMulRight L f v : (a : ℝ) → E) 1 : E))
⊢ 𝓕 (E := (x : ℝ) → E) (fun (x : ℝ) ↦ (-2 * (↑π : ℂ) * I * (↑x : ℂ)) • f x) w =
    (fourierIntegral 𝐞 volume L.toLinearMap₁₂ (fourierSMulRight L f) w : (a : ℝ) → E) 1

Tactic:
rw [fourierIntegral_continuousLinearMap_apply' h_int, VectorFourier.fourierIntegral,
    fourier_real_eq]

Premises used: Real.fourier_real_eq, VectorFourier.fourierIntegral, Real.fourierIntegral_continuousLinearMap_apply'
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
hf' : @Integrable.{u_1, 0} E _ _ _ MeasureSpace.toMeasurableSpace (fun (x : ℝ) ↦ x • f x) volume
w : ℝ
hf'' : @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (v : ℝ) ↦ ‖v‖ * ‖f v‖) volume
L : ℝ →L[ℝ] ℝ →L[ℝ] ℝ := ContinuousLinearMap.flip (ContinuousLinearMap.mul ℝ ℝ)
h_int :
  @Integrable.{u_1, 0} (ℝ →L[ℝ] E) _ _ _ MeasureSpace.toMeasurableSpace (fun (v : ℝ) ↦ fourierSMulRight L f v) volume
⊢ Eq.{u_1 + 1} (α := E)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : ℝ) ↦
      HSMul.hSMul (α := Circle) ((𝐞 : (a : ℝ) → Circle) (-(v * w)) : Circle) ((-2 * (↑π : ℂ) * I * (↑v : ℂ)) • f v))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : ℝ) ↦
      HSMul.hSMul (α := Circle) (β := E)
        ((𝐞 : (a : ℝ) → Circle) (-(((L.toLinearMap₁₂ : (a : ℝ) → ℝ →ₗ[ℝ] ℝ) v : ℝ →ₗ[ℝ] ℝ) : (a : ℝ) → ℝ) w) : Circle)
        ((fourierSMulRight L f v : (a : ℝ) → E) 1 : E))

Tactic:
simp [fourierSMulRight, L, ContinuousLinearMap.smul_apply,
    ContinuousLinearMap.smulRight_apply, ContinuousLinearMap.mul_apply', ← neg_mul, mul_smul]

Premises used: VectorFourier.fourierSMulRight, ContinuousLinearMap.smul_apply, ContinuousLinearMap.mul_apply', neg_mul, ContinuousLinearMap.smulRight_apply, SemigroupAction.mul_smul
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
hf : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace f volume
hf' : @Integrable.{u_1, 0} E _ _ _ MeasureSpace.toMeasurableSpace (fun (x : ℝ) ↦ x • f x) volume
h : ∀ (x : ℝ), deriv (𝓕 f) x = 𝓕 (E := (x : ℝ) → E) (fun (x : ℝ) ↦ (-2 * (↑π : ℂ) * I * (↑x : ℂ)) • f x) x
⊢ deriv (𝓕 f) = 𝓕 (E := (x : ℝ) → E) fun (x : ℝ) ↦ (-2 * (↑π : ℂ) * I * (↑x : ℂ)) • f x

Tactic:
ext x