awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Fourier (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℂ E
inst_3 : NormedSpace 𝕜 E
inst_4 : SMulCommClass ℂ 𝕜 E
V : Type u_3
inst_5 : NormedAddCommGroup V
inst_6 : InnerProductSpace ℝ V
inst_7 : FiniteDimensional ℝ V
inst_8 : MeasurableSpace V
inst_9 : BorelSpace V
k n : ℕ
f : 𝓢(V, E)
x : V
⊢ LE.le (α := ℝ)
    (∑ p ∈ Finset.range (n + 1) ×ˢ Finset.range (k + 1),
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
        ‖v‖ ^ p.1 *
          Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_3, u_2} ℝ (fun (i : Fin p.2) ↦ V) E)
            (iteratedFDeriv ℝ p.2 (⇑f : (a : V) → E) v))
    (∑ x ∈ Finset.range (n + 1) ×ˢ Finset.range (k + 1),
      HMul.hMul (β := ℝ)
        ((HPow.hPow (α := ℝ) 2 (integrablePower.{u_3} (E := V) volume) *
            @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : V) ↦
              HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑(integrablePower.{u_3} (E := V) volume) : ℝ))) *
          2)
        (((Finset.range (n + integrablePower.{u_3} (E := V) volume + 1) ×ˢ Finset.range (k + 1)).sup
                (schwartzSeminormFamily 𝕜 V E) :
              (a : 𝓢(V, E)) → ℝ)
            f :
          ℝ))
have h : ∀ p ∈ Finset.range (n + 1) ×ˢ Finset.range (k + 1),
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
      ‖v‖ ^ p.1 *
        Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_3, u_2} ℝ (fun (i : Fin p.2) ↦ V) E)
          (iteratedFDeriv ℝ p.2 (⇑f : (a : V) → E) v)) ≤
    HMul.hMul (β := ℝ)
      ((HPow.hPow (α := ℝ) 2 (integrablePower.{u_3} (E := V) volume) *
          @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : V) ↦
            HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑(integrablePower.{u_3} (E := V) volume) : ℝ))) *
        2)
      (((Finset.range (n + integrablePower.{u_3} (E := V) volume + 1) ×ˢ Finset.range (k + 1)).sup
              (schwartzSeminormFamily 𝕜 V E) :
            (a : 𝓢(V, E)) → ℝ)
          f :
        ℝ)
Tactic: gcongr with p
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Fourier (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℂ E
inst_3 : NormedSpace 𝕜 E
inst_4 : SMulCommClass ℂ 𝕜 E
V : Type u_3
inst_5 : NormedAddCommGroup V
inst_6 : InnerProductSpace ℝ V
inst_7 : FiniteDimensional ℝ V
inst_8 : MeasurableSpace V
inst_9 : BorelSpace V
k n : ℕ
f : 𝓢(V, E)
x : V
p : ℕ × ℕ
h : p ∈ Finset.range (n + 1) ×ˢ Finset.range (k + 1)
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (v : V) ↦
      ‖v‖ ^ p.1 *
        Norm.norm (E := ContinuousMultilinearMap.{0, 0, u_3, u_2} ℝ (fun (i : Fin p.2) ↦ V) E)
          (iteratedFDeriv ℝ p.2 (⇑f : (a : V) → E) v)) ≤
    HMul.hMul (β := ℝ)
      ((HPow.hPow (α := ℝ) 2 (integrablePower.{u_3} (E := V) volume) *
          @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : V) ↦
            HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑(integrablePower.{u_3} (E := V) volume) : ℝ))) *
        2)
      (((Finset.range (n + integrablePower.{u_3} (E := V) volume + 1) ×ˢ Finset.range (k + 1)).sup
              (schwartzSeminormFamily 𝕜 V E) :
            (a : 𝓢(V, E)) → ℝ)
          f :
        ℝ)
