awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Distribution.FourierMultiplier
Goal:
𝕜 : Type u_2
E : Type u_3
F : Type u_4
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace ℝ E
inst_4 : NormedSpace ℂ F
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℂ 𝕜 F
inst_7 : FiniteDimensional ℝ E
inst_8 : MeasurableSpace E
inst_9 : BorelSpace E
g : E → ℝ
hg : Function.HasTemperateGrowth g
f : 𝓢(E, F)
e_a :
  Eq (α := 𝓢(E, F))
    (((smulLeftCLM F fun (x : E) ↦ (↑(g x) : 𝕜) : 𝓢(E, F) →L[𝕜] 𝓢(E, F)) : (a : 𝓢(E, F)) → 𝓢(E, F)) (𝓕 f) : 𝓢(E, F))
    (((smulLeftCLM F g : 𝓢(E, F) →L[ℝ] 𝓢(E, F)) : (a : 𝓢(E, F)) → 𝓢(E, F)) (𝓕 f) : 𝓢(E, F))
⊢ 𝓕⁻ (E := 𝓢(E, F))
      (((smulLeftCLM F fun (x : E) ↦ (↑(g x) : 𝕜) : 𝓢(E, F) →L[𝕜] 𝓢(E, F)) : (a : 𝓢(E, F)) → 𝓢(E, F)) (𝓕 f) : 𝓢(E, F)) =
    𝓕⁻ (E := 𝓢(E, F)) (((smulLeftCLM F g : 𝓢(E, F) →L[ℝ] 𝓢(E, F)) : (a : 𝓢(E, F)) → 𝓢(E, F)) (𝓕 f) : 𝓢(E, F))

Tactic:
congr 1
-- Module: Mathlib.Analysis.Distribution.FourierMultiplier
Goal:
𝕜 : Type u_2
E : Type u_3
F : Type u_4
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace ℝ E
inst_4 : NormedSpace ℂ F
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℂ 𝕜 F
inst_7 : FiniteDimensional ℝ E
inst_8 : MeasurableSpace E
inst_9 : BorelSpace E
g : E → ℝ
hg : Function.HasTemperateGrowth g
f : 𝓢(E, F)
⊢ Eq (α := 𝓢(E, F))
    (((smulLeftCLM F fun (x : E) ↦ (↑(g x) : 𝕜) : 𝓢(E, F) →L[𝕜] 𝓢(E, F)) : (a : 𝓢(E, F)) → 𝓢(E, F)) (𝓕 f) : 𝓢(E, F))
    (((smulLeftCLM F g : 𝓢(E, F) →L[ℝ] 𝓢(E, F)) : (a : 𝓢(E, F)) → 𝓢(E, F)) (𝓕 f) : 𝓢(E, F))

Tactic:
smulLeftCLM_ofReal 𝕜 hg (𝓕 f)

Premises used: FourierTransform.fourier, SchwartzMap.smulLeftCLM_ofReal
-- Module: Mathlib.Analysis.Distribution.FourierMultiplier
Goal:
𝕜 : Type u_2
E : Type u_3
F : Type u_4
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace ℝ E
inst_4 : NormedSpace ℂ F
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℂ 𝕜 F
inst_7 : FiniteDimensional ℝ E
inst_8 : MeasurableSpace E
inst_9 : BorelSpace E
g : E → ℝ
hg : Function.HasTemperateGrowth g
f : 𝓢(E, F)
⊢ Eq (α := 𝓢(E, F))
    (((smulLeftCLM F fun (x : E) ↦ (↑(g x) : 𝕜) : 𝓢(E, F) →L[𝕜] 𝓢(E, F)) : (a : 𝓢(E, F)) → 𝓢(E, F)) (𝓕 f) : 𝓢(E, F))
    (((smulLeftCLM F g : 𝓢(E, F) →L[ℝ] 𝓢(E, F)) : (a : 𝓢(E, F)) → 𝓢(E, F)) (𝓕 f) : 𝓢(E, F))

Tactic:
exact smulLeftCLM_ofReal 𝕜 hg (𝓕 f)

