awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
Goal:
V : Type u_1
W : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : NormedAddCommGroup W
inst_3 : NormedSpace ℝ W
L : ContinuousLinearMap.{0, 0, u_1, u_2} (RingHom.id ℝ) V (W →L[ℝ] ℝ)
v : V
w : W
ha :
  HasFDerivAt (𝕜 := ℝ) (F := ℝ) (fun (w' : W) ↦ (((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w')
    ((L : (a : V) → W →L[ℝ] ℝ) v) w
h :
  addCommGroup = NormedAddCommGroup.toAddCommGroup →
    HEq (α := Module ℝ ℂ) NormedSpace.toModule (β := Module ℝ ℂ) NormedSpace.toModule →
      HSMul.hSMul (β := W →L[ℝ] ℂ)
          (-2 * (↑π : ℂ) * I *
            (↑((𝐞 : (a : ℝ) → Circle) (-(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w)) : ℂ))
          (ofRealCLM.comp (σ₁₂ := RingHom.id ℝ) ((L : (a : V) → W →L[ℝ] ℝ) v)) =
        ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ)
          (ContinuousLinearMap.toSpanSingleton ℝ
            (2 * (↑π : ℂ) * I *
              (↑((𝐞 : (a : ℝ) → Circle) (-(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w)) : ℂ)))
          (-(L : (a : V) → W →L[ℝ] ℝ) v)
⊢ HasFDerivAt
    (fun (w : W) ↦ (↑((𝐞 : (a : ℝ) → Circle) (-(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w)) : ℂ))
    (HSMul.hSMul (β := W →L[ℝ] ℂ)
      (-2 * (↑π : ℂ) * I *
        (↑((𝐞 : (a : ℝ) → Circle) (-(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w)) : ℂ))
      (ofRealCLM.comp (σ₁₂ := RingHom.id ℝ) ((L : (a : V) → W →L[ℝ] ℝ) v)))
    w

Tactic:
convert! (hasDerivAt_fourierChar (-L v w)).hasFDerivAt.comp w ha.neg using 1

Premises used: HasFDerivAt.neg, HasFDerivAt.comp
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
Goal:
V : Type u_1
W : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : NormedAddCommGroup W
inst_3 : NormedSpace ℝ W
L : ContinuousLinearMap.{0, 0, u_1, u_2} (RingHom.id ℝ) V (W →L[ℝ] ℝ)
v : V
w : W
ha :
  HasFDerivAt (𝕜 := ℝ) (F := ℝ) (fun (w' : W) ↦ (((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w')
    ((L : (a : V) → W →L[ℝ] ℝ) v) w
e_8 : addCommGroup = NormedAddCommGroup.toAddCommGroup
e_9 : HEq (α := Module ℝ ℂ) NormedSpace.toModule (β := Module ℝ ℂ) NormedSpace.toModule
h :
  ∀ (y : W),
    Eq (α := ℂ)
      ((HSMul.hSMul (β := W →L[ℝ] ℂ)
              (-2 * (↑π : ℂ) * I *
                (↑((𝐞 : (a : ℝ) → Circle) (-(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w)) : ℂ))
              (ofRealCLM.comp (σ₁₂ := RingHom.id ℝ) ((L : (a : V) → W →L[ℝ] ℝ) v)) :
            (a : W) → ℂ)
          y :
        ℂ)
      ((ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ)
              (ContinuousLinearMap.toSpanSingleton ℝ
                (2 * (↑π : ℂ) * I *
                  (↑((𝐞 : (a : ℝ) → Circle) (-(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w)) : ℂ)))
              (-(L : (a : V) → W →L[ℝ] ℝ) v) :
            (a : W) → ℂ)
          y :
        ℂ)
⊢ HSMul.hSMul (β := W →L[ℝ] ℂ)
      (-2 * (↑π : ℂ) * I *
        (↑((𝐞 : (a : ℝ) → Circle) (-(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w)) : ℂ))
      (ofRealCLM.comp (σ₁₂ := RingHom.id ℝ) ((L : (a : V) → W →L[ℝ] ℝ) v)) =
    ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ)
      (ContinuousLinearMap.toSpanSingleton ℝ
        (2 * (↑π : ℂ) * I *
          (↑((𝐞 : (a : ℝ) → Circle) (-(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w)) : ℂ)))
      (-(L : (a : V) → W →L[ℝ] ℝ) v)

Tactic:
ext y
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
Goal:
V : Type u_1
W : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : NormedAddCommGroup W
inst_3 : NormedSpace ℝ W
L : ContinuousLinearMap.{0, 0, u_1, u_2} (RingHom.id ℝ) V (W →L[ℝ] ℝ)
v : V
w : W
ha :
  HasFDerivAt (𝕜 := ℝ) (F := ℝ) (fun (w' : W) ↦ (((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w')
    ((L : (a : V) → W →L[ℝ] ℝ) v) w
e_8 : addCommGroup = NormedAddCommGroup.toAddCommGroup
e_9 : HEq (α := Module ℝ ℂ) NormedSpace.toModule (β := Module ℝ ℂ) NormedSpace.toModule
y : W
h :
  2 * (↑π : ℂ) * I * (↑((𝐞 : (a : ℝ) → Circle) (-(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w)) : ℂ) *
      (↑((((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) y) : ℂ) =
    (↑((((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) y) : ℂ) *
      (2 * (↑π : ℂ) * I *
        (↑((𝐞 : (a : ℝ) → Circle) (-(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w)) : ℂ))
⊢ Eq (α := ℂ)
    ((HSMul.hSMul (β := W →L[ℝ] ℂ)
            (-2 * (↑π : ℂ) * I *
              (↑((𝐞 : (a : ℝ) → Circle) (-(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w)) : ℂ))
            (ofRealCLM.comp (σ₁₂ := RingHom.id ℝ) ((L : (a : V) → W →L[ℝ] ℝ) v)) :
          (a : W) → ℂ)
        y :
      ℂ)
    ((ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ)
            (ContinuousLinearMap.toSpanSingleton ℝ
              (2 * (↑π : ℂ) * I *
                (↑((𝐞 : (a : ℝ) → Circle) (-(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w)) : ℂ)))
            (-(L : (a : V) → W →L[ℝ] ℝ) v) :
          (a : W) → ℂ)
        y :
      ℂ)

Tactic:
simp only [neg_mul, ContinuousLinearMap.coe_smul', ContinuousLinearMap.coe_comp', Pi.smul_apply,
    Function.comp_apply, ofRealCLM_apply, smul_eq_mul, ContinuousLinearMap.comp_neg,
    ContinuousLinearMap.neg_apply, ContinuousLinearMap.toSpanSingleton_apply, real_smul, neg_inj]

Premises used: ContinuousLinearMap.comp_neg, ContinuousLinearMap.coe_comp', Complex.real_smul, ContinuousLinearMap.coe_smul', ContinuousLinearMap.toSpanSingleton_apply, Complex.ofRealCLM_apply, ContinuousLinearMap.neg_apply, neg_inj, Function.comp_apply, neg_mul, smul_eq_mul, Pi.smul_apply
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
Goal:
V : Type u_1
W : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : NormedAddCommGroup W
inst_3 : NormedSpace ℝ W
L : ContinuousLinearMap.{0, 0, u_1, u_2} (RingHom.id ℝ) V (W →L[ℝ] ℝ)
v : V
w : W
ha :
  HasFDerivAt (𝕜 := ℝ) (F := ℝ) (fun (w' : W) ↦ (((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w')
    ((L : (a : V) → W →L[ℝ] ℝ) v) w
e_8 : addCommGroup = NormedAddCommGroup.toAddCommGroup
e_9 : HEq (α := Module ℝ ℂ) NormedSpace.toModule (β := Module ℝ ℂ) NormedSpace.toModule
y : W
⊢ 2 * (↑π : ℂ) * I * (↑((𝐞 : (a : ℝ) → Circle) (-(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w)) : ℂ) *
      (↑((((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) y) : ℂ) =
    (↑((((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) y) : ℂ) *
      (2 * (↑π : ℂ) * I *
        (↑((𝐞 : (a : ℝ) → Circle) (-(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w)) : ℂ))

Tactic:
ring
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
Goal:
V : Type u_1
W : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : NormedAddCommGroup W
inst_3 : NormedSpace ℝ W
L : ContinuousLinearMap.{0, 0, u_1, u_2} (RingHom.id ℝ) V (W →L[ℝ] ℝ)
v : V
w y : W
simp :
  2 * (↑π : ℂ) * I * (↑((𝐞 : (a : ℝ) → Circle) (-(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w)) : ℂ) *
      (↑((((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) y) : ℂ) =
    2 * (↑π : ℂ) * I * (↑((((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) y) : ℂ) *
      (↑((𝐞 : (a : ℝ) → Circle) (-(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w)) : ℂ)
⊢ (fderiv ℝ
          (fun (w : W) ↦ (↑((𝐞 : (a : ℝ) → Circle) (-(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w)) : ℂ))
          w :
        (a : W) → ℂ)
      y =
    -2 * (↑π : ℂ) * I * (↑((((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) y) : ℂ) *
      (↑((𝐞 : (a : ℝ) → Circle) (-(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w)) : ℂ)

Tactic:
simp only [(hasFDerivAt_fourierChar_neg_bilinear_right L v w).fderiv, neg_mul,
    ContinuousLinearMap.coe_smul', ContinuousLinearMap.coe_comp', Pi.smul_apply,
    Function.comp_apply, ofRealCLM_apply, smul_eq_mul, neg_inj]

Premises used: ContinuousLinearMap.coe_comp', ContinuousLinearMap.coe_smul', Complex.ofRealCLM_apply, HasFDerivAt.fderiv, neg_inj, Function.comp_apply, neg_mul, Real.hasFDerivAt_fourierChar_neg_bilinear_right, smul_eq_mul, Pi.smul_apply
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
Goal:
V : Type u_1
W : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : NormedAddCommGroup W
inst_3 : NormedSpace ℝ W
L : ContinuousLinearMap.{0, 0, u_1, u_2} (RingHom.id ℝ) V (W →L[ℝ] ℝ)
v : V
w y : W
⊢ 2 * (↑π : ℂ) * I * (↑((𝐞 : (a : ℝ) → Circle) (-(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w)) : ℂ) *
      (↑((((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) y) : ℂ) =
    2 * (↑π : ℂ) * I * (↑((((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) y) : ℂ) *
      (↑((𝐞 : (a : ℝ) → Circle) (-(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w)) : ℂ)

Tactic:
ring
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
Goal:
V : Type u_1
W : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : NormedAddCommGroup W
inst_3 : NormedSpace ℝ W
L : ContinuousLinearMap.{0, 0, u_1, u_2} (RingHom.id ℝ) V (W →L[ℝ] ℝ)
v : V
⊢ Differentiable ℝ (F := ℂ) fun (w : W) ↦
    (↑((𝐞 : (a : ℝ) → Circle) (-(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w)) : ℂ)

Tactic:
fun w ↦ (hasFDerivAt_fourierChar_neg_bilinear_right L v w).differentiableAt

Premises used: Differentiable, HasFDerivAt.differentiableAt, Real.hasFDerivAt_fourierChar_neg_bilinear_right
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
Goal:
V : Type u_1
W : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : NormedAddCommGroup W
inst_3 : NormedSpace ℝ W
L : ContinuousLinearMap.{0, 0, u_1, u_2} (RingHom.id ℝ) V (W →L[ℝ] ℝ)
v : V
w : W
⊢ HasFDerivAt
    (fun (v : V) ↦ (↑((𝐞 : (a : ℝ) → Circle) (-(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w)) : ℂ))
    (HSMul.hSMul (β := V →L[ℝ] ℂ)
      (-2 * (↑π : ℂ) * I *
        (↑((𝐞 : (a : ℝ) → Circle) (-(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w)) : ℂ))
      (ofRealCLM.comp (σ₁₂ := RingHom.id ℝ) ((L.flip : (a : W) → V →L[ℝ] ℝ) w)))
    v

Tactic:
hasFDerivAt_fourierChar_neg_bilinear_right L.flip w v

Premises used: ContinuousLinearMap.flip, Real.hasFDerivAt_fourierChar_neg_bilinear_right
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
Goal:
V : Type u_1
W : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : NormedAddCommGroup W
inst_3 : NormedSpace ℝ W
L : ContinuousLinearMap.{0, 0, u_1, u_2} (RingHom.id ℝ) V (W →L[ℝ] ℝ)
v y : V
w : W
simp :
  2 * (↑π : ℂ) * I * (↑((𝐞 : (a : ℝ) → Circle) (-(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w)) : ℂ) *
      (↑((((L : (a : V) → W →L[ℝ] ℝ) y : W →L[ℝ] ℝ) : (a : W) → ℝ) w) : ℂ) =
    2 * (↑π : ℂ) * I * (↑((((L : (a : V) → W →L[ℝ] ℝ) y : W →L[ℝ] ℝ) : (a : W) → ℝ) w) : ℂ) *
      (↑((𝐞 : (a : ℝ) → Circle) (-(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w)) : ℂ)
⊢ (fderiv ℝ
          (fun (v : V) ↦ (↑((𝐞 : (a : ℝ) → Circle) (-(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w)) : ℂ))
          v :
        (a : V) → ℂ)
      y =
    -2 * (↑π : ℂ) * I * (↑((((L : (a : V) → W →L[ℝ] ℝ) y : W →L[ℝ] ℝ) : (a : W) → ℝ) w) : ℂ) *
      (↑((𝐞 : (a : ℝ) → Circle) (-(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w)) : ℂ)

Tactic:
simp only [(hasFDerivAt_fourierChar_neg_bilinear_left L v w).fderiv, neg_mul,
    ContinuousLinearMap.coe_smul', ContinuousLinearMap.coe_comp', Pi.smul_apply,
    Function.comp_apply, ContinuousLinearMap.flip_apply, ofRealCLM_apply, smul_eq_mul, neg_inj]

Premises used: Real.hasFDerivAt_fourierChar_neg_bilinear_left, ContinuousLinearMap.coe_comp', ContinuousLinearMap.coe_smul', ContinuousLinearMap.flip_apply, Complex.ofRealCLM_apply, HasFDerivAt.fderiv, neg_inj, Function.comp_apply, neg_mul, smul_eq_mul, Pi.smul_apply
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
Goal:
V : Type u_1
W : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : NormedAddCommGroup W
inst_3 : NormedSpace ℝ W
L : ContinuousLinearMap.{0, 0, u_1, u_2} (RingHom.id ℝ) V (W →L[ℝ] ℝ)
v y : V
w : W
⊢ 2 * (↑π : ℂ) * I * (↑((𝐞 : (a : ℝ) → Circle) (-(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w)) : ℂ) *
      (↑((((L : (a : V) → W →L[ℝ] ℝ) y : W →L[ℝ] ℝ) : (a : W) → ℝ) w) : ℂ) =
    2 * (↑π : ℂ) * I * (↑((((L : (a : V) → W →L[ℝ] ℝ) y : W →L[ℝ] ℝ) : (a : W) → ℝ) w) : ℂ) *
      (↑((𝐞 : (a : ℝ) → Circle) (-(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w)) : ℂ)

Tactic:
ring
-- Module: Mathlib.Analysis.Fourier.FourierTransformDeriv
Goal:
V : Type u_1
W : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : NormedAddCommGroup W
inst_3 : NormedSpace ℝ W
L : ContinuousLinearMap.{0, 0, u_1, u_2} (RingHom.id ℝ) V (W →L[ℝ] ℝ)
w : W
⊢ Differentiable ℝ (F := ℂ) fun (v : V) ↦
    (↑((𝐞 : (a : ℝ) → Circle) (-(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w)) : ℂ)

Tactic:
fun v ↦ (hasFDerivAt_fourierChar_neg_bilinear_left L v w).differentiableAt

Premises used: Differentiable, Real.hasFDerivAt_fourierChar_neg_bilinear_left, HasFDerivAt.differentiableAt
-- 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
v : V
w : W
⊢ (fourierSMulRight L f v : (a : W) → E) w =
    -(2 * (↑π : ℂ) * I) • HSMul.hSMul (α := ℝ) ((((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w : ℝ) (f v)

Tactic:
rfl

Premises used: rfl
-- 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
v : V
w : W
⊢ HasFDerivAt (𝕜 := ℝ) (F := ℝ) (fun (w' : W) ↦ (((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w')
    ((L : (a : V) → W →L[ℝ] ℝ) v) w

Tactic:
have ha : HasFDerivAt (fun w' : W ↦ L v w') (L v) w := ContinuousLinearMap.hasFDerivAt (L v)
-- 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
v : V
w : W
ha :
  HasFDerivAt (𝕜 := ℝ) (F := ℝ) (fun (w' : W) ↦ (((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w')
    ((L : (a : V) → W →L[ℝ] ℝ) v) w
⊢ HasFDerivAt
    (fun (y : W) ↦
      HSMul.hSMul (α := ℂ)
        (((fun (x : ℝ) ↦ (↑((𝐞 : (a : ℝ) → Circle) x) : ℂ)) ∘
            (-fun (w' : W) ↦ (((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w'))
          y)
        (f v))
    (ContinuousLinearMap.smulRight
      (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ)
        (ContinuousLinearMap.toSpanSingleton ℝ
          (2 * (↑π : ℂ) * I *
            (↑((𝐞 : (a : ℝ) → Circle) (-(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w)) : ℂ)))
        (-(L : (a : V) → W →L[ℝ] ℝ) v))
      (f v))
    w

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

Premises used: HasFDerivAt.smul_const
-- 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
v : V
w : W
ha :
  HasFDerivAt (𝕜 := ℝ) (F := ℝ) (fun (w' : W) ↦ (((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w')
    ((L : (a : V) → W →L[ℝ] ℝ) v) w
h :
  HSMul.hSMul (α := Circle) (β := W →L[ℝ] E)
      ((𝐞 : (a : ℝ) → Circle) (-(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w) : Circle)
      (fourierSMulRight L f v) =
    ContinuousLinearMap.smulRight
      (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ)
        (ContinuousLinearMap.toSpanSingleton ℝ
          (2 * (↑π : ℂ) * I *
            (↑((𝐞 : (a : ℝ) → Circle) (-(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w)) : ℂ)))
        (-(L : (a : V) → W →L[ℝ] ℝ) v))
      (f v)
⊢ HasFDerivAt
    (fun (w' : W) ↦
      HSMul.hSMul (α := Circle)
        ((𝐞 : (a : ℝ) → Circle) (-(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w') : Circle) (f v))
    (HSMul.hSMul (α := Circle) (β := W →L[ℝ] E)
      ((𝐞 : (a : ℝ) → Circle) (-(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w) : Circle)
      (fourierSMulRight L f v))
    w

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

Premises used: HasFDerivAt.smul_const
-- 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
v : V
w : W
ha :
  HasFDerivAt (𝕜 := ℝ) (F := ℝ) (fun (w' : W) ↦ (((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w')
    ((L : (a : V) → W →L[ℝ] ℝ) v) w
h :
  ∀ (w' : W),
    Eq.{u_1 + 1} (α := E)
      ((HSMul.hSMul (α := Circle) (β := W →L[ℝ] E)
              ((𝐞 : (a : ℝ) → Circle) (-(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w) : Circle)
              (fourierSMulRight L f v) :
            (a : W) → E)
          w' :
        E)
      ((ContinuousLinearMap.smulRight
              (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ)
                (ContinuousLinearMap.toSpanSingleton ℝ
                  (2 * (↑π : ℂ) * I *
                    (↑((𝐞 : (a : ℝ) → Circle) (-(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w)) : ℂ)))
                (-(L : (a : V) → W →L[ℝ] ℝ) v))
              (f v) :
            (a : W) → E)
          w' :
        E)
⊢ HSMul.hSMul (α := Circle) (β := W →L[ℝ] E)
      ((𝐞 : (a : ℝ) → Circle) (-(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w) : Circle)
      (fourierSMulRight L f v) =
    ContinuousLinearMap.smulRight
      (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ)
        (ContinuousLinearMap.toSpanSingleton ℝ
          (2 * (↑π : ℂ) * I *
            (↑((𝐞 : (a : ℝ) → Circle) (-(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w)) : ℂ)))
        (-(L : (a : V) → W →L[ℝ] ℝ) v))
      (f v)

Tactic:
ext w' : 1
-- 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
v : V
w : W
ha :
  HasFDerivAt (𝕜 := ℝ) (F := ℝ) (fun (w' : W) ↦ (((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w')
    ((L : (a : V) → W →L[ℝ] ℝ) v) w
w' : W
h :
  HSMul.hSMul (α := Circle)
      ((𝐞 : (a : ℝ) → Circle) (-(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w) : Circle)
      (-(2 * (↑π : ℂ) * I) •
        HSMul.hSMul (α := ℝ) ((((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w' : ℝ) (f v)) =
    HSMul.hSMul (α := ℂ)
      ((ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ)
              (ContinuousLinearMap.toSpanSingleton ℝ
                (2 * (↑π : ℂ) * I *
                  (↑((𝐞 : (a : ℝ) → Circle) (-(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w)) : ℂ)))
              (-(L : (a : V) → W →L[ℝ] ℝ) v) :
            (a : W) → ℂ)
          w' :
        ℂ)
      (f v)
⊢ Eq.{u_1 + 1} (α := E)
    ((HSMul.hSMul (α := Circle) (β := W →L[ℝ] E)
            ((𝐞 : (a : ℝ) → Circle) (-(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w) : Circle)
            (fourierSMulRight L f v) :
          (a : W) → E)
        w' :
      E)
    ((ContinuousLinearMap.smulRight
            (ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ)
              (ContinuousLinearMap.toSpanSingleton ℝ
                (2 * (↑π : ℂ) * I *
                  (↑((𝐞 : (a : ℝ) → Circle) (-(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w)) : ℂ)))
              (-(L : (a : V) → W →L[ℝ] ℝ) v))
            (f v) :
          (a : W) → E)
        w' :
      E)

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

Premises used: VectorFourier.fourierSMulRight, ContinuousLinearMap.smul_apply, ContinuousLinearMap.smulRight_apply
-- 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
v : V
w : W
ha :
  HasFDerivAt (𝕜 := ℝ) (F := ℝ) (fun (w' : W) ↦ (((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w')
    ((L : (a : V) → W →L[ℝ] ℝ) v) w
w' : W
h :
  ((↑((((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w') : ℂ) *
        ((↑((𝐞 : (a : ℝ) → Circle) (-(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w)) : ℂ) *
          -(2 * (↑π : ℂ) * I))) •
      f v =
    ((↑(-(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w') : ℂ) *
        (2 * (↑π : ℂ) * I *
          (↑((𝐞 : (a : ℝ) → Circle) (-(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w)) : ℂ))) •
      f v
⊢ HSMul.hSMul (α := Circle)
      ((𝐞 : (a : ℝ) → Circle) (-(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w) : Circle)
      (-(2 * (↑π : ℂ) * I) •
        HSMul.hSMul (α := ℝ) ((((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w' : ℝ) (f v)) =
    HSMul.hSMul (α := ℂ)
      ((ContinuousLinearMap.comp (σ₁₂ := RingHom.id ℝ)
              (ContinuousLinearMap.toSpanSingleton ℝ
                (2 * (↑π : ℂ) * I *
                  (↑((𝐞 : (a : ℝ) → Circle) (-(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w)) : ℂ)))
              (-(L : (a : V) → W →L[ℝ] ℝ) v) :
            (a : W) → ℂ)
          w' :
        ℂ)
      (f v)

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

Premises used: Complex.real_smul, smul_assoc, ContinuousLinearMap.toSpanSingleton_apply, Submonoid.smul_def, ContinuousLinearMap.neg_apply, smul_eq_mul, SMulCommClass.smul_comm, ContinuousLinearMap.comp_apply
-- 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
v : V
w : W
ha :
  HasFDerivAt (𝕜 := ℝ) (F := ℝ) (fun (w' : W) ↦ (((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w')
    ((L : (a : V) → W →L[ℝ] ℝ) v) w
w' : W
h :
  ((↑((((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w') : ℂ) *
        ((↑((𝐞 : (a : ℝ) → Circle) (-(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w)) : ℂ) *
          -(2 * (↑π : ℂ) * I))) •
      f v =
    (-(↑((((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w') : ℂ) *
        (2 * (↑π : ℂ) * I *
          (↑((𝐞 : (a : ℝ) → Circle) (-(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w)) : ℂ))) •
      f v
⊢ ((↑((((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w') : ℂ) *
        ((↑((𝐞 : (a : ℝ) → Circle) (-(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w)) : ℂ) *
          -(2 * (↑π : ℂ) * I))) •
      f v =
    ((↑(-(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w') : ℂ) *
        (2 * (↑π : ℂ) * I *
          (↑((𝐞 : (a : ℝ) → Circle) (-(((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) : (a : W) → ℝ) w)) : ℂ))) •
      f v

Tactic:
push_cast