-- 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‖
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‖
rw₈ :
  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‖
rw₉ :
  2 * π * (Norm.norm.{u_3} (E := StrongDual ℝ W) ((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) * ‖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 * π * Norm.norm.{u_3} (E := StrongDual ℝ W) ((L : (a : V) → W →L[ℝ] ℝ) v : W →L[ℝ] ℝ) * ‖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]