Premises used: FourierTransform.fourier, SchwartzMap.smulLeftCLM_ofReal
-- Module: Mathlib.Analysis.Distribution.FourierMultiplier
Goal:
𝕜 : Type u_2
E : Type u_3
F : Type u_4
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace ℝ E
inst_4 : NormedSpace ℂ F
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℂ 𝕜 F
inst_7 : FiniteDimensional ℝ E
inst_8 : MeasurableSpace E
inst_9 : BorelSpace E
g : E → 𝕜
hg : Function.HasTemperateGrowth g
c : 𝕜
h :
  ∀ (f : 𝓢(E, F)),
    Eq (α := 𝓢(E, F)) (((fourierMultiplierCLM F (c • g) : 𝓢(E, F) →L[𝕜] 𝓢(E, F)) : (a : 𝓢(E, F)) → 𝓢(E, F)) f : 𝓢(E, F))
      ((HSMul.hSMul (β := 𝓢(E, F) →L[𝕜] 𝓢(E, F)) c (fourierMultiplierCLM F g : 𝓢(E, F) →L[𝕜] 𝓢(E, F)) :
            (a : 𝓢(E, F)) → 𝓢(E, F))
          f :
        𝓢(E, F))
⊢ fourierMultiplierCLM F (c • g) =
    HSMul.hSMul (β := 𝓢(E, F) →L[𝕜] 𝓢(E, F)) c (fourierMultiplierCLM F g : 𝓢(E, F) →L[𝕜] 𝓢(E, F))

Tactic:
ext1 f
-- Module: Mathlib.Analysis.Distribution.FourierMultiplier
Goal:
𝕜 : Type u_2
E : Type u_3
F : Type u_4
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace ℝ E
inst_4 : NormedSpace ℂ F
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℂ 𝕜 F
inst_7 : FiniteDimensional ℝ E
inst_8 : MeasurableSpace E
inst_9 : BorelSpace E
g : E → 𝕜
hg : Function.HasTemperateGrowth g
c : 𝕜
f : 𝓢(E, F)
⊢ Eq (α := 𝓢(E, F)) (((fourierMultiplierCLM F (c • g) : 𝓢(E, F) →L[𝕜] 𝓢(E, F)) : (a : 𝓢(E, F)) → 𝓢(E, F)) f : 𝓢(E, F))
    ((HSMul.hSMul (β := 𝓢(E, F) →L[𝕜] 𝓢(E, F)) c (fourierMultiplierCLM F g : 𝓢(E, F) →L[𝕜] 𝓢(E, F)) :
          (a : 𝓢(E, F)) → 𝓢(E, F))
        f :
      𝓢(E, F))

Tactic:
simp [fourierMultiplierCLM_apply, smulLeftCLM_smul hg]

Premises used: SchwartzMap.fourierMultiplierCLM_apply, SchwartzMap.smulLeftCLM_smul
-- Module: Mathlib.Analysis.Distribution.FourierMultiplier
Goal:
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
F : Type u_4
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace ℝ E
inst_4 : NormedSpace ℂ F
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℂ 𝕜 F
inst_7 : FiniteDimensional ℝ E
inst_8 : MeasurableSpace E
inst_9 : BorelSpace E
g : ι → E → 𝕜
s : Finset ι
hg : ∀ i ∈ s, Function.HasTemperateGrowth (g i)
h :
  ∀ (f : 𝓢(E, F)),
    Eq (α := 𝓢(E, F))
      (((fourierMultiplierCLM F fun (x : E) ↦ ∑ i ∈ s, g i x : 𝓢(E, F) →L[𝕜] 𝓢(E, F)) : (a : 𝓢(E, F)) → 𝓢(E, F)) f :
        𝓢(E, F))
      ((∑ i ∈ s, fourierMultiplierCLM F (g i) : (a : 𝓢(E, F)) → 𝓢(E, F)) f : 𝓢(E, F))
⊢ Eq (α := 𝓢(E, F) →L[𝕜] 𝓢(E, F)) (fourierMultiplierCLM F fun (x : E) ↦ ∑ i ∈ s, g i x : 𝓢(E, F) →L[𝕜] 𝓢(E, F))
    (∑ i ∈ s, fourierMultiplierCLM F (g i) : 𝓢(E, F) →L[𝕜] 𝓢(E, F))

