-- Mathlib/Analysis/Fourier/FourierTransformDeriv.lean
lemma hasFTaylorSeriesUpTo_fourierIntegral {N : WithTop ℕ∞}
    (hf : ∀ (n : ℕ), n ≤ N → Integrable (fun v ↦ ‖v‖^n * ‖f v‖) μ)
    (h'f : AEStronglyMeasurable f μ) :
    HasFTaylorSeriesUpTo N (fourierIntegral 𝐞 μ L.toLinearMap₂ f)
      (fun w n ↦ fourierIntegral 𝐞 μ L.toLinearMap₂ (fun v ↦ fourierPowSMulRight L f v n) w)

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
μ : Measure V
inst✝ : SecondCountableTopology V
N : WithTop ℕ∞
hf : ∀ (n : ℕ), ↑n ≤ N → Integrable (fun v => ‖v‖ ^ n * ‖f v‖) μ
h'f : AEStronglyMeasurable f μ
n : ℕ
hn : ↑n < N
w : W
I₁ : Integrable (fun v => fourierPowSMulRight L f v n) μ
v : V
⊢ ‖v‖ * ‖fourierPowSMulRight L f v n‖ ≤ ‖v‖ * ((2 * π * ‖L‖) ^ n * ‖v‖ ^ n * ‖f v‖)

Tactic:
gcongr

Result:
case 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
μ : Measure V
inst✝ : SecondCountableTopology V
N : WithTop ℕ∞
hf : ∀ (n : ℕ), ↑n ≤ N → Integrable (fun v => ‖v‖ ^ n * ‖f v‖) μ
h'f : AEStronglyMeasurable f μ
n : ℕ
hn : ↑n < N
w : W
I₁ : Integrable (fun v => fourierPowSMulRight L f v n) μ
v : V
⊢ ‖fourierPowSMulRight L f v n‖ ≤ (2 * π * ‖L‖) ^ n * ‖v‖ ^ n * ‖f v‖

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
μ : Measure V
inst✝ : SecondCountableTopology V
N : WithTop ℕ∞
hf : ∀ (n : ℕ), ↑n ≤ N → Integrable (fun v => ‖v‖ ^ n * ‖f v‖) μ
h'f : AEStronglyMeasurable f μ
n : ℕ
hn : ↑n < N
w : W
I₁ : Integrable (fun v => fourierPowSMulRight L f v n) μ
I₂ : Integrable (fun v => ‖v‖ * ‖fourierPowSMulRight L f v n‖) μ
I₃ : Integrable (fun v => fourierPowSMulRight L f v (n + 1)) μ
I₄ : Integrable (fun v => fourierSMulRight L (fun v => fourierPowSMulRight L f v n) v) μ
⊢ (fourierIntegral 𝐞 μ L.toLinearMap₂ (fun v => fourierPowSMulRight L f v (n + 1)) w).curryLeft =
    fourierIntegral 𝐞 μ L.toLinearMap₂ (fourierSMulRight L fun v => fourierPowSMulRight L f v n) w

Tactic:
ext w' m

Result:
case 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
μ : Measure V
inst✝ : SecondCountableTopology V
N : WithTop ℕ∞
hf : ∀ (n : ℕ), ↑n ≤ N → Integrable (fun v => ‖v‖ ^ n * ‖f v‖) μ
h'f : AEStronglyMeasurable f μ
n : ℕ
hn : ↑n < N
w : W
I₁ : Integrable (fun v => fourierPowSMulRight L f v n) μ
I₂ : Integrable (fun v => ‖v‖ * ‖fourierPowSMulRight L f v n‖) μ
I₃ : Integrable (fun v => fourierPowSMulRight L f v (n + 1)) μ
I₄ : Integrable (fun v => fourierSMulRight L (fun v => fourierPowSMulRight L f v n) v) μ
w' : W
m : Fin n → W
⊢ ((fourierIntegral 𝐞 μ L.toLinearMap₂ (fun v => fourierPowSMulRight L f v (n + 1)) w).curryLeft w') m =
    ((fourierIntegral 𝐞 μ L.toLinearMap₂ (fourierSMulRight L fun v => fourierPowSMulRight L f v n) w) w') m

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
μ : Measure V
inst✝ : SecondCountableTopology V
N : WithTop ℕ∞
hf : ∀ (n : ℕ), ↑n ≤ N → Integrable (fun v => ‖v‖ ^ n * ‖f v‖) μ
h'f : AEStronglyMeasurable f μ
n : ℕ
hn : ↑n ≤ N
⊢ Continuous fun p => (L.toLinearMap₂ p.1) p.2

Tactic:
apply L.continuous₂

Result:
no goals

Proof state:
case fderiv
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
μ : Measure V
inst✝ : SecondCountableTopology V
N : WithTop ℕ∞
hf : ∀ (n : ℕ), ↑n ≤ N → Integrable (fun v => ‖v‖ ^ n * ‖f v‖) μ
h'f : AEStronglyMeasurable f μ
n : ℕ
hn : ↑n < N
w : W
I₁ : Integrable (fun v => fourierPowSMulRight L f v n) μ
I₂ : Integrable (fun v => ‖v‖ * ‖fourierPowSMulRight L f v n‖) μ
I₃ : Integrable (fun v => fourierPowSMulRight L f v (n + 1)) μ
I₄ : Integrable (fun v => fourierSMulRight L (fun v => fourierPowSMulRight L f v n) v) μ
⊢ HasFDerivAt (fun y => fourierIntegral 𝐞 μ L.toLinearMap₂ (fun v => fourierPowSMulRight L f v n) y)
    (fourierIntegral 𝐞 μ L.toLinearMap₂ (fun v => fourierPowSMulRight L f v n.succ) w).curryLeft w

Tactic:
have E : curryLeft
      (fourierIntegral 𝐞 μ L.toLinearMap₂ (fun v ↦ fourierPowSMulRight L f v (n + 1)) w) =
    fourierIntegral 𝐞 μ L.toLinearMap₂
      (fourierSMulRight L fun v ↦ fourierPowSMulRight L f v n) w := by
  ext w' m
  rw [curryLeft_apply, fourierIntegral_continuousMultilinearMap_apply' I₃,
    fourierIntegral_continuousLinearMap_apply' I₄,
    fourierIntegral_continuousMultilinearMap_apply' (I₄.apply_continuousLinearMap _)]
  congr with v
  simp only [fourierPowSMulRight_apply, mul_comm, pow_succ, neg_mul, Fin.prod_univ_succ,
    Fin.cons_zero, Fin.cons_succ, neg_smul, fourierSMulRight_apply, neg_apply, smul_apply,
    smul_comm (M := ℝ) (N := ℂ) (α := E), smul_smul]

Result:
case fderiv
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
μ : Measure V
inst✝ : SecondCountableTopology V
N : WithTop ℕ∞
hf : ∀ (n : ℕ), ↑n ≤ N → Integrable (fun v => ‖v‖ ^ n * ‖f v‖) μ
h'f : AEStronglyMeasurable f μ
n : ℕ
hn : ↑n < N
w : W
I₁ : Integrable (fun v => fourierPowSMulRight L f v n) μ
I₂ : Integrable (fun v => ‖v‖ * ‖fourierPowSMulRight L f v n‖) μ
I₃ : Integrable (fun v => fourierPowSMulRight L f v (n + 1)) μ
I₄ : Integrable (fun v => fourierSMulRight L (fun v => fourierPowSMulRight L f v n) v) μ
E :
  (fourierIntegral 𝐞 μ L.toLinearMap₂ (fun v => fourierPowSMulRight L f v (n + 1)) w).curryLeft =
    fourierIntegral 𝐞 μ L.toLinearMap₂ (fourierSMulRight L fun v => fourierPowSMulRight L f v n) w
⊢ HasFDerivAt (fun y => fourierIntegral 𝐞 μ L.toLinearMap₂ (fun v => fourierPowSMulRight L f v n) y)
    (fourierIntegral 𝐞 μ L.toLinearMap₂ (fun v => fourierPowSMulRight L f v n.succ) w).curryLeft w