have h : (HPow.hPow (α := ℝ) 2 (integrablePower.{u_3} (E := V) (volume : Measure V)) *
      @integral _ _ _ _ inst_8 (volume : Measure V) fun (x : V) ↦
        HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑(integrablePower.{u_3} (E := V) (volume : Measure V)) : ℝ))) *
    HAdd.hAdd (α := ℝ) (β := ℝ) ((SchwartzMap.seminorm 𝕜 0 p.2 : (a : 𝓢(V, E)) → ℝ) f : ℝ)
      ((SchwartzMap.seminorm 𝕜 (p.1 + integrablePower.{u_3} (E := V) (volume : Measure V)) p.2 : (a : 𝓢(V, E)) → ℝ) f :
        ℝ) ≤
  HMul.hMul (β := ℝ)
    ((HPow.hPow (α := ℝ) 2 (integrablePower.{u_3} (E := V) volume) *
        @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : V) ↦
          HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑(integrablePower.{u_3} (E := V) volume) : ℝ))) *
      2)
    (((Finset.range (n + integrablePower.{u_3} (E := V) volume + 1) ×ˢ Finset.range (k + 1)).sup
            (schwartzSeminormFamily 𝕜 V E) :
          (a : 𝓢(V, E)) → ℝ)
        f :
      ℝ)
Tactic: apply (f.integral_pow_mul_iteratedFDeriv_le 𝕜 ..).trans
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Fourier (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℂ E
inst_3 : NormedSpace 𝕜 E
inst_4 : SMulCommClass ℂ 𝕜 E
V : Type u_3
inst_5 : NormedAddCommGroup V
inst_6 : InnerProductSpace ℝ V
inst_7 : FiniteDimensional ℝ V
inst_8 : MeasurableSpace V
inst_9 : BorelSpace V
k n : ℕ
f : 𝓢(V, E)
x : V
p : ℕ × ℕ
h : p ∈ Finset.range (n + 1) ×ˢ Finset.range (k + 1)
⊢ (HPow.hPow (α := ℝ) 2 (integrablePower.{u_3} (E := V) (volume : Measure V)) *
        @integral _ _ _ _ inst_8 (volume : Measure V) fun (x : V) ↦
          HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑(integrablePower.{u_3} (E := V) (volume : Measure V)) : ℝ))) *
      HAdd.hAdd (α := ℝ) (β := ℝ) ((SchwartzMap.seminorm 𝕜 0 p.2 : (a : 𝓢(V, E)) → ℝ) f : ℝ)
        ((SchwartzMap.seminorm 𝕜 (p.1 + integrablePower.{u_3} (E := V) (volume : Measure V)) p.2 : (a : 𝓢(V, E)) → ℝ)
            f :
          ℝ) ≤
    HMul.hMul (β := ℝ)
      ((HPow.hPow (α := ℝ) 2 (integrablePower.{u_3} (E := V) volume) *
          @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : V) ↦
            HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑(integrablePower.{u_3} (E := V) volume) : ℝ))) *
        2)
      (((Finset.range (n + integrablePower.{u_3} (E := V) volume + 1) ×ˢ Finset.range (k + 1)).sup
              (schwartzSeminormFamily 𝕜 V E) :
            (a : 𝓢(V, E)) → ℝ)
          f :
        ℝ)
have h : HPow.hPow (α := ℝ) 2 (integrablePower.{u_3} (E := V) (volume : Measure V)) *
    ((@integral _ _ _ _ inst_8 (volume : Measure V) fun (x : V) ↦
        HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑(integrablePower.{u_3} (E := V) (volume : Measure V)) : ℝ))) *
      HAdd.hAdd (α := ℝ) (β := ℝ) ((SchwartzMap.seminorm 𝕜 0 p.2 : (a : 𝓢(V, E)) → ℝ) f : ℝ)
        ((SchwartzMap.seminorm 𝕜 (p.1 + integrablePower.{u_3} (E := V) (volume : Measure V)) p.2 : (a : 𝓢(V, E)) → ℝ)
            f :
          ℝ)) ≤
  HPow.hPow (α := ℝ) 2 (integrablePower.{u_3} (E := V) volume) *
    ((@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : V) ↦
        HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑(integrablePower.{u_3} (E := V) volume) : ℝ))) *
      HAdd.hAdd (α := ℝ) (β := ℝ)
        (((Finset.range (n + integrablePower.{u_3} (E := V) volume + 1) ×ˢ Finset.range (k + 1)).sup
                (schwartzSeminormFamily 𝕜 V E) :
              (a : 𝓢(V, E)) → ℝ)
            f :
          ℝ)
        (((Finset.range (n + integrablePower.{u_3} (E := V) volume + 1) ×ˢ Finset.range (k + 1)).sup
                (schwartzSeminormFamily 𝕜 V E) :
              (a : 𝓢(V, E)) → ℝ)
            f :
          ℝ))