Tactic:
ext1 f
-- Module: Mathlib.Analysis.Distribution.FourierMultiplier
Goal:
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
F : Type u_4
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace ℝ E
inst_4 : NormedSpace ℂ F
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℂ 𝕜 F
inst_7 : FiniteDimensional ℝ E
inst_8 : MeasurableSpace E
inst_9 : BorelSpace E
g : ι → E → 𝕜
s : Finset ι
hg : ∀ i ∈ s, Function.HasTemperateGrowth (g i)
f : 𝓢(E, F)
⊢ Eq (α := 𝓢(E, F))
    (((fourierMultiplierCLM F fun (x : E) ↦ ∑ i ∈ s, g i x : 𝓢(E, F) →L[𝕜] 𝓢(E, F)) : (a : 𝓢(E, F)) → 𝓢(E, F)) f :
      𝓢(E, F))
    ((∑ i ∈ s, fourierMultiplierCLM F (g i) : (a : 𝓢(E, F)) → 𝓢(E, F)) f : 𝓢(E, F))

Tactic:
simp [fourierMultiplierCLM_apply, smulLeftCLM_sum hg]

Premises used: SchwartzMap.smulLeftCLM_sum, SchwartzMap.fourierMultiplierCLM_apply
-- Module: Mathlib.Analysis.Distribution.FourierMultiplier
Goal:
𝕜 : Type u_2
E : Type u_3
F : Type u_4
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace ℝ E
inst_4 : NormedSpace ℂ F
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℂ 𝕜 F
inst_7 : FiniteDimensional ℝ E
inst_8 : MeasurableSpace E
inst_9 : BorelSpace E
inst_10 : CompleteSpace F
c : 𝕜
h :
  ∀ (f : 𝓢(E, F)) (x : E),
    Eq.{u_4 + 1} (α := F)
      (((((fourierMultiplierCLM F fun (x : E) ↦ c : 𝓢(E, F) →L[𝕜] 𝓢(E, F)) : (a : 𝓢(E, F)) → 𝓢(E, F)) f : 𝓢(E, F)) :
            (a : E) → F)
          x :
        F)
      ((((HSMul.hSMul (β := 𝓢(E, F) →L[𝕜] 𝓢(E, F)) c (ContinuousLinearMap.id 𝕜 𝓢(E, F)) : (a : 𝓢(E, F)) → 𝓢(E, F)) f :
              𝓢(E, F)) :
            (a : E) → F)
          x :
        F)
⊢ (fourierMultiplierCLM F fun (x : E) ↦ c) =
    HSMul.hSMul (β := 𝓢(E, F) →L[𝕜] 𝓢(E, F)) c (ContinuousLinearMap.id 𝕜 𝓢(E, F))

Tactic:
ext f x
-- Module: Mathlib.Analysis.Distribution.FourierMultiplier
Goal:
𝕜 : Type u_2
E : Type u_3
F : Type u_4
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace ℝ E
inst_4 : NormedSpace ℂ F
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℂ 𝕜 F
inst_7 : FiniteDimensional ℝ E
inst_8 : MeasurableSpace E
inst_9 : BorelSpace E
inst_10 : CompleteSpace F
c : 𝕜
f : 𝓢(E, F)
x : E
⊢ Eq.{u_4 + 1} (α := F)
    (((((fourierMultiplierCLM F fun (x : E) ↦ c : 𝓢(E, F) →L[𝕜] 𝓢(E, F)) : (a : 𝓢(E, F)) → 𝓢(E, F)) f : 𝓢(E, F)) :
          (a : E) → F)
        x :
      F)
    ((((HSMul.hSMul (β := 𝓢(E, F) →L[𝕜] 𝓢(E, F)) c (ContinuousLinearMap.id 𝕜 𝓢(E, F)) : (a : 𝓢(E, F)) → 𝓢(E, F)) f :
            𝓢(E, F)) :
          (a : E) → F)
        x :
      F)

Tactic:
simp [fourierMultiplierCLM_apply]

Premises used: SchwartzMap.fourierMultiplierCLM_apply
-- Module: Mathlib.Analysis.Distribution.FourierMultiplier
Goal:
𝕜 : Type u_2
E : Type u_3
F : Type u_4
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace ℝ E
inst_4 : NormedSpace ℂ F
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℂ 𝕜 F
inst_7 : FiniteDimensional ℝ E
inst_8 : MeasurableSpace E
inst_9 : BorelSpace E
inst_10 : CompleteSpace F
g₁ g₂ : E → 𝕜
hg₁ : Function.HasTemperateGrowth g₁
hg₂ : Function.HasTemperateGrowth g₂
f : 𝓢(E, F)
⊢ Eq (α := 𝓢(E, F))
    (((fourierMultiplierCLM F g₁ : 𝓢(E, F) →L[𝕜] 𝓢(E, F)) : (a : 𝓢(E, F)) → 𝓢(E, F))
        (((fourierMultiplierCLM F g₂ : 𝓢(E, F) →L[𝕜] 𝓢(E, F)) : (a : 𝓢(E, F)) → 𝓢(E, F)) f) :
      𝓢(E, F))
    (((fourierMultiplierCLM F (g₁ * g₂) : 𝓢(E, F) →L[𝕜] 𝓢(E, F)) : (a : 𝓢(E, F)) → 𝓢(E, F)) f : 𝓢(E, F))

