awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransformDeriv (hypothesis)
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
    (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
have ha : 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)
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransformDeriv (goal)
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 (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
have 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)
Tactic: convert! ((hasDerivAt_fourierChar (-L v w)).hasFDerivAt.comp w ha.neg).smul_const (f v)
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransformDeriv (goal)
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
⊢ 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)
have 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)
Tactic: ext w' : 1
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransformDeriv (goal)
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
⊢ 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)
have 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)
Tactic: simp_rw [fourierSMulRight, ContinuousLinearMap.smul_apply, ContinuousLinearMap.smulRight_apply]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransformDeriv (goal)
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
⊢ 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)
have 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
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]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransformDeriv (goal)
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
⊢ ((↑((((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
have 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
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransformDeriv (goal)
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
⊢ Norm.norm (E := W →L[ℝ] E) (fourierSMulRight L f v) =
    2 * π * Norm.norm.{u_3} (E := W →L[ℝ] ℝ) ((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) * ‖f v‖
have rw : ‖HSMul.hSMul (β := W →L[ℝ] E) (-(2 * (↑π : ℂ) * I))
      (ContinuousLinearMap.smulRight (S := ℝ) ((L : (a : V) → W →L[ℝ] ℝ) v) (f v))‖ =
  2 * π * Norm.norm.{u_3} (E := W →L[ℝ] ℝ) ((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) * ‖f v‖
Tactic: rw [fourierSMulRight, norm_smul _ (ContinuousLinearMap.smulRight (L v) (f v)),
    norm_neg, norm_mul, norm_mul, norm_I, mul_one, Complex.norm_of_nonneg pi_pos.le,
    Complex.norm_two, ContinuousLinearMap.norm_smulRight_apply, ← mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransformDeriv (goal)
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
rw :
  ‖HSMul.hSMul (β := W →L[ℝ] E) (-(2 * (↑π : ℂ) * I))
        (ContinuousLinearMap.smulRight (S := ℝ) ((L : (a : V) → W →L[ℝ] ℝ) v) (f v))‖ =
    2 * π * Norm.norm.{u_3} (E := W →L[ℝ] ℝ) ((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) * ‖f v‖
⊢ Norm.norm (E := W →L[ℝ] E) (fourierSMulRight L f v) =
    2 * π * Norm.norm.{u_3} (E := W →L[ℝ] ℝ) ((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) * ‖f v‖
have rw₁ : ‖-(2 * (↑π : ℂ) * I)‖ *
    Norm.norm (E := W →L[ℝ] E) (ContinuousLinearMap.smulRight (S := ℝ) ((L : (a : V) → W →L[ℝ] ℝ) v) (f v)) =
  2 * π * Norm.norm.{u_3} (E := W →L[ℝ] ℝ) ((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) * ‖f v‖
Tactic: rw [fourierSMulRight, norm_smul _ (ContinuousLinearMap.smulRight (L v) (f v)),
    norm_neg, norm_mul, norm_mul, norm_I, mul_one, Complex.norm_of_nonneg pi_pos.le,
    Complex.norm_two, ContinuousLinearMap.norm_smulRight_apply, ← mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransformDeriv (goal)
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
rw :
  ‖HSMul.hSMul (β := W →L[ℝ] E) (-(2 * (↑π : ℂ) * I))
        (ContinuousLinearMap.smulRight (S := ℝ) ((L : (a : V) → W →L[ℝ] ℝ) v) (f v))‖ =
    2 * π * Norm.norm.{u_3} (E := W →L[ℝ] ℝ) ((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) * ‖f v‖
rw₁ :
  ‖-(2 * (↑π : ℂ) * I)‖ *
      Norm.norm (E := W →L[ℝ] E) (ContinuousLinearMap.smulRight (S := ℝ) ((L : (a : V) → W →L[ℝ] ℝ) v) (f v)) =
    2 * π * Norm.norm.{u_3} (E := W →L[ℝ] ℝ) ((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) * ‖f v‖
⊢ Norm.norm (E := W →L[ℝ] E) (fourierSMulRight L f v) =
    2 * π * Norm.norm.{u_3} (E := W →L[ℝ] ℝ) ((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) * ‖f v‖
have rw₂ : ‖2 * (↑π : ℂ) * I‖ *
    Norm.norm (E := W →L[ℝ] E) (ContinuousLinearMap.smulRight (S := ℝ) ((L : (a : V) → W →L[ℝ] ℝ) v) (f v)) =
  2 * π * Norm.norm.{u_3} (E := W →L[ℝ] ℝ) ((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) * ‖f v‖
Tactic: rw [fourierSMulRight, norm_smul _ (ContinuousLinearMap.smulRight (L v) (f v)),
    norm_neg, norm_mul, norm_mul, norm_I, mul_one, Complex.norm_of_nonneg pi_pos.le,
    Complex.norm_two, ContinuousLinearMap.norm_smulRight_apply, ← mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransformDeriv (goal)
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
rw :
  ‖HSMul.hSMul (β := W →L[ℝ] E) (-(2 * (↑π : ℂ) * I))
        (ContinuousLinearMap.smulRight (S := ℝ) ((L : (a : V) → W →L[ℝ] ℝ) v) (f v))‖ =
    2 * π * Norm.norm.{u_3} (E := W →L[ℝ] ℝ) ((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) * ‖f v‖
rw₁ :
  ‖-(2 * (↑π : ℂ) * I)‖ *
      Norm.norm (E := W →L[ℝ] E) (ContinuousLinearMap.smulRight (S := ℝ) ((L : (a : V) → W →L[ℝ] ℝ) v) (f v)) =
    2 * π * Norm.norm.{u_3} (E := W →L[ℝ] ℝ) ((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) * ‖f v‖
rw₂ :
  ‖2 * (↑π : ℂ) * I‖ *
      Norm.norm (E := W →L[ℝ] E) (ContinuousLinearMap.smulRight (S := ℝ) ((L : (a : V) → W →L[ℝ] ℝ) v) (f v)) =
    2 * π * Norm.norm.{u_3} (E := W →L[ℝ] ℝ) ((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) * ‖f v‖
⊢ Norm.norm (E := W →L[ℝ] E) (fourierSMulRight L f v) =
    2 * π * Norm.norm.{u_3} (E := W →L[ℝ] ℝ) ((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) * ‖f v‖
have rw₃ : ‖2 * (↑π : ℂ)‖ * ‖I‖ *
    Norm.norm (E := W →L[ℝ] E) (ContinuousLinearMap.smulRight (S := ℝ) ((L : (a : V) → W →L[ℝ] ℝ) v) (f v)) =
  2 * π * Norm.norm.{u_3} (E := W →L[ℝ] ℝ) ((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) * ‖f v‖
Tactic: rw [fourierSMulRight, norm_smul _ (ContinuousLinearMap.smulRight (L v) (f v)),
    norm_neg, norm_mul, norm_mul, norm_I, mul_one, Complex.norm_of_nonneg pi_pos.le,
    Complex.norm_two, ContinuousLinearMap.norm_smulRight_apply, ← mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransformDeriv (goal)
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
rw :
  ‖HSMul.hSMul (β := W →L[ℝ] E) (-(2 * (↑π : ℂ) * I))
        (ContinuousLinearMap.smulRight (S := ℝ) ((L : (a : V) → W →L[ℝ] ℝ) v) (f v))‖ =
    2 * π * Norm.norm.{u_3} (E := W →L[ℝ] ℝ) ((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) * ‖f v‖
rw₁ :
  ‖-(2 * (↑π : ℂ) * I)‖ *
      Norm.norm (E := W →L[ℝ] E) (ContinuousLinearMap.smulRight (S := ℝ) ((L : (a : V) → W →L[ℝ] ℝ) v) (f v)) =
    2 * π * Norm.norm.{u_3} (E := W →L[ℝ] ℝ) ((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) * ‖f v‖
rw₂ :
  ‖2 * (↑π : ℂ) * I‖ *
      Norm.norm (E := W →L[ℝ] E) (ContinuousLinearMap.smulRight (S := ℝ) ((L : (a : V) → W →L[ℝ] ℝ) v) (f v)) =
    2 * π * Norm.norm.{u_3} (E := W →L[ℝ] ℝ) ((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) * ‖f v‖
rw₃ :
  ‖2 * (↑π : ℂ)‖ * ‖I‖ *
      Norm.norm (E := W →L[ℝ] E) (ContinuousLinearMap.smulRight (S := ℝ) ((L : (a : V) → W →L[ℝ] ℝ) v) (f v)) =
    2 * π * Norm.norm.{u_3} (E := W →L[ℝ] ℝ) ((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) * ‖f v‖
⊢ Norm.norm (E := W →L[ℝ] E) (fourierSMulRight L f v) =
    2 * π * Norm.norm.{u_3} (E := W →L[ℝ] ℝ) ((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) * ‖f v‖
have rw₄ : Norm.norm (E := ℂ) 2 * ‖(↑π : ℂ)‖ * ‖I‖ *
    Norm.norm (E := W →L[ℝ] E) (ContinuousLinearMap.smulRight (S := ℝ) ((L : (a : V) → W →L[ℝ] ℝ) v) (f v)) =
  2 * π * Norm.norm.{u_3} (E := W →L[ℝ] ℝ) ((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) * ‖f v‖
Tactic: rw [fourierSMulRight, norm_smul _ (ContinuousLinearMap.smulRight (L v) (f v)),
    norm_neg, norm_mul, norm_mul, norm_I, mul_one, Complex.norm_of_nonneg pi_pos.le,
    Complex.norm_two, ContinuousLinearMap.norm_smulRight_apply, ← mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransformDeriv (goal)
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
rw :
  ‖HSMul.hSMul (β := W →L[ℝ] E) (-(2 * (↑π : ℂ) * I))
        (ContinuousLinearMap.smulRight (S := ℝ) ((L : (a : V) → W →L[ℝ] ℝ) v) (f v))‖ =
    2 * π * Norm.norm.{u_3} (E := W →L[ℝ] ℝ) ((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) * ‖f v‖
rw₁ :
  ‖-(2 * (↑π : ℂ) * I)‖ *
      Norm.norm (E := W →L[ℝ] E) (ContinuousLinearMap.smulRight (S := ℝ) ((L : (a : V) → W →L[ℝ] ℝ) v) (f v)) =
    2 * π * Norm.norm.{u_3} (E := W →L[ℝ] ℝ) ((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) * ‖f v‖
rw₂ :
  ‖2 * (↑π : ℂ) * I‖ *
      Norm.norm (E := W →L[ℝ] E) (ContinuousLinearMap.smulRight (S := ℝ) ((L : (a : V) → W →L[ℝ] ℝ) v) (f v)) =
    2 * π * Norm.norm.{u_3} (E := W →L[ℝ] ℝ) ((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) * ‖f v‖
rw₃ :
  ‖2 * (↑π : ℂ)‖ * ‖I‖ *
      Norm.norm (E := W →L[ℝ] E) (ContinuousLinearMap.smulRight (S := ℝ) ((L : (a : V) → W →L[ℝ] ℝ) v) (f v)) =
    2 * π * Norm.norm.{u_3} (E := W →L[ℝ] ℝ) ((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) * ‖f v‖
rw₄ :
  Norm.norm (E := ℂ) 2 * ‖(↑π : ℂ)‖ * ‖I‖ *
      Norm.norm (E := W →L[ℝ] E) (ContinuousLinearMap.smulRight (S := ℝ) ((L : (a : V) → W →L[ℝ] ℝ) v) (f v)) =
    2 * π * Norm.norm.{u_3} (E := W →L[ℝ] ℝ) ((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) * ‖f v‖
⊢ Norm.norm (E := W →L[ℝ] E) (fourierSMulRight L f v) =
    2 * π * Norm.norm.{u_3} (E := W →L[ℝ] ℝ) ((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) * ‖f v‖
have rw₅ : Norm.norm (E := ℂ) 2 * ‖(↑π : ℂ)‖ * 1 *
    Norm.norm (E := W →L[ℝ] E) (ContinuousLinearMap.smulRight (S := ℝ) ((L : (a : V) → W →L[ℝ] ℝ) v) (f v)) =
  2 * π * Norm.norm.{u_3} (E := W →L[ℝ] ℝ) ((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) * ‖f v‖
Tactic: rw [fourierSMulRight, norm_smul _ (ContinuousLinearMap.smulRight (L v) (f v)),
    norm_neg, norm_mul, norm_mul, norm_I, mul_one, Complex.norm_of_nonneg pi_pos.le,
    Complex.norm_two, ContinuousLinearMap.norm_smulRight_apply, ← mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransformDeriv (goal)
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
rw :
  ‖HSMul.hSMul (β := W →L[ℝ] E) (-(2 * (↑π : ℂ) * I))
        (ContinuousLinearMap.smulRight (S := ℝ) ((L : (a : V) → W →L[ℝ] ℝ) v) (f v))‖ =
    2 * π * Norm.norm.{u_3} (E := W →L[ℝ] ℝ) ((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) * ‖f v‖
rw₁ :
  ‖-(2 * (↑π : ℂ) * I)‖ *
      Norm.norm (E := W →L[ℝ] E) (ContinuousLinearMap.smulRight (S := ℝ) ((L : (a : V) → W →L[ℝ] ℝ) v) (f v)) =
    2 * π * Norm.norm.{u_3} (E := W →L[ℝ] ℝ) ((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) * ‖f v‖
rw₂ :
  ‖2 * (↑π : ℂ) * I‖ *
      Norm.norm (E := W →L[ℝ] E) (ContinuousLinearMap.smulRight (S := ℝ) ((L : (a : V) → W →L[ℝ] ℝ) v) (f v)) =
    2 * π * Norm.norm.{u_3} (E := W →L[ℝ] ℝ) ((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) * ‖f v‖
rw₃ :
  ‖2 * (↑π : ℂ)‖ * ‖I‖ *
      Norm.norm (E := W →L[ℝ] E) (ContinuousLinearMap.smulRight (S := ℝ) ((L : (a : V) → W →L[ℝ] ℝ) v) (f v)) =
    2 * π * Norm.norm.{u_3} (E := W →L[ℝ] ℝ) ((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) * ‖f v‖
rw₄ :
  Norm.norm (E := ℂ) 2 * ‖(↑π : ℂ)‖ * ‖I‖ *
      Norm.norm (E := W →L[ℝ] E) (ContinuousLinearMap.smulRight (S := ℝ) ((L : (a : V) → W →L[ℝ] ℝ) v) (f v)) =
    2 * π * Norm.norm.{u_3} (E := W →L[ℝ] ℝ) ((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) * ‖f v‖
rw₅ :
  Norm.norm (E := ℂ) 2 * ‖(↑π : ℂ)‖ * 1 *
      Norm.norm (E := W →L[ℝ] E) (ContinuousLinearMap.smulRight (S := ℝ) ((L : (a : V) → W →L[ℝ] ℝ) v) (f v)) =
    2 * π * Norm.norm.{u_3} (E := W →L[ℝ] ℝ) ((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) * ‖f v‖
⊢ Norm.norm (E := W →L[ℝ] E) (fourierSMulRight L f v) =
    2 * π * Norm.norm.{u_3} (E := W →L[ℝ] ℝ) ((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) * ‖f v‖
have rw₆ : Norm.norm (E := ℂ) 2 * ‖(↑π : ℂ)‖ *
    Norm.norm (E := W →L[ℝ] E) (ContinuousLinearMap.smulRight (S := ℝ) ((L : (a : V) → W →L[ℝ] ℝ) v) (f v)) =
  2 * π * Norm.norm.{u_3} (E := W →L[ℝ] ℝ) ((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) * ‖f v‖
Tactic: rw [fourierSMulRight, norm_smul _ (ContinuousLinearMap.smulRight (L v) (f v)),
    norm_neg, norm_mul, norm_mul, norm_I, mul_one, Complex.norm_of_nonneg pi_pos.le,
    Complex.norm_two, ContinuousLinearMap.norm_smulRight_apply, ← mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransformDeriv (goal)
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
rw :
  ‖HSMul.hSMul (β := W →L[ℝ] E) (-(2 * (↑π : ℂ) * I))
        (ContinuousLinearMap.smulRight (S := ℝ) ((L : (a : V) → W →L[ℝ] ℝ) v) (f v))‖ =
    2 * π * Norm.norm.{u_3} (E := W →L[ℝ] ℝ) ((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) * ‖f v‖
rw₁ :
  ‖-(2 * (↑π : ℂ) * I)‖ *
      Norm.norm (E := W →L[ℝ] E) (ContinuousLinearMap.smulRight (S := ℝ) ((L : (a : V) → W →L[ℝ] ℝ) v) (f v)) =
    2 * π * Norm.norm.{u_3} (E := W →L[ℝ] ℝ) ((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) * ‖f v‖
rw₂ :
  ‖2 * (↑π : ℂ) * I‖ *
      Norm.norm (E := W →L[ℝ] E) (ContinuousLinearMap.smulRight (S := ℝ) ((L : (a : V) → W →L[ℝ] ℝ) v) (f v)) =
    2 * π * Norm.norm.{u_3} (E := W →L[ℝ] ℝ) ((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) * ‖f v‖
rw₃ :
  ‖2 * (↑π : ℂ)‖ * ‖I‖ *
      Norm.norm (E := W →L[ℝ] E) (ContinuousLinearMap.smulRight (S := ℝ) ((L : (a : V) → W →L[ℝ] ℝ) v) (f v)) =
    2 * π * Norm.norm.{u_3} (E := W →L[ℝ] ℝ) ((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) * ‖f v‖
rw₄ :
  Norm.norm (E := ℂ) 2 * ‖(↑π : ℂ)‖ * ‖I‖ *
      Norm.norm (E := W →L[ℝ] E) (ContinuousLinearMap.smulRight (S := ℝ) ((L : (a : V) → W →L[ℝ] ℝ) v) (f v)) =
    2 * π * Norm.norm.{u_3} (E := W →L[ℝ] ℝ) ((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) * ‖f v‖
rw₅ :
  Norm.norm (E := ℂ) 2 * ‖(↑π : ℂ)‖ * 1 *
      Norm.norm (E := W →L[ℝ] E) (ContinuousLinearMap.smulRight (S := ℝ) ((L : (a : V) → W →L[ℝ] ℝ) v) (f v)) =
    2 * π * Norm.norm.{u_3} (E := W →L[ℝ] ℝ) ((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) * ‖f v‖
rw₆ :
  Norm.norm (E := ℂ) 2 * ‖(↑π : ℂ)‖ *
      Norm.norm (E := W →L[ℝ] E) (ContinuousLinearMap.smulRight (S := ℝ) ((L : (a : V) → W →L[ℝ] ℝ) v) (f v)) =
    2 * π * Norm.norm.{u_3} (E := W →L[ℝ] ℝ) ((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) * ‖f v‖
⊢ Norm.norm (E := W →L[ℝ] E) (fourierSMulRight L f v) =
    2 * π * Norm.norm.{u_3} (E := W →L[ℝ] ℝ) ((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) * ‖f v‖
have rw₇ : Norm.norm (E := ℂ) 2 * π *
    Norm.norm (E := W →L[ℝ] E) (ContinuousLinearMap.smulRight (S := ℝ) ((L : (a : V) → W →L[ℝ] ℝ) v) (f v)) =
  2 * π * Norm.norm.{u_3} (E := W →L[ℝ] ℝ) ((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) * ‖f v‖
Tactic: rw [fourierSMulRight, norm_smul _ (ContinuousLinearMap.smulRight (L v) (f v)),
    norm_neg, norm_mul, norm_mul, norm_I, mul_one, Complex.norm_of_nonneg pi_pos.le,
    Complex.norm_two, ContinuousLinearMap.norm_smulRight_apply, ← mul_assoc]