Tactic: simp only [mul_assoc, two_mul]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Fourier (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℂ E
inst_3 : NormedSpace 𝕜 E
inst_4 : SMulCommClass ℂ 𝕜 E
V : Type u_3
inst_5 : NormedAddCommGroup V
inst_6 : InnerProductSpace ℝ V
inst_7 : FiniteDimensional ℝ V
inst_8 : MeasurableSpace V
inst_9 : BorelSpace V
k n : ℕ
f : 𝓢(V, E)
x : V
p : ℕ × ℕ
h : p ∈ Finset.range (n + 1) ×ˢ Finset.range (k + 1)
⊢ HPow.hPow (α := ℝ) 2 (integrablePower.{u_3} (E := V) (volume : Measure V)) *
      ((@integral _ _ _ _ inst_8 (volume : Measure V) fun (x : V) ↦
          HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑(integrablePower.{u_3} (E := V) (volume : Measure V)) : ℝ))) *
        HAdd.hAdd (α := ℝ) (β := ℝ) ((SchwartzMap.seminorm 𝕜 0 p.2 : (a : 𝓢(V, E)) → ℝ) f : ℝ)
          ((SchwartzMap.seminorm 𝕜 (p.1 + integrablePower.{u_3} (E := V) (volume : Measure V)) p.2 : (a : 𝓢(V, E)) → ℝ)
              f :
            ℝ)) ≤
    HPow.hPow (α := ℝ) 2 (integrablePower.{u_3} (E := V) volume) *
      ((@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : V) ↦
          HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑(integrablePower.{u_3} (E := V) volume) : ℝ))) *
        HAdd.hAdd (α := ℝ) (β := ℝ)
          (((Finset.range (n + integrablePower.{u_3} (E := V) volume + 1) ×ˢ Finset.range (k + 1)).sup
                  (schwartzSeminormFamily 𝕜 V E) :
                (a : 𝓢(V, E)) → ℝ)
              f :
            ℝ)
          (((Finset.range (n + integrablePower.{u_3} (E := V) volume + 1) ×ˢ Finset.range (k + 1)).sup
                  (schwartzSeminormFamily 𝕜 V E) :
                (a : 𝓢(V, E)) → ℝ)
              f :
            ℝ))
