awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
g : E → ℂ
hg : Function.HasTemperateGrowth g
f : 𝓢(E, F)
u : 𝓢(E, ℂ)
⊢ Eq.{u_4 + 1} (α := F)
    ((((fourierMultiplierCLM F g : (a : 𝓢'(E, F)) → 𝓢'(E, F))
              ((SchwartzMap.toTemperedDistributionCLM E F MeasureTheory.volume : (a : 𝓢(E, F)) → 𝓢'(E, F)) f) :
            𝓢'(E, F)) :
          (a : 𝓢(E, ℂ)) → F)
        u :
      F)
    ((((SchwartzMap.toTemperedDistributionCLM E F MeasureTheory.volume : (a : 𝓢(E, F)) → 𝓢'(E, F))
              (((SchwartzMap.fourierMultiplierCLM F g : 𝓢(E, F) →L[ℂ] 𝓢(E, F)) : (a : 𝓢(E, F)) → 𝓢(E, F)) f) :
            𝓢'(E, F)) :
          (a : 𝓢(E, ℂ)) → F)
        u :
      F)

Tactic:
simp [SchwartzMap.integral_fourier_smul_eq, SchwartzMap.fourierMultiplierCLM_apply g f,
    ← SchwartzMap.integral_fourierInv_smul_eq, hg, smul_smul, mul_comm]

Premises used: SchwartzMap.integral_fourierInv_smul_eq, smul_smul, SchwartzMap.fourierMultiplierCLM_apply, mul_comm, SchwartzMap.integral_fourier_smul_eq
-- 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
m : E
f : 𝓢'(E, F)
rw :
  ∂_{m} f =
    (2 * (↑π : ℂ) * Complex.I) •
      𝓕⁻ (E := 𝓢'(E, F))
        ((smulLeftCLM F fun (x : E) ↦ (↑(inner ℝ x m) : ℂ) : (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) : ℂ) : (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) : ℂ) : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f : 𝓢'(E, F))

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

Premises used: FourierPair.fourierInv_fourier_eq, TemperedDistribution.fourierMultiplierCLM_apply, TemperedDistribution.fourier_lineDerivOp_eq, 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
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
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),
      (fun x ↦ Complex.ofReal (inner ℝ x (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
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 :
              (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) : ℂ) : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f :
        𝓢'(E, F))

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

Premises used: Finset.sum_apply, OrthonormalBasis.sum_sq_inner_left, Complex.ofReal_sum, TemperedDistribution.laplacian_eq_sum, ContinuousLinearMap.coe_sum', Finset.smul_sum, TemperedDistribution.fourierMultiplierCLM_sum, Complex.ofReal_pow
-- 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
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 :
            (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 :
              (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
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 :
                    (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 :
            (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
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 :
  Eq.{u_4 + 1} (α := F)
    ((HSMul.hSMul (β := 𝓢'(E, F)) (2 * (↑π : ℂ) * Complex.I * (2 * (↑π : ℂ) * Complex.I))
            ((fourierMultiplierCLM F fun (x : E) ↦ (↑(inner ℝ x ((b : (a : Fin (Module.finrank ℝ E)) → E) i)) : ℂ) :
                  (a : 𝓢'(E, F)) → 𝓢'(E, F))
                ((fourierMultiplierCLM F fun (x : E) ↦ (↑(inner ℝ x ((b : (a : Fin (Module.finrank ℝ E)) → E) i)) : ℂ) :
                    (a : 𝓢'(E, F)) → 𝓢'(E, F))
                  f) :
              𝓢'(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 :
                  (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 :
                  (a : 𝓢'(E, F)) → 𝓢'(E, F))
                f :
              𝓢'(E, F)) :
          (a : 𝓢(E, ℂ)) → F)
        x :
      F)

Tactic:
simp_rw [lineDeriv_eq_fourierMultiplierCLM, map_smul, smul_smul]

Premises used: smul_smul, TemperedDistribution.lineDeriv_eq_fourierMultiplierCLM, map_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
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
-- 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
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 :
  Eq.{u_4 + 1} (α := F)
    ((HSMul.hSMul (β := 𝓢'(E, F)) (2 * (↑π : ℂ) * Complex.I * (2 * (↑π : ℂ) * Complex.I))
            ((fourierMultiplierCLM F
                    (HMul.hMul (α := E → ℂ)
                      (fun (x : E) ↦ (↑(inner ℝ x ((b : (a : Fin (Module.finrank ℝ E)) → E) i)) : ℂ)) fun (x : E) ↦
                      (↑(inner ℝ x ((b : (a : Fin (Module.finrank ℝ E)) → E) i)) : ℂ)) :
                  (a : 𝓢'(E, F)) → 𝓢'(E, F))
                f :
              𝓢'(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 :
                  (a : 𝓢'(E, F)) → 𝓢'(E, F))
                f :
              𝓢'(E, F)) :
          (a : 𝓢(E, ℂ)) → F)
        x :
      F)
⊢ Eq.{u_4 + 1} (α := F)
    ((HSMul.hSMul (β := 𝓢'(E, F)) (2 * (↑π : ℂ) * Complex.I * (2 * (↑π : ℂ) * Complex.I))
            ((fourierMultiplierCLM F fun (x : E) ↦ (↑(inner ℝ x ((b : (a : Fin (Module.finrank ℝ E)) → E) i)) : ℂ) :
                  (a : 𝓢'(E, F)) → 𝓢'(E, F))
                ((fourierMultiplierCLM F fun (x : E) ↦ (↑(inner ℝ x ((b : (a : Fin (Module.finrank ℝ E)) → E) i)) : ℂ) :
                    (a : 𝓢'(E, F)) → 𝓢'(E, F))
                  f) :
              𝓢'(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 :
                  (a : 𝓢'(E, F)) → 𝓢'(E, F))
                f :
              𝓢'(E, F)) :
          (a : 𝓢(E, ℂ)) → F)
        x :
      F)

Tactic:
rw [fourierMultiplierCLM_fourierMultiplierCLM_apply (by fun_prop) (by fun_prop),
    ← Complex.coe_smul (-(2 * π) ^ 2)]

Premises used: Real.pi, HMul.hMul, TemperedDistribution.fourierMultiplierCLM_fourierMultiplierCLM_apply, HPow.hPow, Complex.coe_smul, OfNat.ofNat, Neg.neg
-- 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
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 : 2 * (↑π : ℂ) * Complex.I * (2 * (↑π : ℂ) * Complex.I) = (↑(-HPow.hPow (β := ℕ) (2 * π) 2) : ℂ)
e_f₁ :
  (HMul.hMul (α := E → ℂ) (fun (x : E) ↦ (↑(inner ℝ x ((b : (a : Fin (Module.finrank ℝ E)) → E) i)) : ℂ)) fun (x : E) ↦
      (↑(inner ℝ x ((b : (a : Fin (Module.finrank ℝ E)) → E) i)) : ℂ)) =
    fun (x : E) ↦ HPow.hPow (β := ℕ) (↑(inner ℝ x ((b : (a : Fin (Module.finrank ℝ E)) → E) i)) : ℂ) 2
⊢ Eq.{u_4 + 1} (α := F)
    ((HSMul.hSMul (β := 𝓢'(E, F)) (2 * (↑π : ℂ) * Complex.I * (2 * (↑π : ℂ) * Complex.I))
            ((fourierMultiplierCLM F
                    (HMul.hMul (α := E → ℂ)
                      (fun (x : E) ↦ (↑(inner ℝ x ((b : (a : Fin (Module.finrank ℝ E)) → E) i)) : ℂ)) fun (x : E) ↦
                      (↑(inner ℝ x ((b : (a : Fin (Module.finrank ℝ E)) → E) i)) : ℂ)) :
                  (a : 𝓢'(E, F)) → 𝓢'(E, F))
                f :
              𝓢'(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 :
                  (a : 𝓢'(E, F)) → 𝓢'(E, F))
                f :
              𝓢'(E, F)) :
          (a : 𝓢(E, ℂ)) → F)
        x :
      F)

Tactic:
congr 4
-- 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
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 : HPow.hPow (β := ℕ) (↑π : ℂ) 2 * HPow.hPow (β := ℕ) Complex.I 2 * 4 = (↑(-(HPow.hPow (β := ℕ) π 2 * 4)) : ℂ)
⊢ 2 * (↑π : ℂ) * Complex.I * (2 * (↑π : ℂ) * Complex.I) = (↑(-HPow.hPow (β := ℕ) (2 * π) 2) : ℂ)

Tactic:
ring_nf
-- 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
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, ℂ)
⊢ HPow.hPow (β := ℕ) (↑π : ℂ) 2 * HPow.hPow (β := ℕ) Complex.I 2 * 4 = (↑(-(HPow.hPow (β := ℕ) π 2 * 4)) : ℂ)

Tactic:
simp
-- 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
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, ℂ)
⊢ (HMul.hMul (α := E → ℂ) (fun (x : E) ↦ (↑(inner ℝ x ((b : (a : Fin (Module.finrank ℝ E)) → E) i)) : ℂ)) fun (x : E) ↦
      (↑(inner ℝ x ((b : (a : Fin (Module.finrank ℝ E)) → E) i)) : ℂ)) =
    fun (x : E) ↦ HPow.hPow (β := ℕ) (↑(inner ℝ x ((b : (a : Fin (Module.finrank ℝ E)) → E) i)) : ℂ) 2

Tactic:
simp [sq, Pi.mul_def]

Premises used: sq, Pi.mul_def
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
D : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
H : Type u_8
V : Type u_9
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
f g : 𝓢(E, F)
h : Eq (α := (a : E) → F) ((fun (f : 𝓢(E, F)) ↦ f.toFun) f) ((fun (f : 𝓢(E, F)) ↦ f.toFun) g)
mk :
  ∀ (toFun : E → F) (smooth' : ContDiff ℝ ∞ toFun)
    (decay' :
      ∀ (k n : ℕ),
        ∃ (C : ℝ),
          ∀ (x : E),
            ‖x‖ ^ k *
                norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
                  (iteratedFDeriv ℝ n toFun x) ≤
              C)
    (h :
      Eq (α := (a : E) → F) ((fun (f : 𝓢(E, F)) ↦ f.toFun) { toFun := toFun, smooth' := smooth', decay' := decay' })
        ((fun (f : 𝓢(E, F)) ↦ f.toFun) g)),
    { toFun := toFun, smooth' := smooth', decay' := decay' : 𝓢(E, F) } = g
⊢ f = g

Tactic:
cases f
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
D : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
H : Type u_8
V : Type u_9
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
g : 𝓢(E, F)
toFun : E → F
smooth' : ContDiff ℝ ∞ toFun
decay' :
  ∀ (k n : ℕ),
    ∃ (C : ℝ),
      ∀ (x : E),
        ‖x‖ ^ k *
            norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
              (iteratedFDeriv ℝ n toFun x) ≤
          C
h :
  Eq (α := (a : E) → F) ((fun (f : 𝓢(E, F)) ↦ f.toFun) { toFun := toFun, smooth' := smooth', decay' := decay' })
    ((fun (f : 𝓢(E, F)) ↦ f.toFun) g)
mk :
  ∀ (toFun_1 : E → F) (smooth'_1 : ContDiff ℝ ∞ toFun_1)
    (decay'_1 :
      ∀ (k n : ℕ),
        ∃ (C : ℝ),
          ∀ (x : E),
            ‖x‖ ^ k *
                norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
                  (iteratedFDeriv ℝ n toFun_1 x) ≤
              C)
    (h :
      Eq (α := (a : E) → F) ((fun (f : 𝓢(E, F)) ↦ f.toFun) { toFun := toFun, smooth' := smooth', decay' := decay' })
        ((fun (f : 𝓢(E, F)) ↦ f.toFun) { toFun := toFun_1, smooth' := smooth'_1, decay' := decay'_1 })),
    { toFun := toFun, smooth' := smooth', decay' := decay' : 𝓢(E, F) } =
      { toFun := toFun_1, smooth' := smooth'_1, decay' := decay'_1 }
⊢ { toFun := toFun, smooth' := smooth', decay' := decay' : 𝓢(E, F) } = g

Tactic:
cases g
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
D : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
H : Type u_8
V : Type u_9
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
toFun : E → F
smooth' : ContDiff ℝ ∞ toFun
decay' :
  ∀ (k n : ℕ),
    ∃ (C : ℝ),
      ∀ (x : E),
        ‖x‖ ^ k *
            norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
              (iteratedFDeriv ℝ n toFun x) ≤
          C
toFun_1 : E → F
smooth'_1 : ContDiff ℝ ∞ toFun_1
decay'_1 :
  ∀ (k n : ℕ),
    ∃ (C : ℝ),
      ∀ (x : E),
        ‖x‖ ^ k *
            norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
              (iteratedFDeriv ℝ n toFun_1 x) ≤
          C
h :
  Eq (α := (a : E) → F) ((fun (f : 𝓢(E, F)) ↦ f.toFun) { toFun := toFun, smooth' := smooth', decay' := decay' })
    ((fun (f : 𝓢(E, F)) ↦ f.toFun) { toFun := toFun_1, smooth' := smooth'_1, decay' := decay'_1 })
⊢ { toFun := toFun, smooth' := smooth', decay' := decay' : 𝓢(E, F) } =
    { toFun := toFun_1, smooth' := smooth'_1, decay' := decay'_1 }

Tactic:
congr