-- Mathlib/Analysis/Fourier/FourierTransformDeriv.lean
theorem fourierIntegral_iteratedFDeriv [FiniteDimensional ℝ V]
    {μ : Measure V} [Measure.IsAddHaarMeasure μ] {N : ℕ∞} (hf : ContDiff ℝ N f)
    (h'f : ∀ (n : ℕ), n ≤ N → Integrable (iteratedFDeriv ℝ n f) μ) {n : ℕ} (hn : n ≤ N) :
    fourierIntegral 𝐞 μ L.toLinearMap₂ (iteratedFDeriv ℝ n f)
      = (fun w ↦ fourierPowSMulRight (-L.flip) (fourierIntegral 𝐞 μ L.toLinearMap₂ f) w n)

Proof state:
E : Type u_1
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : NormedSpace ℝ V
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : NormedSpace ℝ W
L : V →L[ℝ] W →L[ℝ] ℝ
f : V → E
inst✝³ : MeasurableSpace V
inst✝² : BorelSpace V
inst✝¹ : FiniteDimensional ℝ V
μ : Measure V
inst✝ : μ.IsAddHaarMeasure
N : ℕ∞
hf : ContDiff ℝ (↑N) f
h'f : ∀ (n : ℕ), ↑n ≤ N → Integrable (iteratedFDeriv ℝ n f) μ
n : ℕ
hn : ↑n ≤ N
⊢ fourierIntegral 𝐞 μ L.toLinearMap₂ (iteratedFDeriv ℝ n f) = fun w =>
    fourierPowSMulRight (-L.flip) (fourierIntegral 𝐞 μ L.toLinearMap₂ f) w n

Tactic:
induction n with
| zero =>
  ext w m
  simp only [iteratedFDeriv_zero_apply, fourierPowSMulRight_apply, pow_zero,
    Finset.univ_eq_empty, ContinuousLinearMap.neg_apply, ContinuousLinearMap.flip_apply,
    Finset.prod_empty, one_smul, fourierIntegral_continuousMultilinearMap_apply' ((h'f 0 bot_le))]