Tactic:
simp [fourierMultiplierCLM_apply, smulLeftCLM_smulLeftCLM_apply hg₁ hg₂]

Premises used: SchwartzMap.fourierMultiplierCLM_apply, SchwartzMap.smulLeftCLM_smulLeftCLM_apply
-- Module: Mathlib.Analysis.Distribution.FourierMultiplier
Goal:
𝕜 : Type u_2
E : Type u_3
F : Type u_4
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace ℝ E
inst_4 : NormedSpace ℂ F
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℂ 𝕜 F
inst_7 : FiniteDimensional ℝ E
inst_8 : MeasurableSpace E
inst_9 : BorelSpace E
inst_10 : CompleteSpace F
g₁ g₂ : E → 𝕜
hg₁ : Function.HasTemperateGrowth g₁
hg₂ : Function.HasTemperateGrowth g₂
h :
  ∀ (f : 𝓢(E, F)),
    Eq (α := 𝓢(E, F))
      ((((fourierMultiplierCLM F g₁ : 𝓢(E, F) →L[𝕜] 𝓢(E, F)) ∘SL (fourierMultiplierCLM F g₂ : 𝓢(E, F) →L[𝕜] 𝓢(E, F)) :
              𝓢(E, F) →L[𝕜] 𝓢(E, F)) :
            (a : 𝓢(E, F)) → 𝓢(E, F))
          f :
        𝓢(E, F))
      (((fourierMultiplierCLM F (g₁ * g₂) : 𝓢(E, F) →L[𝕜] 𝓢(E, F)) : (a : 𝓢(E, F)) → 𝓢(E, F)) f : 𝓢(E, F))
⊢ Eq (α := 𝓢(E, F) →L[𝕜] 𝓢(E, F))
    ((fourierMultiplierCLM F g₁ : 𝓢(E, F) →L[𝕜] 𝓢(E, F)) ∘SL (fourierMultiplierCLM F g₂ : 𝓢(E, F) →L[𝕜] 𝓢(E, F)) :
      𝓢(E, F) →L[𝕜] 𝓢(E, F))
    (fourierMultiplierCLM F (g₁ * g₂) : 𝓢(E, F) →L[𝕜] 𝓢(E, F))

Tactic:
ext1 f
-- Module: Mathlib.Analysis.Distribution.FourierMultiplier
Goal:
𝕜 : Type u_2
E : Type u_3
F : Type u_4
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace ℝ E
inst_4 : NormedSpace ℂ F
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℂ 𝕜 F
inst_7 : FiniteDimensional ℝ E
inst_8 : MeasurableSpace E
inst_9 : BorelSpace E
inst_10 : CompleteSpace F
g₁ g₂ : E → 𝕜
hg₁ : Function.HasTemperateGrowth g₁
hg₂ : Function.HasTemperateGrowth g₂
f : 𝓢(E, F)
⊢ Eq (α := 𝓢(E, F))
    ((((fourierMultiplierCLM F g₁ : 𝓢(E, F) →L[𝕜] 𝓢(E, F)) ∘SL (fourierMultiplierCLM F g₂ : 𝓢(E, F) →L[𝕜] 𝓢(E, F)) :
            𝓢(E, F) →L[𝕜] 𝓢(E, F)) :
          (a : 𝓢(E, F)) → 𝓢(E, F))
        f :
      𝓢(E, F))
    (((fourierMultiplierCLM F (g₁ * g₂) : 𝓢(E, F) →L[𝕜] 𝓢(E, F)) : (a : 𝓢(E, F)) → 𝓢(E, F)) f : 𝓢(E, F))

Tactic:
simp [fourierMultiplierCLM_fourierMultiplierCLM_apply hg₁ hg₂]

