-- 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
inst_6 : MeasurableSpace V
inst_7 : BorelSpace V
μ : Measure V
inst_8 : SecondCountableTopology V
N : ℕ∞ω
hf : ∀ (n : ℕ), (↑n : ℕ∞ω) ≤ N → Integrable (ε := ℝ) (fun (v : V) ↦ ‖v‖ ^ n * ‖f v‖) μ
h'f : AEStronglyMeasurable f μ
n : ℕ
hn : (↑n : ℕ∞ω) < N
w : W
I₁ :
  Integrable (ε := ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin n) ↦ W) E)
    (fun (v : V) ↦ fourierPowSMulRight L f v n) μ
I₂ :
  Integrable (ε := ℝ)
    (fun (v : V) ↦
      ‖v‖ *
        Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin n) ↦ W) E)
          (fourierPowSMulRight L f v n))
    μ
I₃ :
  Integrable (ε := ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin (n + 1)) ↦ W) E)
    (fun (v : V) ↦ fourierPowSMulRight L f v (n + 1)) μ
I₄ :
  Integrable (ε := W →L[ℝ] ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin n) ↦ W) E)
    (fun (v : V) ↦ fourierSMulRight L (fun (v : V) ↦ fourierPowSMulRight L f v n) v) μ
w' : W
m : (i : Fin n) → W
⊢ Eq.{u_1 + 1} (α := E)
    (((((curryLeft.{0, u_3, u_1} (𝕜 := ℝ) (Ei := fun (i : Fin (n + 1)) ↦ W) (G := E)
                    (fourierIntegral 𝐞 μ L.toLinearMap₁₂ (fun (v : V) ↦ fourierPowSMulRight L f v (n + 1)) w) :
                  W →L[ℝ] ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin n) ↦ W) E) :
                (a : W) → ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ W) E)
              w' :
            ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin n) ↦ W) E) :
          (a : (i : Fin n) → W) → E)
        m :
      E)
    (((((fourierIntegral 𝐞 μ L.toLinearMap₁₂ (fourierSMulRight L fun (v : V) ↦ fourierPowSMulRight L f v n) w :
                  W →L[ℝ] ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin n) ↦ W) E) :
                (a : W) → ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ W) E)
              w' :
            ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin n) ↦ W) E) :
          (a : (i : Fin n) → W) → E)
        m :
      E)
have h : Eq.{u_1 + 1} (α := E)
  (fourierIntegral 𝐞 μ L.toLinearMap₁₂
    (fun (x : V) ↦
      (fourierPowSMulRight L f x (n + 1) : (a : (i : Fin (n + 1)) → W) → E)
        (Fin.cons (α := fun (i : Fin (n + 1)) ↦ W) w' m))
    w)
  (fourierIntegral 𝐞 μ L.toLinearMap₁₂
    (fun (x : V) ↦
      ((((fourierSMulRight L (fun (v : V) ↦ fourierPowSMulRight L f v n) x :
                  W →L[ℝ] ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin n) ↦ W) E) :
                (a : W) → ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ W) E)
              w' :
            ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin n) ↦ W) E) :
          (a : (i : Fin n) → W) → E)
        m)
    w)
Tactic: rw [curryLeft_apply, fourierIntegral_continuousMultilinearMap_apply' I₃,
        fourierIntegral_continuousLinearMap_apply' I₄,
        fourierIntegral_continuousMultilinearMap_apply' (I₄.apply_continuousLinearMap _)]