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
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)
⊢ (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)

Tactic:
rw [← fourierMultiplierCLM_ofReal ℂ (by fun_prop)]

Premises used: SchwartzMap.fourierMultiplierCLM_ofReal, Complex
-- 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 (β := F) (2 * (↑π : ℂ) * Complex.I * (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))
                (((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)) :
            (a : E) → F)
          x :
        F) =
    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)
⊢ (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)

Tactic:
simp_rw [map_smul, smul_apply, smul_smul]

Premises used: smul_smul, SchwartzMap.smul_apply, 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
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 :
  2 * (↑π : ℂ) * Complex.I * (2 * (↑π : ℂ) * Complex.I) =
    ((↑(RingHom.toMonoidWithZeroHom (algebraMap ℝ ℂ)) : ZeroHom ℝ ℂ) : (a : ℝ) → ℂ) (-HPow.hPow (β := ℕ) (2 * π) 2)
e_f₁ :
  Eq.{u_4 + 1} (α := F)
    (((((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))
              (((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)) :
          (a : E) → F)
        x :
      F)
    (((((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)
⊢ HSMul.hSMul (β := F) (2 * (↑π : ℂ) * Complex.I * (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))
                (((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)) :
            (a : E) → F)
          x :
        F) =
    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)

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
i : Fin (Module.finrank ℝ E)
x : E
e_f :
  HPow.hPow (β := ℕ) (↑π : ℂ) 2 * HPow.hPow (β := ℕ) Complex.I 2 * 4 =
    ({ toFun := OneHom.toFun (↑(↑(algebraMap ℝ ℂ) : ℝ →* ℂ) : OneHom ℝ ℂ), map_zero' := ⋯ : ZeroHom ℝ ℂ } : (a : ℝ) → ℂ)
      (-(HPow.hPow (β := ℕ) π 2 * 4))
⊢ 2 * (↑π : ℂ) * Complex.I * (2 * (↑π : ℂ) * Complex.I) =
    ((↑(RingHom.toMonoidWithZeroHom (algebraMap ℝ ℂ)) : ZeroHom ℝ ℂ) : (a : ℝ) → ℂ) (-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
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
⊢ HPow.hPow (β := ℕ) (↑π : ℂ) 2 * HPow.hPow (β := ℕ) Complex.I 2 * 4 =
    ({ toFun := OneHom.toFun (↑(↑(algebraMap ℝ ℂ) : ℝ →* ℂ) : OneHom ℝ ℂ), map_zero' := ⋯ : ZeroHom ℝ ℂ } : (a : ℝ) → ℂ)
      (-(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
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 :
  Eq.{u_4 + 1} (α := F)
    (((((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)) :
                  𝓢(E, F) →L[ℝ] 𝓢(E, F)) :
                (a : 𝓢(E, F)) → 𝓢(E, F))
              f :
            𝓢(E, F)) :
          (a : E) → F)
        x :
      F)
    (((((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)
    (((((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))
              (((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)) :
          (a : E) → F)
        x :
      F)
    (((((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:
rw [fourierMultiplierCLM_ofReal ℂ (by fun_prop),
      fourierMultiplierCLM_fourierMultiplierCLM_apply (by fun_prop) (by fun_prop)]

Premises used: SchwartzMap.fourierMultiplierCLM_ofReal, SchwartzMap.fourierMultiplierCLM_fourierMultiplierCLM_apply, Complex
-- 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
⊢ Eq.{u_4 + 1} (α := F)
    (((((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)) :
                  𝓢(E, F) →L[ℝ] 𝓢(E, F)) :
                (a : 𝓢(E, F)) → 𝓢(E, F))
              f :
            𝓢(E, F)) :
          (a : E) → F)
        x :
      F)
    (((((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 [sq, Pi.mul_def]

Premises used: sq, Pi.mul_def
-- 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
g : E → ℂ
f : 𝓢'(E, F)
⊢ (fourierMultiplierCLM F g : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f =
    𝓕⁻ (E := 𝓢'(E, F)) ((smulLeftCLM F g : (a : 𝓢'(E, F)) → 𝓢'(E, F)) (𝓕 f) : 𝓢'(E, F))

Tactic:
rfl
-- 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
g : E → ℂ
f : 𝓢'(E, F)
u : 𝓢(E, ℂ)
⊢ Eq.{u_4 + 1} (α := F)
    ((((fourierMultiplierCLM F g : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f : 𝓢'(E, F)) : (a : 𝓢(E, ℂ)) → F) u : F)
    ((f : (a : 𝓢(E, ℂ)) → F)
        (𝓕 (E := 𝓢(E, ℂ))
          (((SchwartzMap.smulLeftCLM ℂ g : 𝓢(E, ℂ) →L[ℂ] 𝓢(E, ℂ)) : (a : 𝓢(E, ℂ)) → 𝓢(E, ℂ)) (𝓕⁻ u) : 𝓢(E, ℂ))) :
      F)

Tactic:
rfl
-- 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
c : ℂ
h :
  ∀ (x : 𝓢'(E, F)) (x_1 : 𝓢(E, ℂ)),
    Eq.{u_4 + 1} (α := F)
      ((((fourierMultiplierCLM F fun (x : E) ↦ c : (a : 𝓢'(E, F)) → 𝓢'(E, F)) x : 𝓢'(E, F)) : (a : 𝓢(E, ℂ)) → F) x_1 :
        F)
      ((((HSMul.hSMul (β := 𝓢'(E, F) →L[ℂ] 𝓢'(E, F)) c (ContinuousLinearMap.id ℂ 𝓢'(E, F)) : (a : 𝓢'(E, F)) → 𝓢'(E, F))
                x :
              𝓢'(E, F)) :
            (a : 𝓢(E, ℂ)) → F)
          x_1 :
        F)
⊢ (fourierMultiplierCLM F fun (x : E) ↦ c) =
    HSMul.hSMul (β := 𝓢'(E, F) →L[ℂ] 𝓢'(E, F)) c (ContinuousLinearMap.id ℂ 𝓢'(E, F))

Tactic:
ext
-- 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
c : ℂ
x : 𝓢'(E, F)
x_1 : 𝓢(E, ℂ)
⊢ Eq.{u_4 + 1} (α := F)
    ((((fourierMultiplierCLM F fun (x : E) ↦ c : (a : 𝓢'(E, F)) → 𝓢'(E, F)) x : 𝓢'(E, F)) : (a : 𝓢(E, ℂ)) → F) x_1 : F)
    ((((HSMul.hSMul (β := 𝓢'(E, F) →L[ℂ] 𝓢'(E, F)) c (ContinuousLinearMap.id ℂ 𝓢'(E, F)) : (a : 𝓢'(E, F)) → 𝓢'(E, F))
              x :
            𝓢'(E, F)) :
          (a : 𝓢(E, ℂ)) → F)
        x_1 :
      F)

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
g₁ g₂ : E → ℂ
hg₁ : Function.HasTemperateGrowth g₁
hg₂ : Function.HasTemperateGrowth g₂
f : 𝓢'(E, F)
⊢ Eq (α := 𝓢'(E, F))
    ((fourierMultiplierCLM F g₂ : (a : 𝓢'(E, F)) → 𝓢'(E, F))
        ((fourierMultiplierCLM F g₁ : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f) :
      𝓢'(E, F))
    ((fourierMultiplierCLM F (g₁ * g₂) : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f : 𝓢'(E, F))

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

Premises used: TemperedDistribution.fourierMultiplierCLM_apply, TemperedDistribution.smulLeftCLM_smulLeftCLM_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
g₁ g₂ : E → ℂ
hg₁ : Function.HasTemperateGrowth g₁
hg₂ : Function.HasTemperateGrowth g₂
h :
  ∀ (f : 𝓢'(E, F)),
    Eq (α := 𝓢'(E, F))
      ((fourierMultiplierCLM F g₂ ∘SL fourierMultiplierCLM F g₁ : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f : 𝓢'(E, F))
      ((fourierMultiplierCLM F (g₁ * g₂) : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f : 𝓢'(E, F))
⊢ Eq (α := 𝓢'(E, F) →L[ℂ] 𝓢'(E, F)) (fourierMultiplierCLM F g₂ ∘SL fourierMultiplierCLM F g₁)
    (fourierMultiplierCLM F (g₁ * g₂))

Tactic:
ext1 f
-- 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
g₁ g₂ : E → ℂ
hg₁ : Function.HasTemperateGrowth g₁
hg₂ : Function.HasTemperateGrowth g₂
f : 𝓢'(E, F)
⊢ Eq (α := 𝓢'(E, F))
    ((fourierMultiplierCLM F g₂ ∘SL fourierMultiplierCLM F g₁ : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f : 𝓢'(E, F))
    ((fourierMultiplierCLM F (g₁ * g₂) : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f : 𝓢'(E, F))

Tactic:
simp [fourierMultiplierCLM_fourierMultiplierCLM_apply hg₁ hg₂]

Premises used: TemperedDistribution.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
g : E → ℂ
hg : Function.HasTemperateGrowth g
c : ℂ
h :
  ∀ (f : 𝓢'(E, F)),
    Eq (α := 𝓢'(E, F)) ((fourierMultiplierCLM F (c • g) : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f : 𝓢'(E, F))
      ((HSMul.hSMul (β := 𝓢'(E, F) →L[ℂ] 𝓢'(E, F)) c (fourierMultiplierCLM F g) : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f :
        𝓢'(E, F))
⊢ fourierMultiplierCLM F (c • g) = HSMul.hSMul (β := 𝓢'(E, F) →L[ℂ] 𝓢'(E, F)) c (fourierMultiplierCLM F g)

Tactic:
ext1 f
-- 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
g : E → ℂ
hg : Function.HasTemperateGrowth g
c : ℂ
f : 𝓢'(E, F)
⊢ Eq (α := 𝓢'(E, F)) ((fourierMultiplierCLM F (c • g) : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f : 𝓢'(E, F))
    ((HSMul.hSMul (β := 𝓢'(E, F) →L[ℂ] 𝓢'(E, F)) c (fourierMultiplierCLM F g) : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f : 𝓢'(E, F))

Tactic:
simp [fourierMultiplierCLM_apply, smulLeftCLM_smul hg]

Premises used: TemperedDistribution.fourierMultiplierCLM_apply, TemperedDistribution.smulLeftCLM_smul
-- Module: Mathlib.Analysis.Distribution.FourierMultiplier
Goal:
ι : Type u_1
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
g : ι → E → ℂ
s : Finset ι
hg : ∀ i ∈ s, Function.HasTemperateGrowth (g i)
h :
  ∀ (f : 𝓢'(E, F)) (u : 𝓢(E, ℂ)),
    Eq.{u_4 + 1} (α := F)
      ((((fourierMultiplierCLM F fun (x : E) ↦ ∑ i ∈ s, g i x : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f : 𝓢'(E, F)) :
            (a : 𝓢(E, ℂ)) → F)
          u :
        F)
      ((((∑ i ∈ s, fourierMultiplierCLM F (g i) : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f : 𝓢'(E, F)) : (a : 𝓢(E, ℂ)) → F) u : F)
⊢ Eq (α := 𝓢'(E, F) →L[ℂ] 𝓢'(E, F)) (fourierMultiplierCLM F fun (x : E) ↦ ∑ i ∈ s, g i x)
    (∑ i ∈ s, fourierMultiplierCLM F (g i))

Tactic:
ext f u
-- Module: Mathlib.Analysis.Distribution.FourierMultiplier
Goal:
ι : Type u_1
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
g : ι → E → ℂ
s : Finset ι
hg : ∀ i ∈ s, Function.HasTemperateGrowth (g i)
f : 𝓢'(E, F)
u : 𝓢(E, ℂ)
⊢ Eq.{u_4 + 1} (α := F)
    ((((fourierMultiplierCLM F fun (x : E) ↦ ∑ i ∈ s, g i x : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f : 𝓢'(E, F)) :
          (a : 𝓢(E, ℂ)) → F)
        u :
      F)
    ((((∑ i ∈ s, fourierMultiplierCLM F (g i) : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f : 𝓢'(E, F)) : (a : 𝓢(E, ℂ)) → F) u : F)

Tactic:
simp [SchwartzMap.smulLeftCLM_sum hg]

Premises used: SchwartzMap.smulLeftCLM_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
g : E → ℂ
hg : Function.HasTemperateGrowth g
f : 𝓢(E, F)
h :
  ∀ (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)
⊢ Eq (α := 𝓢'(E, F))
    ((fourierMultiplierCLM F g : (a : 𝓢'(E, F)) → 𝓢'(E, F))
        ((SchwartzMap.toTemperedDistributionCLM E F MeasureTheory.volume : (a : 𝓢(E, F)) → 𝓢'(E, F)) f) :
      𝓢'(E, 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))

Tactic:
ext u