Premises used: SchwartzMap.fourierMultiplierCLM_fourierMultiplierCLM_apply
-- Module: Mathlib.Analysis.Distribution.FourierMultiplier
Goal:
E : Type u_3
F : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : NormedSpace ℂ F
inst_4 : FiniteDimensional ℝ E
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
inst_7 : CompleteSpace F
m : E
f : 𝓢(E, F)
rw :
  ∂_{m} f =
    (2 * (↑π : ℂ) * Complex.I) •
      𝓕⁻ (E := 𝓢(E, F))
        (((smulLeftCLM F fun (x : E) ↦ inner ℝ x m : 𝓢(E, F) →L[ℝ] 𝓢(E, F)) : (a : 𝓢(E, F)) → 𝓢(E, F)) (𝓕 f) : 𝓢(E, F))
rw₁ :
  ∂_{m} f =
    𝓕⁻
      (HSMul.hSMul (β := 𝓢(E, F)) (2 * (↑π : ℂ) * Complex.I)
        (((smulLeftCLM F fun (x : E) ↦ inner ℝ x m : 𝓢(E, F) →L[ℝ] 𝓢(E, F)) : (a : 𝓢(E, F)) → 𝓢(E, F)) (𝓕 f) : 𝓢(E, F)))
rw₂ : ∂_{m} f = 𝓕⁻ (𝓕 (∂_{m} f))
rw₃ rw₄ : ∂_{m} f = ∂_{m} f
⊢ ∂_{m} f =
    HSMul.hSMul (β := 𝓢(E, F)) (2 * (↑π : ℂ) * Complex.I)
      (((fourierMultiplierCLM F fun (x : E) ↦ inner ℝ x m : 𝓢(E, F) →L[ℝ] 𝓢(E, F)) : (a : 𝓢(E, F)) → 𝓢(E, F)) f :
        𝓢(E, F))

Tactic:
rw [fourierMultiplierCLM_apply, ← FourierTransform.fourierInv_smul, ← fourier_lineDerivOp_eq,
    FourierTransform.fourierInv_fourier_eq]

Premises used: SchwartzMap.fourier_lineDerivOp_eq, FourierPair.fourierInv_fourier_eq, SchwartzMap.fourierMultiplierCLM_apply, FourierInvSMul.fourierInv_smul
-- Module: Mathlib.Analysis.Distribution.FourierMultiplier
Goal:
E : Type u_3
F : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : NormedSpace ℂ F
inst_4 : FiniteDimensional ℝ E
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
inst_7 : CompleteSpace F
f : 𝓢(E, F)
ι : Type := Fin (Module.finrank ℝ E)
b : OrthonormalBasis (Fin (Module.finrank ℝ E)) ℝ E := stdOrthonormalBasis ℝ E
⊢ ∀ (i : Fin (Module.finrank ℝ E)) (hi : Membership.mem (γ := Finset (Fin (Module.finrank ℝ E))) Finset.univ i),
    Function.HasTemperateGrowth (F := ℝ) fun (x : E) ↦
      HPow.hPow (β := ℕ) (inner ℝ x ((b : (a : Fin (Module.finrank ℝ E)) → E) i)) 2

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Distribution.FourierMultiplier
Goal:
E : Type u_3
F : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : NormedSpace ℂ F
inst_4 : FiniteDimensional ℝ E
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
inst_7 : CompleteSpace F
f : 𝓢(E, F)
ι : Type := Fin (Module.finrank ℝ E)
b : OrthonormalBasis (Fin (Module.finrank ℝ E)) ℝ E := stdOrthonormalBasis ℝ E
⊢ ∀ (i : Fin (Module.finrank ℝ E)) (hi : Membership.mem (γ := Finset (Fin (Module.finrank ℝ E))) Finset.univ i),
    Function.HasTemperateGrowth (F := ℝ) fun (x : E) ↦
      HPow.hPow (β := ℕ) (inner ℝ x ((b : (a : Fin (Module.finrank ℝ E)) → E) i)) 2

Tactic:
have : ∀ i (hi : i ∈ Finset.univ), (inner ℝ · (b i) ^ 2).HasTemperateGrowth := by
    fun_prop
