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
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))
⊢ ∂_{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))
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
inst_7 : CompleteSpace F
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 : 𝓢(E, F) →L[ℝ] 𝓢(E, F)) :
            (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), (inner ℝ · (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
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
⊢ Δ 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))
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 :
              𝓢(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]
-- 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
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 :
                𝓢(E, F) →L[ℝ] 𝓢(E, F)) :
              (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 :
            𝓢(E, F) →L[ℝ] 𝓢(E, F)) :
          (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
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
⊢ 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))
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 :
                    𝓢(E, F) →L[ℝ] 𝓢(E, F)) :
                  (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
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)
    ((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)
have 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)
Tactic: simp_rw [smul_apply, lineDeriv_eq_fourierMultiplierCLM]
-- 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
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
⊢ (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)
have 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)
Tactic: rw [← fourierMultiplierCLM_ofReal ℂ (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
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
⊢ (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)
have 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)
Tactic: simp_rw [map_smul, smul_apply, 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
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
⊢ 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)
have e_f : 2 * (↑π : ℂ) * Complex.I * (2 * (↑π : ℂ) * Complex.I) =
  ((↑(RingHom.toMonoidWithZeroHom (algebraMap ℝ ℂ)) : ZeroHom ℝ ℂ) : (a : ℝ) → ℂ) (-HPow.hPow (β := ℕ) (2 * π) 2)
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
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)
⊢ 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)
have 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)
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
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
⊢ 2 * (↑π : ℂ) * Complex.I * (2 * (↑π : ℂ) * Complex.I) =
    ((↑(RingHom.toMonoidWithZeroHom (algebraMap ℝ ℂ)) : ZeroHom ℝ ℂ) : (a : ℝ) → ℂ) (-HPow.hPow (β := ℕ) (2 * π) 2)
have e_f : HPow.hPow (β := ℕ) (↑π : ℂ) 2 * HPow.hPow (β := ℕ) Complex.I 2 * 4 =
  ({ toFun := OneHom.toFun (↑(↑(algebraMap ℝ ℂ) : ℝ →* ℂ) : OneHom ℝ ℂ), map_zero' := sorry : ZeroHom ℝ ℂ } : (a : ℝ) → ℂ)
    (-(HPow.hPow (β := ℕ) π 2 * 4))
Tactic: ring_nf
-- 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
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 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)
have 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)
Tactic: rw [fourierMultiplierCLM_ofReal ℂ (by fun_prop),
      fourierMultiplierCLM_fourierMultiplierCLM_apply (by fun_prop) (by fun_prop)]