have h : LE.le (α := ℝ) ((SchwartzMap.seminorm 𝕜 0 p.2 : (a : 𝓢(V, E)) → ℝ) f : ℝ)
  (((Finset.range (n + integrablePower.{u_3} (E := V) volume + 1) ×ˢ Finset.range (k + 1)).sup
          (schwartzSeminormFamily 𝕜 V E) :
        (a : 𝓢(V, E)) → ℝ)
      f :
    ℝ)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Fourier (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℂ E
inst_3 : NormedSpace 𝕜 E
inst_4 : SMulCommClass ℂ 𝕜 E
V : Type u_3
inst_5 : NormedAddCommGroup V
inst_6 : InnerProductSpace ℝ V
inst_7 : FiniteDimensional ℝ V
inst_8 : MeasurableSpace V
inst_9 : BorelSpace V
k n : ℕ
f : 𝓢(V, E)
x : V
p : ℕ × ℕ
h_1 : p ∈ Finset.range (n + 1) ×ˢ Finset.range (k + 1)
h :
  LE.le (α := ℝ) ((SchwartzMap.seminorm 𝕜 0 p.2 : (a : 𝓢(V, E)) → ℝ) f : ℝ)
    (((Finset.range (n + integrablePower.{u_3} (E := V) volume + 1) ×ˢ Finset.range (k + 1)).sup
            (schwartzSeminormFamily 𝕜 V E) :
          (a : 𝓢(V, E)) → ℝ)
        f :
      ℝ)
⊢ HPow.hPow (α := ℝ) 2 (integrablePower.{u_3} (E := V) (volume : Measure V)) *
      ((@integral _ _ _ _ inst_8 (volume : Measure V) fun (x : V) ↦
          HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑(integrablePower.{u_3} (E := V) (volume : Measure V)) : ℝ))) *
        HAdd.hAdd (α := ℝ) (β := ℝ) ((SchwartzMap.seminorm 𝕜 0 p.2 : (a : 𝓢(V, E)) → ℝ) f : ℝ)
          ((SchwartzMap.seminorm 𝕜 (p.1 + integrablePower.{u_3} (E := V) (volume : Measure V)) p.2 : (a : 𝓢(V, E)) → ℝ)
              f :
            ℝ)) ≤
    HPow.hPow (α := ℝ) 2 (integrablePower.{u_3} (E := V) volume) *
      ((@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : V) ↦
          HPow.hPow (β := ℝ) (1 + ‖x‖) (-(↑(integrablePower.{u_3} (E := V) volume) : ℝ))) *
        HAdd.hAdd (α := ℝ) (β := ℝ)
          (((Finset.range (n + integrablePower.{u_3} (E := V) volume + 1) ×ˢ Finset.range (k + 1)).sup
                  (schwartzSeminormFamily 𝕜 V E) :
                (a : 𝓢(V, E)) → ℝ)
              f :
            ℝ)
          (((Finset.range (n + integrablePower.{u_3} (E := V) volume + 1) ×ˢ Finset.range (k + 1)).sup
                  (schwartzSeminormFamily 𝕜 V E) :
                (a : 𝓢(V, E)) → ℝ)
              f :
            ℝ))
have h₁ : LE.le (α := ℝ)
  ((SchwartzMap.seminorm 𝕜 (p.1 + integrablePower.{u_3} (E := V) (volume : Measure V)) p.2 : (a : 𝓢(V, E)) → ℝ) f : ℝ)
  (((Finset.range (n + integrablePower.{u_3} (E := V) volume + 1) ×ˢ Finset.range (k + 1)).sup
          (schwartzSeminormFamily 𝕜 V E) :
        (a : 𝓢(V, E)) → ℝ)
      f :
    ℝ)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Fourier (hypothesis)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℂ E
inst_3 : NormedSpace 𝕜 E
inst_4 : SMulCommClass ℂ 𝕜 E
V : Type u_3
inst_5 : NormedAddCommGroup V
inst_6 : InnerProductSpace ℝ V
inst_7 : FiniteDimensional ℝ V
inst_8 : MeasurableSpace V
inst_9 : BorelSpace V
k n : ℕ
f : 𝓢(V, E)
x : V
p : ℕ × ℕ
h : p ∈ Finset.range (n + 1) ×ˢ Finset.range (k + 1)
⊢ LE.le (α := ℝ) ((SchwartzMap.seminorm 𝕜 0 p.2 : (a : 𝓢(V, E)) → ℝ) f : ℝ)
    (((Finset.range (n + integrablePower.{u_3} (E := V) volume + 1) ×ˢ Finset.range (k + 1)).sup
            (schwartzSeminormFamily 𝕜 V E) :
          (a : 𝓢(V, E)) → ℝ)
        f :
      ℝ)