-- Module: Mathlib.Analysis.Distribution.FourierMultiplier
Goal:
E : Type u_3
F : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : NormedSpace ℂ F
inst_4 : FiniteDimensional ℝ E
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
inst_7 : CompleteSpace F
f : 𝓢(E, F)
ι : Type := Fin (Module.finrank ℝ E)
b : OrthonormalBasis (Fin (Module.finrank ℝ E)) ℝ E := stdOrthonormalBasis ℝ E
this :
  ∀ (i : Fin (Module.finrank ℝ E)) (hi : Membership.mem (γ := Finset (Fin (Module.finrank ℝ E))) Finset.univ i),
    Function.HasTemperateGrowth (F := ℝ) fun (x : E) ↦
      HPow.hPow (β := ℕ) (inner ℝ x ((b : (a : Fin (Module.finrank ℝ E)) → E) i)) 2
simp_rw :
  Eq (α := 𝓢(E, F))
    (∑ i : Fin (Module.finrank ℝ E),
      lineDerivOp (V := E) ((b : (a : Fin (Module.finrank ℝ E)) → E) i : E)
        (lineDerivOp (V := E) ((b : (a : Fin (Module.finrank ℝ E)) → E) i : E) f))
    (∑ x : Fin (Module.finrank ℝ E),
      HSMul.hSMul (β := 𝓢(E, F)) (-HPow.hPow (β := ℕ) (2 * π) 2)
        (((fourierMultiplierCLM F fun (x_1 : E) ↦
                  HPow.hPow (β := ℕ) (inner ℝ x_1 ((b : (a : Fin (Module.finrank ℝ E)) → E) x)) 2 :
                𝓢(E, F) →L[ℝ] 𝓢(E, F)) :
              (a : 𝓢(E, F)) → 𝓢(E, F))
            f :
          𝓢(E, F)))
⊢ Δ f =
    HSMul.hSMul (β := 𝓢(E, F)) (-HPow.hPow (β := ℕ) (2 * π) 2)
      (((fourierMultiplierCLM F fun (x : E) ↦ HPow.hPow (β := ℕ) ‖x‖ 2 : 𝓢(E, F) →L[ℝ] 𝓢(E, F)) :
            (a : 𝓢(E, F)) → 𝓢(E, F))
          f :
        𝓢(E, F))

