awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransformDeriv (hypothesis)
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))
    μ
⊢ HasFDerivAt (𝕜 := ℝ) (F := ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin n) ↦ W) E)
    (fun (y : W) ↦ fourierIntegral 𝐞 μ L.toLinearMap₁₂ (fun (v : V) ↦ fourierPowSMulRight L f v n) y)
    (curryLeft.{0, u_3, u_1} (𝕜 := ℝ) (Ei := fun (i : Fin n.succ) ↦ W) (G := E)
      (fourierIntegral 𝐞 μ L.toLinearMap₁₂ (fun (v : V) ↦ fourierPowSMulRight L f v n.succ) w))
    w
have 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)) μ
Tactic: have I₃ : Integrable (fun v ↦ fourierPowSMulRight L f v (n + 1)) μ :=
      integrable_fourierPowSMulRight L (hf (n + 1) (ENat.add_one_natCast_le_withTop_of_lt hn)) h'f
-- 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)) μ
⊢ 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) μ
have apply : ∀ᵐ (a : V) ∂μ,
  Norm.norm (E := W →L[ℝ] ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin n) ↦ W) E)
      (fourierSMulRight L (fun (v : V) ↦ fourierPowSMulRight L f v n) a) ≤
    2 * π * ‖L‖ *
      (‖a‖ *
        Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin n) ↦ W) E)
          (fourierPowSMulRight L f a n))
Tactic: apply (I₂.const_mul ((2 * π * ‖L‖))).mono' (h'f.fourierPowSMulRight L n).fourierSMulRight
-- 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)) μ
⊢ ∀ᵐ (a : V) ∂μ,
    Norm.norm (E := W →L[ℝ] ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin n) ↦ W) E)
        (fourierSMulRight L (fun (v : V) ↦ fourierPowSMulRight L f v n) a) ≤
      2 * π * ‖L‖ *
        (‖a‖ *
          Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin n) ↦ W) E)
            (fourierPowSMulRight L f a n))
have h : ∀ (v : V),
  Norm.norm (E := W →L[ℝ] ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin n) ↦ W) E)
      (fourierSMulRight L (fun (v : V) ↦ fourierPowSMulRight L f v n) v) ≤
    2 * π * ‖L‖ *
      (‖v‖ *
        Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin n) ↦ W) E)
          (fourierPowSMulRight L f v n))
Tactic: filter_upwards with v
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransformDeriv (hypothesis)
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)) μ
⊢ HasFDerivAt (𝕜 := ℝ) (F := ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin n) ↦ W) E)
    (fun (y : W) ↦ fourierIntegral 𝐞 μ L.toLinearMap₁₂ (fun (v : V) ↦ fourierPowSMulRight L f v n) y)
    (curryLeft.{0, u_3, u_1} (𝕜 := ℝ) (Ei := fun (i : Fin n.succ) ↦ W) (G := E)
      (fourierIntegral 𝐞 μ L.toLinearMap₁₂ (fun (v : V) ↦ fourierPowSMulRight L f v n.succ) w))
    w
have 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) μ
Tactic: have I₄ : Integrable
        (fun v ↦ fourierSMulRight L (fun v ↦ fourierPowSMulRight L f v n) v) μ := by
      apply (I₂.const_mul ((2 * π * ‖L‖))).mono' (h'f.fourierPowSMulRight L n).fourierSMulRight
      filter_upwards with v
      exact (norm_fourierSMulRight_le _ _ _).trans (le_of_eq (by ring))
-- 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) μ
⊢ Eq (α := W →L[ℝ] ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin n) ↦ W) 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)
    (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)
have h : ∀ (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)
Tactic: ext w' m
-- 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)
    (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)
have h : ∀ (v : V),
  Eq.{u_1 + 1} (α := E)
    ((fourierPowSMulRight L f v (n + 1) : (a : (i : Fin (n + 1)) → W) → E)
        (Fin.cons (α := fun (i : Fin (n + 1)) ↦ W) w' m) :
      E)
    (((((fourierSMulRight L (fun (v : V) ↦ fourierPowSMulRight L f v n) v :
                  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)
Tactic: congr with v
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransformDeriv (hypothesis)
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) μ
⊢ HasFDerivAt (𝕜 := ℝ) (F := ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin n) ↦ W) E)
    (fun (y : W) ↦ fourierIntegral 𝐞 μ L.toLinearMap₁₂ (fun (v : V) ↦ fourierPowSMulRight L f v n) y)
    (curryLeft.{0, u_3, u_1} (𝕜 := ℝ) (Ei := fun (i : Fin n.succ) ↦ W) (G := E)
      (fourierIntegral 𝐞 μ L.toLinearMap₁₂ (fun (v : V) ↦ fourierPowSMulRight L f v n.succ) w))
    w
have E₁ : Eq (α := W →L[ℝ] ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin n) ↦ W) 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)
  (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)
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]
-- 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
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] fun (x : W) ↦
    fourierIntegral 𝐞 μ L.toLinearMap₁₂ (fun (v : V) ↦ fourierPowSMulRight L f v n) x
have cont : Integrable (ε := ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin n) ↦ W) E)
  (fun (v : V) ↦ fourierPowSMulRight L f v n) μ
