awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Distribution.TemperedDistribution
Goal:
E : Type u_3
F : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace ℂ F
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
μ : Measure E
hμ : μ.HasTemperateGrowth
inst_6 : CompleteSpace F
p q r : ℝ≥0∞
inst_7 : p.HolderTriple q r
inst_8 : Fact (1 ≤ q)
inst_9 : Fact (1 ≤ r)
g : E → ℂ
hg₁ : Function.HasTemperateGrowth g
hg₂ : MemLp g p μ
f : ↥(Lp F q μ)
u : 𝓢(E, ℂ)
h :
  ∀ (x : E)
    (hg :
      (↑(↑(MemLp.toLp g hg₂ • f) : E →ₘ[μ] F) : E → F) x =
        ((↑(↑(MemLp.toLp g hg₂) : E →ₘ[μ] ℂ) : E → ℂ) • (↑(↑f : E →ₘ[μ] F) : E → F)) x)
    (hg' : (↑(↑(MemLp.toLp g hg₂) : E →ₘ[μ] ℂ) : E → ℂ) x = g x),
    HSMul.hSMul (α := ℂ) ((u : (a : E) → ℂ) x : ℂ) ((↑(↑(MemLp.toLp g hg₂ • f) : E →ₘ[μ] F) : E → F) x) =
      HSMul.hSMul (α := ℂ)
        (((((SchwartzMap.smulLeftCLM ℂ g : 𝓢(E, ℂ) →L[ℂ] 𝓢(E, ℂ)) : (a : 𝓢(E, ℂ)) → 𝓢(E, ℂ)) u : 𝓢(E, ℂ)) : (a : E) → ℂ)
            x :
          ℂ)
        ((↑(↑f : E →ₘ[μ] F) : E → F) x)
⊢ Filter.EventuallyEq.{u_3, u_4} (β := F) (ae μ)
    (fun (a : E) ↦ HSMul.hSMul (α := ℂ) ((u : (a : E) → ℂ) a : ℂ) ((↑(↑(MemLp.toLp g hg₂ • f) : E →ₘ[μ] F) : E → F) a))
    fun (a : E) ↦
    HSMul.hSMul (α := ℂ)
      (((((SchwartzMap.smulLeftCLM ℂ g : 𝓢(E, ℂ) →L[ℂ] 𝓢(E, ℂ)) : (a : 𝓢(E, ℂ)) → 𝓢(E, ℂ)) u : 𝓢(E, ℂ)) : (a : E) → ℂ)
          a :
        ℂ)
      ((↑(↑f : E →ₘ[μ] F) : E → F) a)

Tactic:
filter_upwards [Lp.coeFn_lpSMul (r := r) (hg₂.toLp _) f, hg₂.coeFn_toLp] with x hg hg'

Premises used: MeasureTheory.Lp.coeFn_lpSMul, MeasureTheory.MemLp.toLp, MeasureTheory.MemLp.coeFn_toLp
-- Module: Mathlib.Analysis.Distribution.TemperedDistribution
Goal:
E : Type u_3
F : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace ℂ F
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
μ : Measure E
hμ : μ.HasTemperateGrowth
inst_6 : CompleteSpace F
p q r : ℝ≥0∞
inst_7 : p.HolderTriple q r
inst_8 : Fact (1 ≤ q)
inst_9 : Fact (1 ≤ r)
g : E → ℂ
hg₁ : Function.HasTemperateGrowth g
hg₂ : MemLp g p μ
f : ↥(Lp F q μ)
u : 𝓢(E, ℂ)
x : E
hg :
  (↑(↑(MemLp.toLp g hg₂ • f) : E →ₘ[μ] F) : E → F) x =
    ((↑(↑(MemLp.toLp g hg₂) : E →ₘ[μ] ℂ) : E → ℂ) • (↑(↑f : E →ₘ[μ] F) : E → F)) x
hg' : (↑(↑(MemLp.toLp g hg₂) : E →ₘ[μ] ℂ) : E → ℂ) x = g x
⊢ HSMul.hSMul (α := ℂ) ((u : (a : E) → ℂ) x : ℂ) ((↑(↑(MemLp.toLp g hg₂ • f) : E →ₘ[μ] F) : E → F) x) =
    HSMul.hSMul (α := ℂ)
      (((((SchwartzMap.smulLeftCLM ℂ g : 𝓢(E, ℂ) →L[ℂ] 𝓢(E, ℂ)) : (a : 𝓢(E, ℂ)) → 𝓢(E, ℂ)) u : 𝓢(E, ℂ)) : (a : E) → ℂ)
          x :
        ℂ)
      ((↑(↑f : E →ₘ[μ] F) : E → F) x)

Tactic:
simp [hg, hg', hg₁, smul_smul, mul_comm]

Premises used: smul_smul, mul_comm
-- Module: Mathlib.Analysis.Distribution.TemperedDistribution
Goal:
F : Type u_4
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℂ F
f : 𝓢'(ℝ, F)
g : 𝓢(ℝ, ℂ)
⊢ Eq (α := F) ((((derivCLM F : (a : 𝓢'(ℝ, F)) → 𝓢'(ℝ, F)) f : 𝓢'(ℝ, F)) : (a : 𝓢(ℝ, ℂ)) → F) g : F)
    ((f : (a : 𝓢(ℝ, ℂ)) → F) (-(SchwartzMap.derivCLM ℂ ℂ : (a : 𝓢(ℝ, ℂ)) → 𝓢(ℝ, ℂ)) g : 𝓢(ℝ, ℂ)) : F)

Tactic:
rfl

Premises used: ContinuousLinearMap.comp, UniformConvergenceCLM, rfl
-- Module: Mathlib.Analysis.Distribution.TemperedDistribution
Goal:
𝕜 : Type u_2
F : Type u_4
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℂ F
inst_2 : RCLike 𝕜
inst_3 : NormedSpace 𝕜 F
f : 𝓢(ℝ, F)
h :
  ∀ (g : 𝓢(ℝ, ℂ)),
    Eq (α := F)
      ((((derivCLM F : (a : 𝓢'(ℝ, F)) → 𝓢'(ℝ, F))
                ((toTemperedDistributionCLM ℝ F volume : (a : 𝓢(ℝ, F)) → 𝓢'(ℝ, F)) f) :
              𝓢'(ℝ, F)) :
            (a : 𝓢(ℝ, ℂ)) → F)
          g :
        F)
      ((((toTemperedDistributionCLM ℝ F volume : (a : 𝓢(ℝ, F)) → 𝓢'(ℝ, F))
                ((SchwartzMap.derivCLM 𝕜 F : (a : 𝓢(ℝ, F)) → 𝓢(ℝ, F)) f) :
              𝓢'(ℝ, F)) :
            (a : 𝓢(ℝ, ℂ)) → F)
          g :
        F)
⊢ Eq (α := 𝓢'(ℝ, F))
    ((derivCLM F : (a : 𝓢'(ℝ, F)) → 𝓢'(ℝ, F)) ((toTemperedDistributionCLM ℝ F volume : (a : 𝓢(ℝ, F)) → 𝓢'(ℝ, F)) f) :
      𝓢'(ℝ, F))
    ((toTemperedDistributionCLM ℝ F volume : (a : 𝓢(ℝ, F)) → 𝓢'(ℝ, F))
        ((SchwartzMap.derivCLM 𝕜 F : (a : 𝓢(ℝ, F)) → 𝓢(ℝ, F)) f) :
      𝓢'(ℝ, F))

Tactic:
ext1 g
-- Module: Mathlib.Analysis.Distribution.TemperedDistribution
Goal:
𝕜 : Type u_2
F : Type u_4
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℂ F
inst_2 : RCLike 𝕜
inst_3 : NormedSpace 𝕜 F
f : 𝓢(ℝ, F)
g : 𝓢(ℝ, ℂ)
⊢ Eq (α := F)
    ((((derivCLM F : (a : 𝓢'(ℝ, F)) → 𝓢'(ℝ, F)) ((toTemperedDistributionCLM ℝ F volume : (a : 𝓢(ℝ, F)) → 𝓢'(ℝ, F)) f) :
            𝓢'(ℝ, F)) :
          (a : 𝓢(ℝ, ℂ)) → F)
        g :
      F)
    ((((toTemperedDistributionCLM ℝ F volume : (a : 𝓢(ℝ, F)) → 𝓢'(ℝ, F))
              ((SchwartzMap.derivCLM 𝕜 F : (a : 𝓢(ℝ, F)) → 𝓢(ℝ, F)) f) :
            𝓢'(ℝ, F)) :
          (a : 𝓢(ℝ, ℂ)) → F)
        g :
      F)

Tactic:
simp [integral_smul_deriv_right_eq_neg_left, integral_neg]

Premises used: MeasureTheory.integral_neg, SchwartzMap.integral_smul_deriv_right_eq_neg_left
-- Module: Mathlib.Analysis.Distribution.TemperedDistribution
Goal:
E : Type u_3
F : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace ℂ F
f : 𝓢'(E, F)
g : 𝓢(E, ℂ)
m : E
⊢ Eq.{u_4 + 1} (α := F) ((∂_{m} f : (a : 𝓢(E, ℂ)) → F) g : F) ((f : (a : 𝓢(E, ℂ)) → F) (-∂_{m} g) : F)

Tactic:
rfl

Premises used: ContinuousLinearMap.comp, UniformConvergenceCLM, rfl
-- Module: Mathlib.Analysis.Distribution.TemperedDistribution
Goal:
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
F : Type u_4
F₁ : Type u_5
F₂ : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace ℂ F
x y : E
f : 𝓢'(E, F)
h :
  ∀ (u : 𝓢(E, ℂ)),
    Eq.{u_4 + 1} (α := F) ((∂_{x + y} f : (a : 𝓢(E, ℂ)) → F) u : F) ((∂_{x} f + ∂_{y} f : (a : 𝓢(E, ℂ)) → F) u : F)
⊢ ∂_{x + y} f = ∂_{x} f + ∂_{y} f

Tactic:
ext u
-- Module: Mathlib.Analysis.Distribution.TemperedDistribution
Goal:
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
F : Type u_4
F₁ : Type u_5
F₂ : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace ℂ F
x y : E
f : 𝓢'(E, F)
u : 𝓢(E, ℂ)
⊢ Eq.{u_4 + 1} (α := F) ((∂_{x + y} f : (a : 𝓢(E, ℂ)) → F) u : F) ((∂_{x} f + ∂_{y} f : (a : 𝓢(E, ℂ)) → F) u : F)

Tactic:
simp [lineDerivOp_left_add, UniformConvergenceCLM.add_apply, add_comm]

Premises used: UniformConvergenceCLM.add_apply, LineDerivAdd.lineDerivOp_left_add, add_comm
-- Module: Mathlib.Analysis.Distribution.TemperedDistribution
Goal:
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
F : Type u_4
F₁ : Type u_5
F₂ : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace ℂ F
r : ℝ
x : E
f : 𝓢'(E, F)
h :
  ∀ (u : 𝓢(E, ℂ)),
    Eq.{u_4 + 1} (α := F) ((∂_{r • x} f : (a : 𝓢(E, ℂ)) → F) u : F) ((r • ∂_{x} f : (a : 𝓢(E, ℂ)) → F) u : F)
⊢ ∂_{r • x} f = r • ∂_{x} f

Tactic:
ext u
-- Module: Mathlib.Analysis.Distribution.TemperedDistribution
Goal:
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
F : Type u_4
F₁ : Type u_5
F₂ : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace ℂ F
r : ℝ
x : E
f : 𝓢'(E, F)
u : 𝓢(E, ℂ)
⊢ Eq.{u_4 + 1} (α := F) ((∂_{r • x} f : (a : 𝓢(E, ℂ)) → F) u : F) ((r • ∂_{x} f : (a : 𝓢(E, ℂ)) → F) u : F)

Tactic:
simp [lineDerivOp_left_smul, map_smul_of_tower f]

Premises used: ContinuousLinearMap.map_smul_of_tower, LineDerivLeftSMul.lineDerivOp_left_smul
-- Module: Mathlib.Analysis.Distribution.TemperedDistribution
Goal:
E : Type u_3
F : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace ℂ F
m : E
⊢ Eq (α := 𝓢'(E, F) →L[ℂ] 𝓢'(E, F)) (lineDerivOpCLM ℂ 𝓢'(E, F) m)
    (PointwiseConvergenceCLM.precomp F (-lineDerivOpCLM ℂ 𝓢(E, ℂ) m))

Tactic:
rfl

Premises used: ContinuousLinearMap.comp, PointwiseConvergenceCLM.precomp, LineDeriv.lineDerivOpCLM, rfl
-- Module: Mathlib.Analysis.Distribution.TemperedDistribution
Goal:
E : Type u_3
F : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace ℂ F
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : SecondCountableTopology E
inst_7 : FiniteDimensional ℝ E
μ : Measure E
inst_8 : μ.IsAddHaarMeasure
f : 𝓢(E, F)
m : E
h :
  ∀ (g : 𝓢(E, ℂ)),
    Eq.{u_4 + 1} (α := F)
      ((lineDerivOp (E := 𝓢'(E, F)) m ((toTemperedDistributionCLM E F μ : (a : 𝓢(E, F)) → 𝓢'(E, F)) f : 𝓢'(E, F)) :
            (a : 𝓢(E, ℂ)) → F)
          g :
        F)
      ((((toTemperedDistributionCLM E F μ : (a : 𝓢(E, F)) → 𝓢'(E, F)) (∂_{m} f) : 𝓢'(E, F)) : (a : 𝓢(E, ℂ)) → F) g : F)
⊢ lineDerivOp (E := 𝓢'(E, F)) m ((toTemperedDistributionCLM E F μ : (a : 𝓢(E, F)) → 𝓢'(E, F)) f : 𝓢'(E, F)) =
    (toTemperedDistributionCLM E F μ : (a : 𝓢(E, F)) → 𝓢'(E, F)) (∂_{m} f)

Tactic:
ext1 g
-- Module: Mathlib.Analysis.Distribution.TemperedDistribution
Goal:
E : Type u_3
F : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace ℂ F
inst_4 : MeasurableSpace E
inst_5 : BorelSpace E
inst_6 : SecondCountableTopology E
inst_7 : FiniteDimensional ℝ E
μ : Measure E
inst_8 : μ.IsAddHaarMeasure
f : 𝓢(E, F)
m : E
g : 𝓢(E, ℂ)
⊢ Eq.{u_4 + 1} (α := F)
    ((lineDerivOp (E := 𝓢'(E, F)) m ((toTemperedDistributionCLM E F μ : (a : 𝓢(E, F)) → 𝓢'(E, F)) f : 𝓢'(E, F)) :
          (a : 𝓢(E, ℂ)) → F)
        g :
      F)
    ((((toTemperedDistributionCLM E F μ : (a : 𝓢(E, F)) → 𝓢'(E, F)) (∂_{m} f) : 𝓢'(E, F)) : (a : 𝓢(E, ℂ)) → F) g : F)

Tactic:
simp [integral_smul_lineDerivOp_right_eq_neg_left g f, integral_neg]

Premises used: MeasureTheory.integral_neg, SchwartzMap.integral_smul_lineDerivOp_right_eq_neg_left
-- Module: Mathlib.Analysis.Distribution.TemperedDistribution
Goal:
E : Type u_3
F : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : FiniteDimensional ℝ E
inst_4 : NormedSpace ℂ F
f : 𝓢'(E, F)
⊢ (laplacianCLM ℂ E 𝓢'(E, F) : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f = Δ f

Tactic:
simp [laplacianCLM, laplacian]

Premises used: Laplacian.laplacian, LineDeriv.laplacianCLM
-- Module: Mathlib.Analysis.Distribution.TemperedDistribution
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 : FiniteDimensional ℝ E
inst_4 : NormedSpace ℂ F
inst_5 : Fintype ι
b : OrthonormalBasis ι ℝ E
f : 𝓢'(E, F)
⊢ Δ f = ∑ i : ι, lineDerivOp (V := E) ((b : (a : ι) → E) i : E) (lineDerivOp (V := E) ((b : (a : ι) → E) i : E) f)

Tactic:
LineDeriv.laplacianCLM_eq_sum b f

Premises used: LineDeriv.laplacianCLM_eq_sum
-- Module: Mathlib.Analysis.Distribution.TemperedDistribution
Goal:
E : Type u_3
F : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : FiniteDimensional ℝ E
inst_4 : NormedSpace ℂ F
f : 𝓢'(E, F)
u : 𝓢(E, ℂ)
⊢ Eq.{u_4 + 1} (α := F) ((Δ f : (a : 𝓢(E, ℂ)) → F) u : F) ((f : (a : 𝓢(E, ℂ)) → F) (Δ u) : F)

Tactic:
simp [laplacian_eq_sum (stdOrthonormalBasis ℝ E),
    SchwartzMap.laplacian_eq_sum (stdOrthonormalBasis ℝ E),
    UniformConvergenceCLM.sum_apply, map_neg, neg_neg]

Premises used: Real, neg_neg, map_neg, TemperedDistribution.laplacian_eq_sum, SchwartzMap.laplacian_eq_sum, UniformConvergenceCLM.sum_apply, stdOrthonormalBasis
-- Module: Mathlib.Analysis.Distribution.TemperedDistribution
Goal:
E : Type u_3
F : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : FiniteDimensional ℝ E
inst_4 : NormedSpace ℂ F
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
f : 𝓢(E, F)
h :
  ∀ (u : 𝓢(E, ℂ)),
    Eq.{u_4 + 1} (α := F)
      ((Δ (E := 𝓢'(E, F)) ((toTemperedDistributionCLM E F volume : (a : 𝓢(E, F)) → 𝓢'(E, F)) f : 𝓢'(E, F)) :
            (a : 𝓢(E, ℂ)) → F)
          u :
        F)
      ((((toTemperedDistributionCLM E F volume : (a : 𝓢(E, F)) → 𝓢'(E, F)) (Δ f) : 𝓢'(E, F)) : (a : 𝓢(E, ℂ)) → F) u : F)
⊢ Δ (E := 𝓢'(E, F)) ((toTemperedDistributionCLM E F volume : (a : 𝓢(E, F)) → 𝓢'(E, F)) f : 𝓢'(E, F)) =
    (toTemperedDistributionCLM E F volume : (a : 𝓢(E, F)) → 𝓢'(E, F)) (Δ f)

Tactic:
ext u
-- Module: Mathlib.Analysis.Distribution.TemperedDistribution
Goal:
E : Type u_3
F : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : FiniteDimensional ℝ E
inst_4 : NormedSpace ℂ F
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
f : 𝓢(E, F)
u : 𝓢(E, ℂ)
⊢ Eq.{u_4 + 1} (α := F)
    ((Δ (E := 𝓢'(E, F)) ((toTemperedDistributionCLM E F volume : (a : 𝓢(E, F)) → 𝓢'(E, F)) f : 𝓢'(E, F)) :
          (a : 𝓢(E, ℂ)) → F)
        u :
      F)
    ((((toTemperedDistributionCLM E F volume : (a : 𝓢(E, F)) → 𝓢'(E, F)) (Δ f) : 𝓢'(E, F)) : (a : 𝓢(E, ℂ)) → F) u : F)

Tactic:
simp [SchwartzMap.integral_smul_laplacian_right_eq_left]

Premises used: SchwartzMap.integral_smul_laplacian_right_eq_left
-- Module: Mathlib.Analysis.Distribution.TemperedDistribution
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)
g : 𝓢(E, ℂ)
⊢ Eq.{u_4 + 1} (α := F) ((𝓕 f : (a : 𝓢(E, ℂ)) → F) g : F) ((f : (a : 𝓢(E, ℂ)) → F) (𝓕 g) : F)

Tactic:
rfl

Premises used: ContinuousLinearMap.comp, VectorFourier.fourierIntegral, UniformConvergenceCLM, rfl
-- Module: Mathlib.Analysis.Distribution.TemperedDistribution
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)
g : 𝓢(E, ℂ)
⊢ Eq.{u_4 + 1} (α := F) ((𝓕⁻ f : (a : 𝓢(E, ℂ)) → F) g : F) ((f : (a : 𝓢(E, ℂ)) → F) (𝓕⁻ g) : F)

Tactic:
rfl

Premises used: ContinuousLinearMap.comp, VectorFourier.fourierIntegral, UniformConvergenceCLM, rfl
-- Module: Mathlib.Analysis.Distribution.TemperedDistribution
Goal:
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
F : Type u_4
F₁ : Type u_5
F₂ : Type u_6
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)
h : ∀ (x : 𝓢(E, ℂ)), Eq.{u_4 + 1} (α := F) ((𝓕⁻ (𝓕 f) : (a : 𝓢(E, ℂ)) → F) x : F) ((f : (a : 𝓢(E, ℂ)) → F) x : F)
⊢ 𝓕⁻ (𝓕 f) = f

Tactic:
ext
-- Module: Mathlib.Analysis.Distribution.TemperedDistribution
Goal:
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
F : Type u_4
F₁ : Type u_5
F₂ : Type u_6
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)
x : 𝓢(E, ℂ)
⊢ Eq.{u_4 + 1} (α := F) ((𝓕⁻ (𝓕 f) : (a : 𝓢(E, ℂ)) → F) x : F) ((f : (a : 𝓢(E, ℂ)) → F) x : F)

Tactic:
simp
-- Module: Mathlib.Analysis.Distribution.TemperedDistribution
Goal:
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
F : Type u_4
F₁ : Type u_5
F₂ : Type u_6
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)
h : ∀ (x : 𝓢(E, ℂ)), Eq.{u_4 + 1} (α := F) ((𝓕 (𝓕⁻ f) : (a : 𝓢(E, ℂ)) → F) x : F) ((f : (a : 𝓢(E, ℂ)) → F) x : F)
⊢ 𝓕 (𝓕⁻ f) = f

Tactic:
ext
-- Module: Mathlib.Analysis.Distribution.TemperedDistribution
Goal:
ι : Type u_1
𝕜 : Type u_2
E : Type u_3
F : Type u_4
F₁ : Type u_5
F₂ : Type u_6
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)
x : 𝓢(E, ℂ)
⊢ Eq.{u_4 + 1} (α := F) ((𝓕 (𝓕⁻ f) : (a : 𝓢(E, ℂ)) → F) x : F) ((f : (a : 𝓢(E, ℂ)) → F) x : F)

Tactic:
simp
-- Module: Mathlib.Analysis.Distribution.TemperedDistribution
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)
h :
  ∀ (g : 𝓢(E, ℂ)),
    Eq.{u_4 + 1} (α := F)
      ((𝓕 (E := 𝓢'(E, F)) ((toTemperedDistributionCLM E F volume : (a : 𝓢(E, F)) → 𝓢'(E, F)) f : 𝓢'(E, F)) :
            (a : 𝓢(E, ℂ)) → F)
          g :
        F)
      ((((toTemperedDistributionCLM E F volume : (a : 𝓢(E, F)) → 𝓢'(E, F)) (𝓕 f) : 𝓢'(E, F)) : (a : 𝓢(E, ℂ)) → F) g : F)
⊢ 𝓕 (E := 𝓢'(E, F)) ((toTemperedDistributionCLM E F volume : (a : 𝓢(E, F)) → 𝓢'(E, F)) f : 𝓢'(E, F)) =
    (toTemperedDistributionCLM E F volume : (a : 𝓢(E, F)) → 𝓢'(E, F)) (𝓕 f)

Tactic:
ext g
-- Module: Mathlib.Analysis.Distribution.TemperedDistribution
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)
g : 𝓢(E, ℂ)
⊢ Eq.{u_4 + 1} (α := F)
    ((𝓕 (E := 𝓢'(E, F)) ((toTemperedDistributionCLM E F volume : (a : 𝓢(E, F)) → 𝓢'(E, F)) f : 𝓢'(E, F)) :
          (a : 𝓢(E, ℂ)) → F)
        g :
      F)
    ((((toTemperedDistributionCLM E F volume : (a : 𝓢(E, F)) → 𝓢'(E, F)) (𝓕 f) : 𝓢'(E, F)) : (a : 𝓢(E, ℂ)) → F) g : F)

Tactic:
simpa using integral_fourier_smul_eq g f

Premises used: SchwartzMap.integral_fourier_smul_eq
-- Module: Mathlib.Analysis.Distribution.TemperedDistribution
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)
e_a : f = 𝓕 (𝓕⁻ f)
⊢ 𝓕⁻ (E := 𝓢'(E, F)) ((toTemperedDistributionCLM E F volume : (a : 𝓢(E, F)) → 𝓢'(E, F)) f : 𝓢'(E, F)) =
    𝓕⁻ (E := 𝓢'(E, F)) ((toTemperedDistributionCLM E F volume : (a : 𝓢(E, F)) → 𝓢'(E, F)) (𝓕 (𝓕⁻ f)) : 𝓢'(E, F))

Tactic:
congr
-- Module: Mathlib.Analysis.Distribution.TemperedDistribution
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)
⊢ f = 𝓕 (𝓕⁻ f)

Tactic:
(fourier_fourierInv_eq f).symm

Premises used: FourierInvPair.fourier_fourierInv_eq, Eq.symm
-- Module: Mathlib.Analysis.Distribution.TemperedDistribution
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)
⊢ f = 𝓕 (𝓕⁻ f)

Tactic:
exact (fourier_fourierInv_eq f).symm

Premises used: FourierInvPair.fourier_fourierInv_eq, Eq.symm
-- Module: Mathlib.Analysis.Distribution.TemperedDistribution
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)
rw rw₁ :
  𝓕⁻ (E := 𝓢'(E, F)) ((toTemperedDistributionCLM E F volume : (a : 𝓢(E, F)) → 𝓢'(E, F)) (𝓕 (𝓕⁻ f)) : 𝓢'(E, F)) =
    𝓕⁻ (E := 𝓢'(E, F)) ((toTemperedDistributionCLM E F volume : (a : 𝓢(E, F)) → 𝓢'(E, F)) (𝓕 (𝓕⁻ f)) : 𝓢'(E, F))
⊢ 𝓕⁻ (E := 𝓢'(E, F)) ((toTemperedDistributionCLM E F volume : (a : 𝓢(E, F)) → 𝓢'(E, F)) (𝓕 (𝓕⁻ f)) : 𝓢'(E, F)) =
    𝓕⁻ (𝓕 (E := 𝓢'(E, F)) ((toTemperedDistributionCLM E F volume : (a : 𝓢(E, F)) → 𝓢'(E, F)) (𝓕⁻ f) : 𝓢'(E, F)))

Tactic:
rw [fourier_toTemperedDistributionCLM_eq]

Premises used: TemperedDistribution.fourier_toTemperedDistributionCLM_eq
-- Module: Mathlib.Analysis.Distribution.TemperedDistribution
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)
m : E
h :
  ∀ (u : 𝓢(E, ℂ)),
    Eq.{u_4 + 1} (α := F) ((∂_{m} (𝓕 f) : (a : 𝓢(E, ℂ)) → F) u : F)
      ((𝓕
              (HSMul.hSMul (β := 𝓢'(E, F)) (-(2 * (↑π : ℂ) * Complex.I))
                ((smulLeftCLM F fun (x : E) ↦ (↑(inner ℝ x m) : ℂ) : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f : 𝓢'(E, F))) :
            (a : 𝓢(E, ℂ)) → F)
          u :
        F)
⊢ ∂_{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:
ext u
-- Module: Mathlib.Analysis.Distribution.TemperedDistribution
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)
m : E
u : 𝓢(E, ℂ)
⊢ Function.HasTemperateGrowth (F := ℝ) fun (x : E) ↦ inner ℝ x m

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Distribution.TemperedDistribution
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)
m : E
u : 𝓢(E, ℂ)
⊢ Function.HasTemperateGrowth (F := ℝ) fun (x : E) ↦ inner ℝ x m

Tactic:
have : (inner ℝ · m).HasTemperateGrowth := by fun_prop
-- Module: Mathlib.Analysis.Distribution.TemperedDistribution
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)
m : E
u : 𝓢(E, ℂ)
this : Function.HasTemperateGrowth (F := ℝ) fun (x : E) ↦ inner ℝ x m
⊢ Eq.{u_4 + 1} (α := F) ((∂_{m} (𝓕 f) : (a : 𝓢(E, ℂ)) → F) u : F)
    ((𝓕
            (HSMul.hSMul (β := 𝓢'(E, F)) (-(2 * (↑π : ℂ) * Complex.I))
              ((smulLeftCLM F fun (x : E) ↦ (↑(inner ℝ x m) : ℂ) : (a : 𝓢'(E, F)) → 𝓢'(E, F)) f : 𝓢'(E, F))) :
          (a : 𝓢(E, ℂ)) → F)
        u :
      F)

Tactic:
simp [SchwartzMap.fourier_lineDerivOp_eq, ← smulLeftCLM_ofReal ℂ this]

Premises used: SchwartzMap.fourier_lineDerivOp_eq, Complex, SchwartzMap.smulLeftCLM_ofReal
-- Module: Mathlib.Analysis.Distribution.TemperedDistribution
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)
m : E
h :
  ∀ (u : 𝓢(E, ℂ)),
    Eq.{u_4 + 1} (α := F) ((𝓕 (∂_{m} f) : (a : 𝓢(E, ℂ)) → F) u : F)
      ((HSMul.hSMul (β := 𝓢'(E, F)) (2 * (↑π : ℂ) * Complex.I)
              ((smulLeftCLM F fun (x : E) ↦ (↑(inner ℝ x m) : ℂ) : (a : 𝓢'(E, F)) → 𝓢'(E, F)) (𝓕 f) : 𝓢'(E, F)) :
            (a : 𝓢(E, ℂ)) → F)
          u :
        F)
⊢ 𝓕 (∂_{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:
ext u
-- Module: Mathlib.Analysis.Distribution.TemperedDistribution
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)
m : E
u : 𝓢(E, ℂ)
this : Function.HasTemperateGrowth (F := ℝ) fun (x : E) ↦ inner ℝ x m
⊢ Eq.{u_4 + 1} (α := F) ((𝓕 (∂_{m} f) : (a : 𝓢(E, ℂ)) → F) u : F)
    ((HSMul.hSMul (β := 𝓢'(E, F)) (2 * (↑π : ℂ) * Complex.I)
            ((smulLeftCLM F fun (x : E) ↦ (↑(inner ℝ x m) : ℂ) : (a : 𝓢'(E, F)) → 𝓢'(E, F)) (𝓕 f) : 𝓢'(E, F)) :
          (a : 𝓢(E, ℂ)) → F)
        u :
      F)

Tactic:
simp [SchwartzMap.lineDerivOp_fourier_eq, ← smulLeftCLM_ofReal ℂ this]

Premises used: SchwartzMap.lineDerivOp_fourier_eq, Complex, SchwartzMap.smulLeftCLM_ofReal