-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransform (goal)
Goal:
𝕜 : Type u_1
inst : CommRing 𝕜
V : Type u_2
inst_1 : AddCommGroup V
inst_2 : Module 𝕜 V
inst_3 : MeasurableSpace V
W : Type u_3
inst_4 : AddCommGroup W
inst_5 : Module 𝕜 W
E : Type u_4
inst_6 : NormedAddCommGroup E
inst_7 : NormedSpace ℂ E
inst_8 : MeasurableAdd V
e : AddChar 𝕜 𝕊
μ : Measure V
inst_9 : μ.IsAddRightInvariant
L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜
f : V → E
v₀ : V
w : W
v : V
h :
  HSMul.hSMul (α := ℂ) (↑((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) (v - v₀) : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) w)) : ℂ)
      (f v) =
    HSMul.hSMul (α := ℂ) (β := ℂ)
        (↑((e : (a : 𝕜) → 𝕊) ((((L : (a : V) → W →ₗ[𝕜] 𝕜) v₀ : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) w)) : ℂ)
        (↑((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) v : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) w)) : ℂ) •
      f v
h₁ :
  HSMul.hSMul (α := ℂ) (↑((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) (v - v₀) : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) w)) : ℂ)
      (f v) =
    HMul.hMul (α := ℂ) (↑((e : (a : 𝕜) → 𝕊) ((((L : (a : V) → W →ₗ[𝕜] 𝕜) v₀ : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) w)) : ℂ)
        (↑((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) v : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) w)) : ℂ) •
      f v
h₂ :
  HSMul.hSMul (α := ℂ) (↑((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) (v - v₀) : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) w)) : ℂ)
      (f v) =
    (↑(HMul.hMul (α := 𝕊) (β := 𝕊)
            ((e : (a : 𝕜) → 𝕊) ((((L : (a : V) → W →ₗ[𝕜] 𝕜) v₀ : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) w) : 𝕊)
            ((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) v : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) w) : 𝕊)) :
        ℂ) •
      f v
h₃ :
  HSMul.hSMul (α := ℂ) (↑((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) (v - v₀) : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) w)) : ℂ)
      (f v) =
    HSMul.hSMul (α := ℂ)
      (↑((e : (a : 𝕜) → 𝕊)
            (HAdd.hAdd (α := 𝕜) (β := 𝕜) ((((L : (a : V) → W →ₗ[𝕜] 𝕜) v₀ : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) w : 𝕜)
              (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) v : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) w : 𝕜))) :
        ℂ)
      (f v)
h₄ :
  HSMul.hSMul (α := ℂ) (↑((e : (a : 𝕜) → 𝕊) (((-(L : (a : V) → W →ₗ[𝕜] 𝕜) (v - v₀) : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) w)) : ℂ)
      (f v) =
    HSMul.hSMul (α := ℂ)
      (↑((e : (a : 𝕜) → 𝕊)
            (HAdd.hAdd (α := 𝕜) (β := 𝕜) ((((L : (a : V) → W →ₗ[𝕜] 𝕜) v₀ : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) w : 𝕜)
              (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) v : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) w : 𝕜))) :
        ℂ)
      (f v)
h₅ :
  HSMul.hSMul (α := ℂ) (↑((e : (a : 𝕜) → 𝕊) (((-(L : (a : V) → W →ₗ[𝕜] 𝕜) (v - v₀) : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) w)) : ℂ)
      (f v) =
    HSMul.hSMul (α := ℂ)
      (↑((e : (a : 𝕜) → 𝕊)
            (HSub.hSub (α := 𝕜) (β := 𝕜) ((((L : (a : V) → W →ₗ[𝕜] 𝕜) v₀ : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) w : 𝕜)
              ((((L : (a : V) → W →ₗ[𝕜] 𝕜) v : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) w : 𝕜))) :
        ℂ)
      (f v)
h₆ :
  HSMul.hSMul (α := ℂ) (↑((e : (a : 𝕜) → 𝕊) (((-(L : (a : V) → W →ₗ[𝕜] 𝕜) (v - v₀) : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) w)) : ℂ)
      (f v) =
    HSMul.hSMul (α := ℂ)
      (↑((e : (a : 𝕜) → 𝕊)
            ((HSub.hSub (α := W →ₗ[𝕜] 𝕜) (β := W →ₗ[𝕜] 𝕜) ((L : (a : V) → W →ₗ[𝕜] 𝕜) v₀ : W →ₗ[𝕜] 𝕜)
                  ((L : (a : V) → W →ₗ[𝕜] 𝕜) v : W →ₗ[𝕜] 𝕜) :
                (a : W) → 𝕜)
              w)) :
        ℂ)
      (f v)
⊢ HSMul.hSMul (α := ℂ) (↑((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) (v - v₀) : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) w)) : ℂ)
      (f v) =
    HSMul.hSMul (α := ℂ) (↑((e : (a : 𝕜) → 𝕊) ((((L : (a : V) → W →ₗ[𝕜] 𝕜) v₀ : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) w)) : ℂ)
      (HSMul.hSMul (α := ℂ) (↑((e : (a : 𝕜) → 𝕊) (-(((L : (a : V) → W →ₗ[𝕜] 𝕜) v : W →ₗ[𝕜] 𝕜) : (a : W) → 𝕜) w)) : ℂ)
        (f v))
have h₇ : HSMul.hSMul (α := ℂ)
    (↑((e : (a : 𝕜) → 𝕊)
          ((-HSub.hSub (α := W →ₗ[𝕜] 𝕜) (β := W →ₗ[𝕜] 𝕜) ((L : (a : V) → W →ₗ[𝕜] 𝕜) v : W →ₗ[𝕜] 𝕜)
                  ((L : (a : V) → W →ₗ[𝕜] 𝕜) v₀ : W →ₗ[𝕜] 𝕜) :
              (a : W) → 𝕜)
            w)) :
      ℂ)
    (f v) =
  HSMul.hSMul (α := ℂ)
    (↑((e : (a : 𝕜) → 𝕊)
          ((HSub.hSub (α := W →ₗ[𝕜] 𝕜) (β := W →ₗ[𝕜] 𝕜) ((L : (a : V) → W →ₗ[𝕜] 𝕜) v₀ : W →ₗ[𝕜] 𝕜)
                ((L : (a : V) → W →ₗ[𝕜] 𝕜) v : W →ₗ[𝕜] 𝕜) :
              (a : W) → 𝕜)
            w)) :
      ℂ)
    (f v)
Tactic: rw [← smul_assoc, smul_eq_mul, ← Circle.coe_mul, ← e.map_add_eq_mul, ← LinearMap.neg_apply,
    ← sub_eq_add_neg, ← LinearMap.sub_apply, map_sub, neg_sub]