Tactic: apply fourierIntegral_continuous Real.continuous_fourierChar (by apply L.continuous₂)
-- 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‖) μ
⊢ ContDiff ℝ (↑N : ℕ∞ω) (fourierIntegral 𝐞 μ L.toLinearMap₁₂ f)
have pos : ∀ (h'f : Integrable f μ), ContDiff ℝ (↑N : ℕ∞ω) (fourierIntegral 𝐞 μ L.toLinearMap₁₂ f)
Tactic: by_cases h'f : Integrable f μ
-- 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‖) μ
pos : ∀ (h'f : Integrable f μ), ContDiff ℝ (↑N : ℕ∞ω) (fourierIntegral 𝐞 μ L.toLinearMap₁₂ f)
⊢ ContDiff ℝ (↑N : ℕ∞ω) (fourierIntegral 𝐞 μ L.toLinearMap₁₂ f)
have neg : ∀ (h'f : ¬Integrable f μ), ContDiff ℝ (↑N : ℕ∞ω) (fourierIntegral 𝐞 μ L.toLinearMap₁₂ f)
Tactic: by_cases h'f : Integrable f μ
-- 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 : ¬Integrable f μ
⊢ fourierIntegral 𝐞 μ L.toLinearMap₁₂ f = 0
have h : ∀ (w : W), fourierIntegral 𝐞 μ L.toLinearMap₁₂ f w = 0 w
Tactic: ext w
-- Lean 4 proof step from Mathlib.Analysis.Fourier.FourierTransformDeriv (hypothesis)
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 : ¬Integrable f μ
⊢ ContDiff ℝ (↑N : ℕ∞ω) (fourierIntegral 𝐞 μ L.toLinearMap₁₂ f)
have this : fourierIntegral 𝐞 μ L.toLinearMap₁₂ f = 0
Tactic: have : fourierIntegral 𝐞 μ L.toLinearMap₁₂ f = 0 := by
      ext w; simp [fourierIntegral, integral, h'f]
-- 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
⊢ Eq (α := W → ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin n) ↦ W) E)
    (iteratedFDeriv ℝ n (fourierIntegral 𝐞 μ L.toLinearMap₁₂ f))
    (fourierIntegral 𝐞 μ L.toLinearMap₁₂ fun (v : V) ↦ fourierPowSMulRight L f v n)
have h : ∀ (w : W),
  Eq (α := ContinuousMultilinearMap.{0, 0, u_3, u_1} ℝ (fun (i : Fin n) ↦ W) E)
    (iteratedFDeriv ℝ n (fourierIntegral 𝐞 μ L.toLinearMap₁₂ f) w)
    (fourierIntegral 𝐞 μ L.toLinearMap₁₂ (fun (v : V) ↦ fourierPowSMulRight L f v n) w)
Tactic: ext w : 1
-- 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
inst_8 : FiniteDimensional ℝ V
μ : Measure V
inst_9 : μ.IsAddHaarMeasure
N : ℕ∞
hf : ContDiff ℝ (↑N : ℕ∞ω) f
h'f :
  ∀ (n : ℕ),
    (↑n : ℕ∞) ≤ N →
      Integrable (ε := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin n) ↦ V) E) (iteratedFDeriv ℝ n f) μ
hn : (↑0 : ℕ∞) ≤ N
⊢ Eq (α := (w : W) → ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin 0) ↦ V) E)
    (fourierIntegral 𝐞 μ L.toLinearMap₁₂ (iteratedFDeriv ℝ 0 f)) fun (w : W) ↦
    fourierPowSMulRight (-L.flip) (fourierIntegral 𝐞 μ L.toLinearMap₁₂ f) w 0
have zero : ∀ (w : W) (m : (i : Fin 0) → V),
  Eq.{u_1 + 1} (α := E)
    ((fourierIntegral 𝐞 μ L.toLinearMap₁₂ (iteratedFDeriv ℝ 0 f) w : (a : (i : Fin 0) → V) → E) m : E)
    ((fourierPowSMulRight (-L.flip) (fourierIntegral 𝐞 μ L.toLinearMap₁₂ f) w 0 : (a : (i : Fin 0) → V) → E) m : E)
Tactic: ext w m
-- 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
inst_8 : FiniteDimensional ℝ V
μ : Measure V
inst_9 : μ.IsAddHaarMeasure
N : ℕ∞
hf : ContDiff ℝ (↑N : ℕ∞ω) f
h'f :
  ∀ (n : ℕ),
    (↑n : ℕ∞) ≤ N →
      Integrable (ε := ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin n) ↦ V) E) (iteratedFDeriv ℝ n f) μ
n : ℕ
ih :
  ∀ (hn : (↑n : ℕ∞) ≤ N),
    Eq (α := (w : W) → ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin n) ↦ V) E)
      (fourierIntegral 𝐞 μ L.toLinearMap₁₂ (iteratedFDeriv ℝ n f)) fun (w : W) ↦
      fourierPowSMulRight (-L.flip) (fourierIntegral 𝐞 μ L.toLinearMap₁₂ f) w n
hn : (↑(n + 1) : ℕ∞) ≤ N
⊢ Eq (α := (w : W) → ContinuousMultilinearMap.{0, 0, u_2, u_1} ℝ (fun (i : Fin (n + 1)) ↦ V) E)
    (fourierIntegral 𝐞 μ L.toLinearMap₁₂ (iteratedFDeriv ℝ (n + 1) f)) fun (w : W) ↦
    fourierPowSMulRight (-L.flip) (fourierIntegral 𝐞 μ L.toLinearMap₁₂ f) w (n + 1)
have succ : ∀ (w : W) (m : (i : Fin (n + 1)) → V),
  Eq.{u_1 + 1} (α := E)
    ((fourierIntegral 𝐞 μ L.toLinearMap₁₂ (iteratedFDeriv ℝ (n + 1) f) w : (a : (i : Fin (n + 1)) → V) → E) m : E)
    ((fourierPowSMulRight (-L.flip) (fourierIntegral 𝐞 μ L.toLinearMap₁₂ f) w (n + 1) : (a : (i : Fin (n + 1)) → V) → E)
        m :
      E)
Tactic: ext w m