have this : (0, p.2) ∈ Finset.range (n + integrablePower.{u_3} (E := V) volume + 1) ×ˢ Finset.range (k + 1)
Tactic: have : (0, p.2) ∈ Finset.range (n + integrablePower (volume : Measure V) + 1) ×ˢ
            Finset.range (k + 1) := by simp_all
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Fourier (hypothesis)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℂ E
inst_3 : NormedSpace 𝕜 E
inst_4 : SMulCommClass ℂ 𝕜 E
V : Type u_3
inst_5 : NormedAddCommGroup V
inst_6 : InnerProductSpace ℝ V
inst_7 : FiniteDimensional ℝ V
inst_8 : MeasurableSpace V
inst_9 : BorelSpace V
k n : ℕ
f : 𝓢(V, E)
x : V
p : ℕ × ℕ
h : p ∈ Finset.range (n + 1) ×ˢ Finset.range (k + 1)
⊢ LE.le (α := ℝ)
    ((SchwartzMap.seminorm 𝕜 (p.1 + integrablePower.{u_3} (E := V) (volume : Measure V)) p.2 : (a : 𝓢(V, E)) → ℝ) f : ℝ)
    (((Finset.range (n + integrablePower.{u_3} (E := V) volume + 1) ×ˢ Finset.range (k + 1)).sup
            (schwartzSeminormFamily 𝕜 V E) :
          (a : 𝓢(V, E)) → ℝ)
        f :
      ℝ)
have this : (p.1 + integrablePower.{u_3} (E := V) volume, p.2) ∈
  Finset.range (n + integrablePower.{u_3} (E := V) volume + 1) ×ˢ Finset.range (k + 1)
