awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Distribution.FourierMultiplier (goal)
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 : ℂ
⊢ (fourierMultiplierCLM F fun (x : E) ↦ c) =
    HSMul.hSMul (β := 𝓢'(E, F) →L[ℂ] 𝓢'(E, F)) c (ContinuousLinearMap.id ℂ 𝓢'(E, F))
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Distribution.FourierMultiplier (goal)
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₂
⊢ Eq (α := 𝓢'(E, F) →L[ℂ] 𝓢'(E, F)) (fourierMultiplierCLM F g₂ ∘SL fourierMultiplierCLM F g₁)
    (fourierMultiplierCLM F (g₁ * g₂))
have 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))
Tactic: ext1 f
-- Lean 4 proof step from Mathlib.Analysis.Distribution.FourierMultiplier (goal)
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 : ℂ
⊢ fourierMultiplierCLM F (c • g) = HSMul.hSMul (β := 𝓢'(E, F) →L[ℂ] 𝓢'(E, F)) c (fourierMultiplierCLM F g)
have 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))
Tactic: ext1 f
-- Lean 4 proof step from Mathlib.Analysis.Distribution.FourierMultiplier (goal)
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)
⊢ Eq (α := 𝓢'(E, F) →L[ℂ] 𝓢'(E, F)) (fourierMultiplierCLM F fun (x : E) ↦ ∑ i ∈ s, g i x)
    (∑ i ∈ s, fourierMultiplierCLM F (g i))
have 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)
Tactic: ext f u
-- Lean 4 proof step from Mathlib.Analysis.Distribution.FourierMultiplier (goal)
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)
⊢ 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))
have 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)
Tactic: ext u
-- Lean 4 proof step from Mathlib.Analysis.Distribution.FourierMultiplier (goal)
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)
⊢ ∂_{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))
have 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))
Tactic: rw [fourierMultiplierCLM_apply, ← FourierTransform.fourierInv_smul, ← fourier_lineDerivOp_eq,
    FourierTransform.fourierInv_fourier_eq]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.FourierMultiplier (goal)
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))
⊢ ∂_{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))
have 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)))
Tactic: rw [fourierMultiplierCLM_apply, ← FourierTransform.fourierInv_smul, ← fourier_lineDerivOp_eq,
    FourierTransform.fourierInv_fourier_eq]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.FourierMultiplier (goal)
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)))
⊢ ∂_{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))
have rw₂ : ∂_{m} f = 𝓕⁻ (𝓕 (∂_{m} f))
Tactic: rw [fourierMultiplierCLM_apply, ← FourierTransform.fourierInv_smul, ← fourier_lineDerivOp_eq,
    FourierTransform.fourierInv_fourier_eq]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.FourierMultiplier (goal)
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))
⊢ ∂_{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))
have rw₃ : ∂_{m} f = ∂_{m} f
Tactic: rw [fourierMultiplierCLM_apply, ← FourierTransform.fourierInv_smul, ← fourier_lineDerivOp_eq,
    FourierTransform.fourierInv_fourier_eq]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.FourierMultiplier (hypothesis)
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
⊢ Δ 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))
have 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
Tactic: have : ∀ i (hi : i ∈ Finset.univ),
      (fun x ↦ Complex.ofReal (inner ℝ x (b i)) ^ 2).HasTemperateGrowth := by
    fun_prop
-- Lean 4 proof step from Mathlib.Analysis.Distribution.FourierMultiplier (goal)
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
⊢ Δ 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))
have 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)))
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]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.FourierMultiplier (goal)
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
⊢ 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)))
have 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))
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Analysis.Distribution.FourierMultiplier (goal)
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
⊢ 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))
have 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)
Tactic: ext i x
-- Lean 4 proof step from Mathlib.Analysis.Distribution.FourierMultiplier (goal)
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, ℂ)
⊢ 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)
have 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)
Tactic: simp_rw [lineDeriv_eq_fourierMultiplierCLM, map_smul, smul_smul]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.FourierMultiplier (goal)
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, ℂ)
⊢ 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)
have 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)
Tactic: rw [fourierMultiplierCLM_fourierMultiplierCLM_apply (by fun_prop) (by fun_prop),
    ← Complex.coe_smul (-(2 * π) ^ 2)]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.FourierMultiplier (goal)
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, ℂ)
⊢ 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)
have e_f : 2 * (↑π : ℂ) * Complex.I * (2 * (↑π : ℂ) * Complex.I) = (↑(-HPow.hPow (β := ℕ) (2 * π) 2) : ℂ)
Tactic: congr 4
-- Lean 4 proof step from Mathlib.Analysis.Distribution.FourierMultiplier (goal)
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) : ℂ)
⊢ 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)
have 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
Tactic: congr 4