-- 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:
case succ.h.H
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)) μ
⊢ ((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 ∂μ

Tactic:
have h'n : n < N := (Nat.cast_lt.mpr n.lt_succ_self).trans_le hn

Result:
case succ.h.H
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'n : ↑n < N
⊢ ((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 ∂μ

Proof state:
case succ.h.H.e_a
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'n : ↑n < N
⊢ 2 * ↑π * I * (↑((L (m 0)) w) * ((-(2 * ↑π * I)) ^ n * ∏ x : Fin n, -↑((L (m x.succ)) w))) =
    (-(2 * ↑π * I)) ^ n * (2 * ↑π * I) * (↑((L (m 0)) w) * ∏ x : Fin n, -↑((L (m x.succ)) w))

Tactic:
ring

Result:
no goals

Proof state:
case succ.h.H
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
⊢ (fourierIntegral 𝐞 μ L.toLinearMap₂ (iteratedFDeriv ℝ (n + 1) f) w) m =
    (fourierPowSMulRight (-L.flip) (fourierIntegral 𝐞 μ L.toLinearMap₂ f) w (n + 1)) m

Tactic:
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

Result:
case succ.h.H
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)) μ
⊢ (fourierIntegral 𝐞 μ L.toLinearMap₂ (iteratedFDeriv ℝ (n + 1) f) w) m =
    (fourierPowSMulRight (-L.flip) (fourierIntegral 𝐞 μ L.toLinearMap₂ f) w (n + 1)) m

Proof state:
case succ.h.H
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'n : ↑n < N
⊢ ((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 ∂μ

Tactic:
rw [fourierIntegral_fderiv _ (h'f n h'n.le)
  (hf.differentiable_iteratedFDeriv (mod_cast h'n)) J]

Result:
case succ.h.H
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'n : ↑n < N
⊢ ((fourierSMulRight (-L.flip) (fourierIntegral 𝐞 μ L.toLinearMap₂ (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 ∂μ