Tactic: have : (p.1 + integrablePower (volume : Measure V), p.2) ∈ Finset.range
            (n + integrablePower (volume : Measure V) + 1) ×ˢ Finset.range (k + 1) := by simp_all
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Fourier (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
V : Type u_3
inst_2 : NormedAddCommGroup V
inst_3 : InnerProductSpace ℝ V
inst_4 : FiniteDimensional ℝ V
inst_5 : MeasurableSpace V
inst_6 : BorelSpace V
f : 𝓢(V, E)
⊢ (⇑(𝓕⁻ f) : (a : V) → E) = 𝓕⁻ (E := (a : V) → E) (⇑f : (a : V) → E)
have h : ∀ (x : V), (𝓕⁻ f : (a : V) → E) x = 𝓕⁻ (E := (a : V) → E) (⇑f : (a : V) → E) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Fourier (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℂ E
inst_3 : NormedSpace 𝕜 E
inst_4 : SMulCommClass ℂ 𝕜 E
V : Type u_3
inst_5 : NormedAddCommGroup V
inst_6 : InnerProductSpace ℝ V
inst_7 : FiniteDimensional ℝ V
inst_8 : MeasurableSpace V
inst_9 : BorelSpace V
inst_10 : CompleteSpace E
f : 𝓢(V, E)
⊢ 𝓕⁻ (𝓕 f) = f
have h : ∀ (x : V), Eq.{u_2 + 1} (α := E) ((𝓕⁻ (𝓕 f) : (a : V) → E) x : E) ((f : (a : V) → E) x : E)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Fourier (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℂ E
inst_3 : NormedSpace 𝕜 E
inst_4 : SMulCommClass ℂ 𝕜 E
V : Type u_3
inst_5 : NormedAddCommGroup V
inst_6 : InnerProductSpace ℝ V
inst_7 : FiniteDimensional ℝ V
inst_8 : MeasurableSpace V
inst_9 : BorelSpace V
inst_10 : CompleteSpace E
f : 𝓢(V, E)
x : V
⊢ Eq.{u_2 + 1} (α := E) ((𝓕⁻ (𝓕 f) : (a : V) → E) x : E) ((f : (a : V) → E) x : E)
have h : 𝓕⁻ (E := (a : V) → E) (⇑(𝓕 f) : (a : V) → E) x = (f : (a : V) → E) x
Tactic: rw [fourierInv_coe, fourier_coe, f.continuous.fourierInv_fourier_eq f.integrable
      (𝓕 f).integrable]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Fourier (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℂ E
inst_3 : NormedSpace 𝕜 E
inst_4 : SMulCommClass ℂ 𝕜 E
V : Type u_3
inst_5 : NormedAddCommGroup V
inst_6 : InnerProductSpace ℝ V
inst_7 : FiniteDimensional ℝ V
inst_8 : MeasurableSpace V
inst_9 : BorelSpace V
inst_10 : CompleteSpace E
f : 𝓢(V, E)
x : V
h : 𝓕⁻ (E := (a : V) → E) (⇑(𝓕 f) : (a : V) → E) x = (f : (a : V) → E) x
⊢ Eq.{u_2 + 1} (α := E) ((𝓕⁻ (𝓕 f) : (a : V) → E) x : E) ((f : (a : V) → E) x : E)
have h₁ : 𝓕⁻ (𝓕 (E := (a : V) → E) (⇑f : (a : V) → E)) x = (f : (a : V) → E) x
Tactic: rw [fourierInv_coe, fourier_coe, f.continuous.fourierInv_fourier_eq f.integrable
      (𝓕 f).integrable]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Fourier (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℂ E
inst_3 : NormedSpace 𝕜 E
inst_4 : SMulCommClass ℂ 𝕜 E
V : Type u_3
inst_5 : NormedAddCommGroup V
inst_6 : InnerProductSpace ℝ V
inst_7 : FiniteDimensional ℝ V
inst_8 : MeasurableSpace V
inst_9 : BorelSpace V
inst_10 : CompleteSpace E
f : 𝓢(V, E)
x : V
h : 𝓕⁻ (E := (a : V) → E) (⇑(𝓕 f) : (a : V) → E) x = (f : (a : V) → E) x
h₁ : 𝓕⁻ (𝓕 (E := (a : V) → E) (⇑f : (a : V) → E)) x = (f : (a : V) → E) x
⊢ Eq.{u_2 + 1} (α := E) ((𝓕⁻ (𝓕 f) : (a : V) → E) x : E) ((f : (a : V) → E) x : E)
have h₂ : Eq.{u_2 + 1} (α := E) ((f : (a : V) → E) x : E) ((f : (a : V) → E) x : E)
Tactic: rw [fourierInv_coe, fourier_coe, f.continuous.fourierInv_fourier_eq f.integrable
      (𝓕 f).integrable]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Fourier (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℂ E
inst_3 : NormedSpace 𝕜 E
inst_4 : SMulCommClass ℂ 𝕜 E
V : Type u_3
inst_5 : NormedAddCommGroup V
inst_6 : InnerProductSpace ℝ V
inst_7 : FiniteDimensional ℝ V
inst_8 : MeasurableSpace V
inst_9 : BorelSpace V
inst_10 : CompleteSpace E
f : 𝓢(V, E)
⊢ 𝓕 (𝓕⁻ f) = f
have h : ∀ (x : V), Eq.{u_2 + 1} (α := E) ((𝓕 (𝓕⁻ f) : (a : V) → E) x : E) ((f : (a : V) → E) x : E)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Fourier (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℂ E
inst_3 : NormedSpace 𝕜 E
inst_4 : SMulCommClass ℂ 𝕜 E
V : Type u_3
inst_5 : NormedAddCommGroup V
inst_6 : InnerProductSpace ℝ V
inst_7 : FiniteDimensional ℝ V
inst_8 : MeasurableSpace V
inst_9 : BorelSpace V
inst_10 : CompleteSpace E
f : 𝓢(V, E)
x : V
⊢ Eq.{u_2 + 1} (α := E) ((𝓕 (𝓕⁻ f) : (a : V) → E) x : E) ((f : (a : V) → E) x : E)
have h : 𝓕 (E := (a : V) → E) (⇑(𝓕⁻ f) : (a : V) → E) x = (f : (a : V) → E) x
Tactic: rw [fourier_coe, fourierInv_coe, f.continuous.fourier_fourierInv_eq f.integrable
      (𝓕 f).integrable]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Fourier (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℂ E
inst_3 : NormedSpace 𝕜 E
inst_4 : SMulCommClass ℂ 𝕜 E
V : Type u_3
inst_5 : NormedAddCommGroup V
inst_6 : InnerProductSpace ℝ V
inst_7 : FiniteDimensional ℝ V
inst_8 : MeasurableSpace V
inst_9 : BorelSpace V
inst_10 : CompleteSpace E
f : 𝓢(V, E)
x : V
h : 𝓕 (E := (a : V) → E) (⇑(𝓕⁻ f) : (a : V) → E) x = (f : (a : V) → E) x
⊢ Eq.{u_2 + 1} (α := E) ((𝓕 (𝓕⁻ f) : (a : V) → E) x : E) ((f : (a : V) → E) x : E)
have h₁ : 𝓕 (𝓕⁻ (E := (a : V) → E) (⇑f : (a : V) → E)) x = (f : (a : V) → E) x
Tactic: rw [fourier_coe, fourierInv_coe, f.continuous.fourier_fourierInv_eq f.integrable
      (𝓕 f).integrable]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Fourier (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℂ E
inst_3 : NormedSpace 𝕜 E
inst_4 : SMulCommClass ℂ 𝕜 E
V : Type u_3
inst_5 : NormedAddCommGroup V
inst_6 : InnerProductSpace ℝ V
inst_7 : FiniteDimensional ℝ V
inst_8 : MeasurableSpace V
inst_9 : BorelSpace V
inst_10 : CompleteSpace E
f : 𝓢(V, E)
x : V
h : 𝓕 (E := (a : V) → E) (⇑(𝓕⁻ f) : (a : V) → E) x = (f : (a : V) → E) x
h₁ : 𝓕 (𝓕⁻ (E := (a : V) → E) (⇑f : (a : V) → E)) x = (f : (a : V) → E) x
⊢ Eq.{u_2 + 1} (α := E) ((𝓕 (𝓕⁻ f) : (a : V) → E) x : E) ((f : (a : V) → E) x : E)
have h₂ : Eq.{u_2 + 1} (α := E) ((f : (a : V) → E) x : E) ((f : (a : V) → E) x : E)
Tactic: rw [fourier_coe, fourierInv_coe, f.continuous.fourier_fourierInv_eq f.integrable
      (𝓕 f).integrable]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Fourier (goal)
Goal:
V : Type u_3
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : FiniteDimensional ℝ V
inst_3 : MeasurableSpace V
inst_4 : BorelSpace V
𝕜' : Type u_4
inst_5 : NormedField 𝕜'
F : Type u_5
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace ℝ F
G : Type u_6
inst_8 : NormedAddCommGroup G
inst_9 : NormedSpace ℂ G
inst_10 : NormedSpace 𝕜' G
inst_11 : SMulCommClass ℝ 𝕜' G
f : 𝓢(V, F →L[ℝ] G)
m : F
⊢ 𝓕 (E := 𝓢(V, G)) ((SchwartzMap.evalCLM 𝕜' V G m : (a : 𝓢(V, F →L[ℝ] G)) → 𝓢(V, G)) f : 𝓢(V, G)) =
    (SchwartzMap.evalCLM 𝕜' V G m : (a : 𝓢(V, F →L[ℝ] G)) → 𝓢(V, G)) (𝓕 f)
have h : ∀ (x : V),
  Eq.{u_6 + 1} (α := G)
    ((𝓕 (E := 𝓢(V, G)) ((SchwartzMap.evalCLM 𝕜' V G m : (a : 𝓢(V, F →L[ℝ] G)) → 𝓢(V, G)) f : 𝓢(V, G)) : (a : V) → G) x :
      G)
    ((((SchwartzMap.evalCLM 𝕜' V G m : (a : 𝓢(V, F →L[ℝ] G)) → 𝓢(V, G)) (𝓕 f) : 𝓢(V, G)) : (a : V) → G) x : G)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Fourier (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℂ E
inst_3 : NormedSpace 𝕜 E
inst_4 : SMulCommClass ℂ 𝕜 E
V : Type u_3
inst_5 : NormedAddCommGroup V
inst_6 : InnerProductSpace ℝ V
inst_7 : FiniteDimensional ℝ V
inst_8 : MeasurableSpace V
inst_9 : BorelSpace V
f : 𝓢(V, E)
⊢ (fderivCLM 𝕜 V E : (a : 𝓢(V, E)) → 𝓢(V, V →L[ℝ] E)) (𝓕 f) =
    𝓕
      (HSMul.hSMul (β := 𝓢(V, V →L[ℝ] E)) (-(2 * (↑π : ℂ) * Complex.I))
        (((smulRightCLM ℂ E (innerSL ℝ) : 𝓢(V, E) →L[ℂ] 𝓢(V, V →L[ℝ] E)) : (a : 𝓢(V, E)) → 𝓢(V, V →L[ℝ] E)) f :
          𝓢(V, V →L[ℝ] E)))
have h : ∀ (x : V),
  Eq (α := V →L[ℝ] E)
    ((((fderivCLM 𝕜 V E : (a : 𝓢(V, E)) → 𝓢(V, V →L[ℝ] E)) (𝓕 f) : 𝓢(V, V →L[ℝ] E)) : (a : V) → V →L[ℝ] E) x :
      V →L[ℝ] E)
    ((𝓕
            (HSMul.hSMul (β := 𝓢(V, V →L[ℝ] E)) (-(2 * (↑π : ℂ) * Complex.I))
              (((smulRightCLM ℂ E (innerSL ℝ) : 𝓢(V, E) →L[ℂ] 𝓢(V, V →L[ℝ] E)) : (a : 𝓢(V, E)) → 𝓢(V, V →L[ℝ] E)) f :
                𝓢(V, V →L[ℝ] E))) :
          (a : V) → V →L[ℝ] E)
        x :
      V →L[ℝ] E)
Tactic: ext1 x
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Fourier (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℂ E
inst_3 : NormedSpace 𝕜 E
inst_4 : SMulCommClass ℂ 𝕜 E
V : Type u_3
inst_5 : NormedAddCommGroup V
inst_6 : InnerProductSpace ℝ V
inst_7 : FiniteDimensional ℝ V
inst_8 : MeasurableSpace V
inst_9 : BorelSpace V
f : 𝓢(V, E)
x : V
⊢ Eq (α := V →L[ℝ] E)
    ((((fderivCLM 𝕜 V E : (a : 𝓢(V, E)) → 𝓢(V, V →L[ℝ] E)) (𝓕 f) : 𝓢(V, V →L[ℝ] E)) : (a : V) → V →L[ℝ] E) x :
      V →L[ℝ] E)
    ((𝓕
            (HSMul.hSMul (β := 𝓢(V, V →L[ℝ] E)) (-(2 * (↑π : ℂ) * Complex.I))
              (((smulRightCLM ℂ E (innerSL ℝ) : 𝓢(V, E) →L[ℂ] 𝓢(V, V →L[ℝ] E)) : (a : 𝓢(V, E)) → 𝓢(V, V →L[ℝ] E)) f :
                𝓢(V, V →L[ℝ] E))) :
          (a : V) → V →L[ℝ] E)
        x :
      V →L[ℝ] E)
have h : fderiv ℝ (𝓕 (E := (a : V) → E) (⇑f : (a : V) → E)) x =
  𝓕 (E := (v : V) → V →L[ℝ] E) (VectorFourier.fourierSMulRight (innerSL ℝ) (⇑f : (a : V) → E)) x
Tactic: change fderiv ℝ (𝓕 ⇑f) x = 𝓕 (VectorFourier.fourierSMulRight (innerSL ℝ) f) x
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Fourier (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℂ E
inst_3 : NormedSpace 𝕜 E
inst_4 : SMulCommClass ℂ 𝕜 E
V : Type u_3
inst_5 : NormedAddCommGroup V
inst_6 : InnerProductSpace ℝ V
inst_7 : FiniteDimensional ℝ V
inst_8 : MeasurableSpace V
inst_9 : BorelSpace V
f : 𝓢(V, E)
x : V
⊢ fderiv ℝ (𝓕 (E := (a : V) → E) (⇑f : (a : V) → E)) x =
    𝓕 (E := (v : V) → V →L[ℝ] E) (VectorFourier.fourierSMulRight (innerSL ℝ) (⇑f : (a : V) → E)) x
have h : @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace
  (fun (v : V) ↦ ‖v‖ * Norm.norm.{u_2} (E := E) ((f : (a : V) → E) v : E)) volume
Tactic: rw [fderiv_fourier f.integrable]