Tactic:
simp_rw [laplacian_eq_sum b, ← b.sum_sq_inner_left, fourierMultiplierCLM_sum F this,
    ContinuousLinearMap.coe_sum', Finset.sum_apply, Finset.smul_sum]

Premises used: Finset.sum_apply, SchwartzMap.fourierMultiplierCLM_sum, OrthonormalBasis.sum_sq_inner_left, ContinuousLinearMap.coe_sum', Finset.smul_sum, SchwartzMap.laplacian_eq_sum
-- Module: Mathlib.Analysis.Distribution.FourierMultiplier
Goal:
E : Type u_3
F : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : NormedSpace ℂ F
inst_4 : FiniteDimensional ℝ E
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
inst_7 : CompleteSpace F
f : 𝓢(E, F)
ι : Type := Fin (Module.finrank ℝ E)
b : OrthonormalBasis (Fin (Module.finrank ℝ E)) ℝ E := stdOrthonormalBasis ℝ E
this :
  ∀ (i : Fin (Module.finrank ℝ E)) (hi : Membership.mem (γ := Finset (Fin (Module.finrank ℝ E))) Finset.univ i),
    Function.HasTemperateGrowth (F := ℝ) fun (x : E) ↦
      HPow.hPow (β := ℕ) (inner ℝ x ((b : (a : Fin (Module.finrank ℝ E)) → E) i)) 2
e_f :
  Eq (α := Fin (Module.finrank ℝ E) → 𝓢(E, F))
    (fun (i : Fin (Module.finrank ℝ E)) ↦
      lineDerivOp (V := E) ((b : (a : Fin (Module.finrank ℝ E)) → E) i : E)
        (lineDerivOp (V := E) ((b : (a : Fin (Module.finrank ℝ E)) → E) i : E) f))
    fun (x : Fin (Module.finrank ℝ E)) ↦
    HSMul.hSMul (β := 𝓢(E, F)) (-HPow.hPow (β := ℕ) (2 * π) 2)
      (((fourierMultiplierCLM F fun (x_1 : E) ↦
                HPow.hPow (β := ℕ) (inner ℝ x_1 ((b : (a : Fin (Module.finrank ℝ E)) → E) x)) 2 :
              𝓢(E, F) →L[ℝ] 𝓢(E, F)) :
            (a : 𝓢(E, F)) → 𝓢(E, F))
          f :
        𝓢(E, F))
⊢ Eq (α := 𝓢(E, F))
    (∑ i : Fin (Module.finrank ℝ E),
      lineDerivOp (V := E) ((b : (a : Fin (Module.finrank ℝ E)) → E) i : E)
        (lineDerivOp (V := E) ((b : (a : Fin (Module.finrank ℝ E)) → E) i : E) f))
    (∑ x : Fin (Module.finrank ℝ E),
      HSMul.hSMul (β := 𝓢(E, F)) (-HPow.hPow (β := ℕ) (2 * π) 2)
        (((fourierMultiplierCLM F fun (x_1 : E) ↦
                  HPow.hPow (β := ℕ) (inner ℝ x_1 ((b : (a : Fin (Module.finrank ℝ E)) → E) x)) 2 :
                𝓢(E, F) →L[ℝ] 𝓢(E, F)) :
              (a : 𝓢(E, F)) → 𝓢(E, F))
            f :
          𝓢(E, F)))

Tactic:
congr 1
-- Module: Mathlib.Analysis.Distribution.FourierMultiplier
Goal:
E : Type u_3
F : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : NormedSpace ℂ F
inst_4 : FiniteDimensional ℝ E
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
inst_7 : CompleteSpace F
f : 𝓢(E, F)
ι : Type := Fin (Module.finrank ℝ E)
b : OrthonormalBasis (Fin (Module.finrank ℝ E)) ℝ E := stdOrthonormalBasis ℝ E
this :
  ∀ (i : Fin (Module.finrank ℝ E)) (hi : Membership.mem (γ := Finset (Fin (Module.finrank ℝ E))) Finset.univ i),
    Function.HasTemperateGrowth (F := ℝ) fun (x : E) ↦
      HPow.hPow (β := ℕ) (inner ℝ x ((b : (a : Fin (Module.finrank ℝ E)) → E) i)) 2
e_f :
  ∀ (i : Fin (Module.finrank ℝ E)) (x : E),
    Eq.{u_4 + 1} (α := F)
      ((lineDerivOp (V := E) ((b : (a : Fin (Module.finrank ℝ E)) → E) i : E)
              (lineDerivOp (V := E) ((b : (a : Fin (Module.finrank ℝ E)) → E) i : E) f) :
            (a : E) → F)
          x :
        F)
      ((HSMul.hSMul (β := 𝓢(E, F)) (-HPow.hPow (β := ℕ) (2 * π) 2)
              (((fourierMultiplierCLM F fun (x : E) ↦
                        HPow.hPow (β := ℕ) (inner ℝ x ((b : (a : Fin (Module.finrank ℝ E)) → E) i)) 2 :
                      𝓢(E, F) →L[ℝ] 𝓢(E, F)) :
                    (a : 𝓢(E, F)) → 𝓢(E, F))
                  f :
                𝓢(E, F)) :
            (a : E) → F)
          x :
        F)
⊢ Eq (α := Fin (Module.finrank ℝ E) → 𝓢(E, F))
    (fun (i : Fin (Module.finrank ℝ E)) ↦
      lineDerivOp (V := E) ((b : (a : Fin (Module.finrank ℝ E)) → E) i : E)
        (lineDerivOp (V := E) ((b : (a : Fin (Module.finrank ℝ E)) → E) i : E) f))
    fun (x : Fin (Module.finrank ℝ E)) ↦
    HSMul.hSMul (β := 𝓢(E, F)) (-HPow.hPow (β := ℕ) (2 * π) 2)
      (((fourierMultiplierCLM F fun (x_1 : E) ↦
                HPow.hPow (β := ℕ) (inner ℝ x_1 ((b : (a : Fin (Module.finrank ℝ E)) → E) x)) 2 :
              𝓢(E, F) →L[ℝ] 𝓢(E, F)) :
            (a : 𝓢(E, F)) → 𝓢(E, F))
          f :
        𝓢(E, F))

Tactic:
ext i x
-- Module: Mathlib.Analysis.Distribution.FourierMultiplier
Goal:
E : Type u_3
F : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : NormedSpace ℂ F
inst_4 : FiniteDimensional ℝ E
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
inst_7 : CompleteSpace F
f : 𝓢(E, F)
ι : Type := Fin (Module.finrank ℝ E)
b : OrthonormalBasis (Fin (Module.finrank ℝ E)) ℝ E := stdOrthonormalBasis ℝ E
this :
  ∀ (i : Fin (Module.finrank ℝ E)) (hi : Membership.mem (γ := Finset (Fin (Module.finrank ℝ E))) Finset.univ i),
    Function.HasTemperateGrowth (F := ℝ) fun (x : E) ↦
      HPow.hPow (β := ℕ) (inner ℝ x ((b : (a : Fin (Module.finrank ℝ E)) → E) i)) 2
i : Fin (Module.finrank ℝ E)
x : E
e_f :
  (HSMul.hSMul (β := 𝓢(E, F)) (2 * (↑π : ℂ) * Complex.I)
          (((fourierMultiplierCLM F fun (x : E) ↦ inner ℝ x ((b : (a : Fin (Module.finrank ℝ E)) → E) i) :
                  𝓢(E, F) →L[ℝ] 𝓢(E, F)) :
                (a : 𝓢(E, F)) → 𝓢(E, F))
              (HSMul.hSMul (β := 𝓢(E, F)) (2 * (↑π : ℂ) * Complex.I)
                (((fourierMultiplierCLM F fun (x : E) ↦ inner ℝ x ((b : (a : Fin (Module.finrank ℝ E)) → E) i) :
                        𝓢(E, F) →L[ℝ] 𝓢(E, F)) :
                      (a : 𝓢(E, F)) → 𝓢(E, F))
                    f :
                  𝓢(E, F))) :
            𝓢(E, F)) :
        (a : E) → F)
      x =
    HSMul.hSMul (β := F) (-HPow.hPow (β := ℕ) (2 * π) 2)
      (((((fourierMultiplierCLM F fun (x : E) ↦
                      HPow.hPow (β := ℕ) (inner ℝ x ((b : (a : Fin (Module.finrank ℝ E)) → E) i)) 2 :
                    𝓢(E, F) →L[ℝ] 𝓢(E, F)) :
                  (a : 𝓢(E, F)) → 𝓢(E, F))
                f :
              𝓢(E, F)) :
            (a : E) → F)
          x :
        F)
⊢ Eq.{u_4 + 1} (α := F)
    ((lineDerivOp (V := E) ((b : (a : Fin (Module.finrank ℝ E)) → E) i : E)
            (lineDerivOp (V := E) ((b : (a : Fin (Module.finrank ℝ E)) → E) i : E) f) :
          (a : E) → F)
        x :
      F)
    ((HSMul.hSMul (β := 𝓢(E, F)) (-HPow.hPow (β := ℕ) (2 * π) 2)
            (((fourierMultiplierCLM F fun (x : E) ↦
                      HPow.hPow (β := ℕ) (inner ℝ x ((b : (a : Fin (Module.finrank ℝ E)) → E) i)) 2 :
                    𝓢(E, F) →L[ℝ] 𝓢(E, F)) :
                  (a : 𝓢(E, F)) → 𝓢(E, F))
                f :
              𝓢(E, F)) :
          (a : E) → F)
        x :
      F)

Tactic:
simp_rw [smul_apply, lineDeriv_eq_fourierMultiplierCLM]

Premises used: SchwartzMap.lineDeriv_eq_fourierMultiplierCLM, SchwartzMap.smul_apply
-- Module: Mathlib.Analysis.Distribution.FourierMultiplier
Goal:
E : Type u_3
F : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : NormedSpace ℂ F
inst_4 : FiniteDimensional ℝ E
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
inst_7 : CompleteSpace F
f : 𝓢(E, F)
ι : Type := Fin (Module.finrank ℝ E)
b : OrthonormalBasis (Fin (Module.finrank ℝ E)) ℝ E := stdOrthonormalBasis ℝ E
this :
  ∀ (i : Fin (Module.finrank ℝ E)) (hi : Membership.mem (γ := Finset (Fin (Module.finrank ℝ E))) Finset.univ i),
    Function.HasTemperateGrowth (F := ℝ) fun (x : E) ↦
      HPow.hPow (β := ℕ) (inner ℝ x ((b : (a : Fin (Module.finrank ℝ E)) → E) i)) 2
i : Fin (Module.finrank ℝ E)
x : E
⊢ Function.HasTemperateGrowth (F := ℝ) fun (x : E) ↦ inner ℝ x ((b : (a : Fin (Module.finrank ℝ E)) → E) i)

Tactic:
fun_prop