| succ n ih =>
  ext w m
  have J : Integrable (fderiv ℝ (iteratedFDeriv ℝ n f)) μ := by
    specialize h'f (n + 1) hn
    rwa [iteratedFDeriv_succ_eq_comp_left, Function.comp_def,
        LinearIsometryEquiv.integrable_comp_iff (𝕜 := ℝ) (φ := fderiv ℝ (iteratedFDeriv ℝ n f))]
      at h'f
  suffices H : (fourierIntegral 𝐞 μ L.toLinearMap₂ (fderiv ℝ (iteratedFDeriv ℝ n f)) w)
        (m 0) (Fin.tail m) =
      (-(2 * π * I)) ^ (n + 1) • (∏ x : Fin (n + 1), -L (m x) w) • ∫ v, 𝐞 (-L v w) • f v ∂μ by
    rw [fourierIntegral_continuousMultilinearMap_apply' (h'f _ hn)]
    simp only [iteratedFDeriv_succ_apply_left, fourierPowSMulRight_apply,
      ContinuousLinearMap.neg_apply, ContinuousLinearMap.flip_apply]
    rw [← fourierIntegral_continuousMultilinearMap_apply' ((J.apply_continuousLinearMap _)),
        ← fourierIntegral_continuousLinearMap_apply' J]
    exact H
  have h'n : n < N := (Nat.cast_lt.mpr n.lt_succ_self).trans_le hn
  rw [fourierIntegral_fderiv _ (h'f n h'n.le)
    (hf.differentiable_iteratedFDeriv (mod_cast h'n)) J]
  simp only [ih h'n.le, fourierSMulRight_apply, ContinuousLinearMap.neg_apply,
    ContinuousLinearMap.flip_apply, neg_smul, smul_neg, neg_neg, smul_apply,
    fourierPowSMulRight_apply, ← coe_smul (E := E), smul_smul]
  congr 1
  simp only [ofReal_prod, ofReal_neg, pow_succ, mul_neg, Fin.prod_univ_succ, neg_mul,
    ofReal_mul, neg_neg, Fin.tail_def]
  ring

Result:
no goals

Proof state:
E : Type u_1
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : NormedSpace ℝ V
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : NormedSpace ℝ W
L : V →L[ℝ] W →L[ℝ] ℝ
f : V → E
inst✝³ : MeasurableSpace V
inst✝² : BorelSpace V
inst✝¹ : FiniteDimensional ℝ V
μ : Measure V
inst✝ : μ.IsAddHaarMeasure
N : ℕ∞
hf : ContDiff ℝ (↑N) f
h'f : ∀ (n : ℕ), ↑n ≤ N → Integrable (iteratedFDeriv ℝ n f) μ
n : ℕ
ih :
  ↑n ≤ N →
    fourierIntegral 𝐞 μ L.toLinearMap₂ (iteratedFDeriv ℝ n f) = fun w =>
      fourierPowSMulRight (-L.flip) (fourierIntegral 𝐞 μ L.toLinearMap₂ f) w n
hn : ↑(n + 1) ≤ N
w : W
m : Fin (n + 1) → V
⊢ Integrable (fderiv ℝ (iteratedFDeriv ℝ n f)) μ

Tactic:
specialize h'f (n + 1) hn

Result:
E : Type u_1
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : NormedSpace ℝ V
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : NormedSpace ℝ W
L : V →L[ℝ] W →L[ℝ] ℝ
f : V → E
inst✝³ : MeasurableSpace V
inst✝² : BorelSpace V
inst✝¹ : FiniteDimensional ℝ V
μ : Measure V
inst✝ : μ.IsAddHaarMeasure
N : ℕ∞
hf : ContDiff ℝ (↑N) f
n : ℕ
ih :
  ↑n ≤ N →
    fourierIntegral 𝐞 μ L.toLinearMap₂ (iteratedFDeriv ℝ n f) = fun w =>
      fourierPowSMulRight (-L.flip) (fourierIntegral 𝐞 μ L.toLinearMap₂ f) w n
hn : ↑(n + 1) ≤ N
w : W
m : Fin (n + 1) → V
h'f : Integrable (iteratedFDeriv ℝ (n + 1) f) μ
⊢ Integrable (fderiv ℝ (iteratedFDeriv ℝ n f)) μ

Proof state:
E : Type u_1
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : NormedSpace ℝ V
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : NormedSpace ℝ W
L : V →L[ℝ] W →L[ℝ] ℝ
f : V → E
inst✝³ : MeasurableSpace V
inst✝² : BorelSpace V
inst✝¹ : FiniteDimensional ℝ V
μ : Measure V
inst✝ : μ.IsAddHaarMeasure
N : ℕ∞
hf : ContDiff ℝ (↑N) f
h'f : ∀ (n : ℕ), ↑n ≤ N → Integrable (iteratedFDeriv ℝ n f) μ
n : ℕ
ih :
  ↑n ≤ N →
    fourierIntegral 𝐞 μ L.toLinearMap₂ (iteratedFDeriv ℝ n f) = fun w =>
      fourierPowSMulRight (-L.flip) (fourierIntegral 𝐞 μ L.toLinearMap₂ f) w n
hn : ↑(n + 1) ≤ N
w : W
m : Fin (n + 1) → V
J : Integrable (fderiv ℝ (iteratedFDeriv ℝ n f)) μ
H :
  ((fourierIntegral 𝐞 μ L.toLinearMap₂ (fderiv ℝ (iteratedFDeriv ℝ n f)) w) (m 0)) (Fin.tail m) =
    (-(2 * ↑π * I)) ^ (n + 1) • (∏ x : Fin (n + 1), -(L (m x)) w) • ∫ (v : V), 𝐞 (-(L v) w) • f v ∂μ
⊢ fourierIntegral 𝐞 μ L.toLinearMap₂ (fun x => ((fderiv ℝ (iteratedFDeriv ℝ n f) x) (m 0)) (Fin.tail m)) w =
    (-(2 * ↑π * I)) ^ (n + 1) • (∏ x : Fin (n + 1), -(L (m x)) w) • fourierIntegral 𝐞 μ L.toLinearMap₂ f w

Tactic:
rw [← fourierIntegral_continuousMultilinearMap_apply' ((J.apply_continuousLinearMap _)),
    ← fourierIntegral_continuousLinearMap_apply' J]

Result:
E : Type u_1
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℂ E
V : Type u_2
W : Type u_3
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : NormedSpace ℝ V
inst✝⁵ : NormedAddCommGroup W
inst✝⁴ : NormedSpace ℝ W
L : V →L[ℝ] W →L[ℝ] ℝ
f : V → E
inst✝³ : MeasurableSpace V
inst✝² : BorelSpace V
inst✝¹ : FiniteDimensional ℝ V
μ : Measure V
inst✝ : μ.IsAddHaarMeasure
N : ℕ∞
hf : ContDiff ℝ (↑N) f
h'f : ∀ (n : ℕ), ↑n ≤ N → Integrable (iteratedFDeriv ℝ n f) μ
n : ℕ
ih :
  ↑n ≤ N →
    fourierIntegral 𝐞 μ L.toLinearMap₂ (iteratedFDeriv ℝ n f) = fun w =>
      fourierPowSMulRight (-L.flip) (fourierIntegral 𝐞 μ L.toLinearMap₂ f) w n
hn : ↑(n + 1) ≤ N
w : W
m : Fin (n + 1) → V
J : Integrable (fderiv ℝ (iteratedFDeriv ℝ n f)) μ
H :
  ((fourierIntegral 𝐞 μ L.toLinearMap₂ (fderiv ℝ (iteratedFDeriv ℝ n f)) w) (m 0)) (Fin.tail m) =
    (-(2 * ↑π * I)) ^ (n + 1) • (∏ x : Fin (n + 1), -(L (m x)) w) • ∫ (v : V), 𝐞 (-(L v) w) • f v ∂μ
⊢ ((fourierIntegral 𝐞 μ L.toLinearMap₂ (fderiv ℝ (iteratedFDeriv ℝ n f)) w) (m 0)) (Fin.tail m) =
    (-(2 * ↑π * I)) ^ (n + 1) • (∏ x : Fin (n + 1), -(L (m x)) w) • fourierIntegral 𝐞 μ L.toLinearMap₂ f w