awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
D : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
H : Type u_8
V : Type u_9
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedAlgebra ℝ 𝕜
inst_6 : NormedAddCommGroup D
inst_7 : NormedSpace ℝ D
inst_8 : NormedAddCommGroup G
inst_9 : NormedSpace ℝ G
inst_10 : NormedSpace 𝕜 F
inst_11 : NormedSpace 𝕜 E
inst_12 : NormedSpace 𝕜 G
B : E →L[𝕜] F →L[𝕜] G
g : D → F
hg : Function.HasTemperateGrowth g
k n l : ℕ
C : ℝ
hC : 0 ≤ C
f : 𝓢(D, E)
x : D
hxk : 0 ≤ ‖x‖ ^ k
hnorm_mul :
  norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_7} ℝ (fun (i : Fin n) ↦ D) G)
      (iteratedFDeriv ℝ n
        (fun (y : D) ↦
          (((ContinuousLinearMap.bilinearRestrictScalars ℝ B : (a : E) → F →L[ℝ] G) ((f : (a : D) → E) y) : F →L[ℝ] G) :
              (a : F) → G)
            (g y))
        x) ≤
    norm (E := E →L[ℝ] F →L[ℝ] G) (ContinuousLinearMap.bilinearRestrictScalars ℝ B) *
      ∑ i ∈ Finset.range (n + 1),
        (↑(n.choose i) : ℝ) *
            norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_5} ℝ (fun (i : Fin i) ↦ D) E)
              (iteratedFDeriv ℝ i (⇑f : (a : D) → E) x) *
          norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_6} ℝ (fun (i : Fin (n - i)) ↦ D) F)
            (iteratedFDeriv ℝ (n - i) g x)
this : ∑ _x ∈ Finset.range (n + 1), 1 = HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
i : ℕ
hgrowth :
  norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_6} ℝ (fun (i : Fin (n - i)) ↦ D) F) (iteratedFDeriv ℝ (n - i) g x) ≤
    C * (1 + ‖x‖) ^ l
hi : i ≤ (l + k, n).2
right : ‖x‖ ≤ 1 + ‖x‖
⊢ ‖x‖ ^ k *
        norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_5} ℝ (fun (i : Fin i) ↦ D) E)
          (iteratedFDeriv ℝ i (⇑f : (a : D) → E) x) *
      (1 + ‖x‖) ^ l ≤
    (1 + ‖x‖) ^ k *
        norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_5} ℝ (fun (i : Fin i) ↦ D) E)
          (iteratedFDeriv ℝ i (⇑f : (a : D) → E) x) *
      (1 + ‖x‖) ^ l

Tactic:
gcongr
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
D : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
H : Type u_8
V : Type u_9
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedAlgebra ℝ 𝕜
inst_6 : NormedAddCommGroup D
inst_7 : NormedSpace ℝ D
inst_8 : NormedAddCommGroup G
inst_9 : NormedSpace ℝ G
inst_10 : NormedSpace 𝕜 F
inst_11 : NormedSpace 𝕜 E
inst_12 : NormedSpace 𝕜 G
B : E →L[𝕜] F →L[𝕜] G
g : D → F
hg : Function.HasTemperateGrowth g
k n l : ℕ
C : ℝ
hC : 0 ≤ C
f : 𝓢(D, E)
x : D
hxk : 0 ≤ ‖x‖ ^ k
hnorm_mul :
  norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_7} ℝ (fun (i : Fin n) ↦ D) G)
      (iteratedFDeriv ℝ n
        (fun (y : D) ↦
          (((ContinuousLinearMap.bilinearRestrictScalars ℝ B : (a : E) → F →L[ℝ] G) ((f : (a : D) → E) y) : F →L[ℝ] G) :
              (a : F) → G)
            (g y))
        x) ≤
    norm (E := E →L[ℝ] F →L[ℝ] G) (ContinuousLinearMap.bilinearRestrictScalars ℝ B) *
      ∑ i ∈ Finset.range (n + 1),
        (↑(n.choose i) : ℝ) *
            norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_5} ℝ (fun (i : Fin i) ↦ D) E)
              (iteratedFDeriv ℝ i (⇑f : (a : D) → E) x) *
          norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_6} ℝ (fun (i : Fin (n - i)) ↦ D) F)
            (iteratedFDeriv ℝ (n - i) g x)
this : ∑ _x ∈ Finset.range (n + 1), 1 = HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
i : ℕ
hgrowth :
  norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_6} ℝ (fun (i : Fin (n - i)) ↦ D) F) (iteratedFDeriv ℝ (n - i) g x) ≤
    C * (1 + ‖x‖) ^ l
hi : i ≤ (l + k, n).2
⊢ ‖x‖ ≤ 1 + ‖x‖

Tactic:
simp
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
𝕜 : Type u_2
D : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedAlgebra ℝ 𝕜
inst_6 : NormedAddCommGroup D
inst_7 : NormedSpace ℝ D
inst_8 : NormedAddCommGroup G
inst_9 : NormedSpace ℝ G
inst_10 : NormedSpace 𝕜 F
inst_11 : NormedSpace 𝕜 E
inst_12 : NormedSpace 𝕜 G
B : E →L[𝕜] F →L[𝕜] G
g : D → F
hg : Function.HasTemperateGrowth g
f : 𝓢(D, E)
⊢ Eq (α := (a : D) → G)
    (⇑(((bilinLeftCLM B hg : 𝓢(D, E) →L[𝕜] 𝓢(D, G)) : (a : 𝓢(D, E)) → 𝓢(D, G)) f : 𝓢(D, G)) : (a : D) → G) fun (x : D) ↦
    (((B : (a : E) → F →L[𝕜] G) ((f : (a : D) → E) x) : F →L[𝕜] G) : (a : F) → G) (g x)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
𝕜 : Type u_2
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedAlgebra ℝ 𝕜
inst_6 : NormedSpace 𝕜 F
g : E → 𝕜
hg : Function.HasTemperateGrowth g
f : 𝓢(E, F)
⊢ Eq (α := (a : E) → F)
    (⇑(((smulLeftCLM F g : 𝓢(E, F) →L[𝕜] 𝓢(E, F)) : (a : 𝓢(E, F)) → 𝓢(E, F)) f : 𝓢(E, F)) : (a : E) → F) fun (x : E) ↦
    HSMul.hSMul (β := F) (g x) ((f : (a : E) → F) x : F)

Tactic:
simp [smulLeftCLM, hg]

Premises used: SchwartzMap.smulLeftCLM
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
𝕜 : Type u_2
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedAlgebra ℝ 𝕜
inst_6 : NormedSpace 𝕜 F
g : E → 𝕜
hg : Function.HasTemperateGrowth g
f : 𝓢(E, F)
x : E
⊢ ((((smulLeftCLM F g : 𝓢(E, F) →L[𝕜] 𝓢(E, F)) : (a : 𝓢(E, F)) → 𝓢(E, F)) f : 𝓢(E, F)) : (a : E) → F) x =
    HSMul.hSMul (β := F) (g x) ((f : (a : E) → F) x : F)

Tactic:
simp [smulLeftCLM_apply hg]

Premises used: SchwartzMap.smulLeftCLM_apply
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
𝕜 : Type u_2
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedAlgebra ℝ 𝕜
inst_6 : NormedSpace 𝕜 F
c : 𝕜
h :
  ∀ (f : 𝓢(E, F)) (x : E),
    Eq.{u_6 + 1} (α := F)
      (((((smulLeftCLM F fun (x : E) ↦ c : 𝓢(E, F) →L[𝕜] 𝓢(E, F)) : (a : 𝓢(E, F)) → 𝓢(E, F)) f : 𝓢(E, F)) : (a : E) → F)
          x :
        F)
      ((((HSMul.hSMul (β := 𝓢(E, F) →L[𝕜] 𝓢(E, F)) c (ContinuousLinearMap.id 𝕜 𝓢(E, F)) : (a : 𝓢(E, F)) → 𝓢(E, F)) f :
              𝓢(E, F)) :
            (a : E) → F)
          x :
        F)
⊢ (smulLeftCLM F fun (x : E) ↦ c) = HSMul.hSMul (β := 𝓢(E, F) →L[𝕜] 𝓢(E, F)) c (ContinuousLinearMap.id 𝕜 𝓢(E, F))

Tactic:
ext f x
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
𝕜 : Type u_2
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedAlgebra ℝ 𝕜
inst_6 : NormedSpace 𝕜 F
c : 𝕜
f : 𝓢(E, F)
x : E
⊢ Function.HasTemperateGrowth.{u_5, u_2} (F := 𝕜) fun (x : E) ↦ c

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
𝕜 : Type u_2
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedAlgebra ℝ 𝕜
inst_6 : NormedSpace 𝕜 F
c : 𝕜
f : 𝓢(E, F)
x : E
⊢ Function.HasTemperateGrowth.{u_5, u_2} (F := 𝕜) fun (x : E) ↦ c

Tactic:
have : (fun (_ : E) ↦ c).HasTemperateGrowth := by fun_prop
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
𝕜 : Type u_2
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedAlgebra ℝ 𝕜
inst_6 : NormedSpace 𝕜 F
c : 𝕜
f : 𝓢(E, F)
x : E
this : Function.HasTemperateGrowth.{u_5, u_2} (F := 𝕜) fun (x : E) ↦ c
⊢ Eq.{u_6 + 1} (α := F)
    (((((smulLeftCLM F fun (x : E) ↦ c : 𝓢(E, F) →L[𝕜] 𝓢(E, F)) : (a : 𝓢(E, F)) → 𝓢(E, F)) f : 𝓢(E, F)) : (a : E) → F)
        x :
      F)
    ((((HSMul.hSMul (β := 𝓢(E, F) →L[𝕜] 𝓢(E, F)) c (ContinuousLinearMap.id 𝕜 𝓢(E, F)) : (a : 𝓢(E, F)) → 𝓢(E, F)) f :
            𝓢(E, F)) :
          (a : E) → F)
        x :
      F)

Tactic:
simp [this]
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
𝕜 : Type u_2
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedAlgebra ℝ 𝕜
inst_6 : NormedSpace 𝕜 F
g₁ g₂ : E → 𝕜
hg₁ : Function.HasTemperateGrowth g₁
hg₂ : Function.HasTemperateGrowth g₂
f : 𝓢(E, F)
h :
  ∀ (x : E),
    Eq.{u_6 + 1} (α := F)
      (((((smulLeftCLM F g₁ : 𝓢(E, F) →L[𝕜] 𝓢(E, F)) : (a : 𝓢(E, F)) → 𝓢(E, F))
                (((smulLeftCLM F g₂ : 𝓢(E, F) →L[𝕜] 𝓢(E, F)) : (a : 𝓢(E, F)) → 𝓢(E, F)) f) :
              𝓢(E, F)) :
            (a : E) → F)
          x :
        F)
      (((((smulLeftCLM F (g₁ * g₂) : 𝓢(E, F) →L[𝕜] 𝓢(E, F)) : (a : 𝓢(E, F)) → 𝓢(E, F)) f : 𝓢(E, F)) : (a : E) → F) x :
        F)
⊢ Eq (α := 𝓢(E, F))
    (((smulLeftCLM F g₁ : 𝓢(E, F) →L[𝕜] 𝓢(E, F)) : (a : 𝓢(E, F)) → 𝓢(E, F))
        (((smulLeftCLM F g₂ : 𝓢(E, F) →L[𝕜] 𝓢(E, F)) : (a : 𝓢(E, F)) → 𝓢(E, F)) f) :
      𝓢(E, F))
    (((smulLeftCLM F (g₁ * g₂) : 𝓢(E, F) →L[𝕜] 𝓢(E, F)) : (a : 𝓢(E, F)) → 𝓢(E, F)) f : 𝓢(E, F))

Tactic:
ext x
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
𝕜 : Type u_2
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedAlgebra ℝ 𝕜
inst_6 : NormedSpace 𝕜 F
g₁ g₂ : E → 𝕜
hg₁ : Function.HasTemperateGrowth g₁
hg₂ : Function.HasTemperateGrowth g₂
f : 𝓢(E, F)
x : E
⊢ Eq.{u_6 + 1} (α := F)
    (((((smulLeftCLM F g₁ : 𝓢(E, F) →L[𝕜] 𝓢(E, F)) : (a : 𝓢(E, F)) → 𝓢(E, F))
              (((smulLeftCLM F g₂ : 𝓢(E, F) →L[𝕜] 𝓢(E, F)) : (a : 𝓢(E, F)) → 𝓢(E, F)) f) :
            𝓢(E, F)) :
          (a : E) → F)
        x :
      F)
    (((((smulLeftCLM F (g₁ * g₂) : 𝓢(E, F) →L[𝕜] 𝓢(E, F)) : (a : 𝓢(E, F)) → 𝓢(E, F)) f : 𝓢(E, F)) : (a : E) → F) x : F)

Tactic:
simp [smul_smul, hg₁, hg₂, hg₁.mul hg₂]

Premises used: smul_smul, Function.HasTemperateGrowth.mul
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
𝕜 : Type u_2
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedAlgebra ℝ 𝕜
inst_6 : NormedSpace 𝕜 F
g₁ g₂ : E → 𝕜
hg₁ : Function.HasTemperateGrowth g₁
hg₂ : Function.HasTemperateGrowth g₂
h :
  ∀ (f : 𝓢(E, F)),
    Eq (α := 𝓢(E, F))
      ((((smulLeftCLM F g₁ : 𝓢(E, F) →L[𝕜] 𝓢(E, F)) ∘SL (smulLeftCLM F g₂ : 𝓢(E, F) →L[𝕜] 𝓢(E, F)) :
              𝓢(E, F) →L[𝕜] 𝓢(E, F)) :
            (a : 𝓢(E, F)) → 𝓢(E, F))
          f :
        𝓢(E, F))
      (((smulLeftCLM F (g₁ * g₂) : 𝓢(E, F) →L[𝕜] 𝓢(E, F)) : (a : 𝓢(E, F)) → 𝓢(E, F)) f : 𝓢(E, F))
⊢ Eq (α := 𝓢(E, F) →L[𝕜] 𝓢(E, F))
    ((smulLeftCLM F g₁ : 𝓢(E, F) →L[𝕜] 𝓢(E, F)) ∘SL (smulLeftCLM F g₂ : 𝓢(E, F) →L[𝕜] 𝓢(E, F)) : 𝓢(E, F) →L[𝕜] 𝓢(E, F))
    (smulLeftCLM F (g₁ * g₂) : 𝓢(E, F) →L[𝕜] 𝓢(E, F))

Tactic:
ext1 f
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
𝕜 : Type u_2
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedAlgebra ℝ 𝕜
inst_6 : NormedSpace 𝕜 F
g₁ g₂ : E → 𝕜
hg₁ : Function.HasTemperateGrowth g₁
hg₂ : Function.HasTemperateGrowth g₂
f : 𝓢(E, F)
⊢ Eq (α := 𝓢(E, F))
    ((((smulLeftCLM F g₁ : 𝓢(E, F) →L[𝕜] 𝓢(E, F)) ∘SL (smulLeftCLM F g₂ : 𝓢(E, F) →L[𝕜] 𝓢(E, F)) :
            𝓢(E, F) →L[𝕜] 𝓢(E, F)) :
          (a : 𝓢(E, F)) → 𝓢(E, F))
        f :
      𝓢(E, F))
    (((smulLeftCLM F (g₁ * g₂) : 𝓢(E, F) →L[𝕜] 𝓢(E, F)) : (a : 𝓢(E, F)) → 𝓢(E, F)) f : 𝓢(E, F))

Tactic:
smulLeftCLM_smulLeftCLM_apply hg₁ hg₂ f

Premises used: SchwartzMap.smulLeftCLM_smulLeftCLM_apply
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
𝕜 : Type u_2
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedAlgebra ℝ 𝕜
inst_6 : NormedSpace 𝕜 F
g₁ g₂ : E → 𝕜
hg₁ : Function.HasTemperateGrowth g₁
hg₂ : Function.HasTemperateGrowth g₂
f : 𝓢(E, F)
⊢ Eq (α := 𝓢(E, F))
    ((((smulLeftCLM F g₁ : 𝓢(E, F) →L[𝕜] 𝓢(E, F)) ∘SL (smulLeftCLM F g₂ : 𝓢(E, F) →L[𝕜] 𝓢(E, F)) :
            𝓢(E, F) →L[𝕜] 𝓢(E, F)) :
          (a : 𝓢(E, F)) → 𝓢(E, F))
        f :
      𝓢(E, F))
    (((smulLeftCLM F (g₁ * g₂) : 𝓢(E, F) →L[𝕜] 𝓢(E, F)) : (a : 𝓢(E, F)) → 𝓢(E, F)) f : 𝓢(E, F))

Tactic:
exact smulLeftCLM_smulLeftCLM_apply hg₁ hg₂ f

Premises used: SchwartzMap.smulLeftCLM_smulLeftCLM_apply
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
𝕜 : Type u_2
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedAlgebra ℝ 𝕜
inst_6 : NormedSpace 𝕜 F
g : E → 𝕜
hg : Function.HasTemperateGrowth g
c : 𝕜
⊢ Function.HasTemperateGrowth.{u_5, u_2} (F := 𝕜) fun (x : E) ↦ c

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
𝕜 : Type u_2
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedAlgebra ℝ 𝕜
inst_6 : NormedSpace 𝕜 F
g : E → 𝕜
hg : Function.HasTemperateGrowth g
c : 𝕜
⊢ Function.HasTemperateGrowth.{u_5, u_2} (F := 𝕜) fun (x : E) ↦ c

Tactic:
have : (fun (_ : E) ↦ c).HasTemperateGrowth := by fun_prop
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
𝕜 : Type u_2
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedAlgebra ℝ 𝕜
inst_6 : NormedSpace 𝕜 F
g : E → 𝕜
hg : Function.HasTemperateGrowth g
c : 𝕜
this : Function.HasTemperateGrowth.{u_5, u_2} (F := 𝕜) fun (x : E) ↦ c
⊢ Eq (α := 𝓢(E, F) →L[𝕜] 𝓢(E, F)) (smulLeftCLM F ((fun (x : E) ↦ c) * g) : 𝓢(E, F) →L[𝕜] 𝓢(E, F))
    ((smulLeftCLM F fun (x : E) ↦ c : 𝓢(E, F) →L[𝕜] 𝓢(E, F)) ∘SL (smulLeftCLM F g : 𝓢(E, F) →L[𝕜] 𝓢(E, F)) :
      𝓢(E, F) →L[𝕜] 𝓢(E, F))

Tactic:
(smulLeftCLM_compL_smulLeftCLM this hg).symm

Premises used: Eq.symm, SchwartzMap.smulLeftCLM_compL_smulLeftCLM
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
𝕜 : Type u_2
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedAlgebra ℝ 𝕜
inst_6 : NormedSpace 𝕜 F
g : E → 𝕜
hg : Function.HasTemperateGrowth g
c : 𝕜
this : Function.HasTemperateGrowth.{u_5, u_2} (F := 𝕜) fun (x : E) ↦ c
h :
  HSMul.hSMul (β := 𝓢(E, F) →L[𝕜] 𝓢(E, F)) c (smulLeftCLM F g : 𝓢(E, F) →L[𝕜] 𝓢(E, F)) =
    (smulLeftCLM F fun (x : E) ↦ c : 𝓢(E, F) →L[𝕜] 𝓢(E, F)) ∘SL (smulLeftCLM F g : 𝓢(E, F) →L[𝕜] 𝓢(E, F))
⊢ smulLeftCLM F (c • g) = HSMul.hSMul (β := 𝓢(E, F) →L[𝕜] 𝓢(E, F)) c (smulLeftCLM F g : 𝓢(E, F) →L[𝕜] 𝓢(E, F))

Tactic:
convert! (smulLeftCLM_compL_smulLeftCLM this hg).symm using 1

Premises used: Eq.symm, SchwartzMap.smulLeftCLM_compL_smulLeftCLM
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
𝕜 : Type u_2
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedAlgebra ℝ 𝕜
inst_6 : NormedSpace 𝕜 F
g : E → 𝕜
hg : Function.HasTemperateGrowth g
c : 𝕜
this : Function.HasTemperateGrowth.{u_5, u_2} (F := 𝕜) fun (x : E) ↦ c
⊢ HSMul.hSMul (β := 𝓢(E, F) →L[𝕜] 𝓢(E, F)) c (smulLeftCLM F g : 𝓢(E, F) →L[𝕜] 𝓢(E, F)) =
    (smulLeftCLM F fun (x : E) ↦ c : 𝓢(E, F) →L[𝕜] 𝓢(E, F)) ∘SL (smulLeftCLM F g : 𝓢(E, F) →L[𝕜] 𝓢(E, F))

Tactic:
simp
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
𝕜 : Type u_2
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedAlgebra ℝ 𝕜
inst_6 : NormedSpace 𝕜 F
g₁ g₂ : E → 𝕜
hg₁ : Function.HasTemperateGrowth g₁
hg₂ : Function.HasTemperateGrowth g₂
h :
  ∀ (f : 𝓢(E, F)) (x : E),
    Eq.{u_6 + 1} (α := F)
      (((((smulLeftCLM F (g₁ + g₂) : 𝓢(E, F) →L[𝕜] 𝓢(E, F)) : (a : 𝓢(E, F)) → 𝓢(E, F)) f : 𝓢(E, F)) : (a : E) → F) x :
        F)
      ((((HAdd.hAdd (α := 𝓢(E, F) →L[𝕜] 𝓢(E, F)) (β := 𝓢(E, F) →L[𝕜] 𝓢(E, F)) (smulLeftCLM F g₁ : 𝓢(E, F) →L[𝕜] 𝓢(E, F))
                    (smulLeftCLM F g₂ : 𝓢(E, F) →L[𝕜] 𝓢(E, F)) :
                  (a : 𝓢(E, F)) → 𝓢(E, F))
                f :
              𝓢(E, F)) :
            (a : E) → F)
          x :
        F)
⊢ smulLeftCLM F (g₁ + g₂) =
    HAdd.hAdd (α := 𝓢(E, F) →L[𝕜] 𝓢(E, F)) (β := 𝓢(E, F) →L[𝕜] 𝓢(E, F)) (smulLeftCLM F g₁ : 𝓢(E, F) →L[𝕜] 𝓢(E, F))
      (smulLeftCLM F g₂ : 𝓢(E, F) →L[𝕜] 𝓢(E, F))

Tactic:
ext f x
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
𝕜 : Type u_2
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedAlgebra ℝ 𝕜
inst_6 : NormedSpace 𝕜 F
g₁ g₂ : E → 𝕜
hg₁ : Function.HasTemperateGrowth g₁
hg₂ : Function.HasTemperateGrowth g₂
f : 𝓢(E, F)
x : E
⊢ Eq.{u_6 + 1} (α := F)
    (((((smulLeftCLM F (g₁ + g₂) : 𝓢(E, F) →L[𝕜] 𝓢(E, F)) : (a : 𝓢(E, F)) → 𝓢(E, F)) f : 𝓢(E, F)) : (a : E) → F) x : F)
    ((((HAdd.hAdd (α := 𝓢(E, F) →L[𝕜] 𝓢(E, F)) (β := 𝓢(E, F) →L[𝕜] 𝓢(E, F)) (smulLeftCLM F g₁ : 𝓢(E, F) →L[𝕜] 𝓢(E, F))
                  (smulLeftCLM F g₂ : 𝓢(E, F) →L[𝕜] 𝓢(E, F)) :
                (a : 𝓢(E, F)) → 𝓢(E, F))
              f :
            𝓢(E, F)) :
          (a : E) → F)
        x :
      F)

Tactic:
simp [hg₁, hg₂, hg₁.add hg₂, add_smul]

Premises used: Function.HasTemperateGrowth.add, add_smul
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
𝕜 : Type u_2
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedAlgebra ℝ 𝕜
inst_6 : NormedSpace 𝕜 F
g₁ g₂ : E → 𝕜
hg₁ : Function.HasTemperateGrowth g₁
hg₂ : Function.HasTemperateGrowth g₂
h :
  ∀ (f : 𝓢(E, F)) (x : E),
    Eq.{u_6 + 1} (α := F)
      (((((smulLeftCLM F (g₁ - g₂) : 𝓢(E, F) →L[𝕜] 𝓢(E, F)) : (a : 𝓢(E, F)) → 𝓢(E, F)) f : 𝓢(E, F)) : (a : E) → F) x :
        F)
      ((((HSub.hSub (α := 𝓢(E, F) →L[𝕜] 𝓢(E, F)) (β := 𝓢(E, F) →L[𝕜] 𝓢(E, F)) (smulLeftCLM F g₁ : 𝓢(E, F) →L[𝕜] 𝓢(E, F))
                    (smulLeftCLM F g₂ : 𝓢(E, F) →L[𝕜] 𝓢(E, F)) :
                  (a : 𝓢(E, F)) → 𝓢(E, F))
                f :
              𝓢(E, F)) :
            (a : E) → F)
          x :
        F)
⊢ smulLeftCLM F (g₁ - g₂) =
    HSub.hSub (α := 𝓢(E, F) →L[𝕜] 𝓢(E, F)) (β := 𝓢(E, F) →L[𝕜] 𝓢(E, F)) (smulLeftCLM F g₁ : 𝓢(E, F) →L[𝕜] 𝓢(E, F))
      (smulLeftCLM F g₂ : 𝓢(E, F) →L[𝕜] 𝓢(E, F))

Tactic:
ext f x
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
𝕜 : Type u_2
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedAlgebra ℝ 𝕜
inst_6 : NormedSpace 𝕜 F
g₁ g₂ : E → 𝕜
hg₁ : Function.HasTemperateGrowth g₁
hg₂ : Function.HasTemperateGrowth g₂
f : 𝓢(E, F)
x : E
⊢ Eq.{u_6 + 1} (α := F)
    (((((smulLeftCLM F (g₁ - g₂) : 𝓢(E, F) →L[𝕜] 𝓢(E, F)) : (a : 𝓢(E, F)) → 𝓢(E, F)) f : 𝓢(E, F)) : (a : E) → F) x : F)
    ((((HSub.hSub (α := 𝓢(E, F) →L[𝕜] 𝓢(E, F)) (β := 𝓢(E, F) →L[𝕜] 𝓢(E, F)) (smulLeftCLM F g₁ : 𝓢(E, F) →L[𝕜] 𝓢(E, F))
                  (smulLeftCLM F g₂ : 𝓢(E, F) →L[𝕜] 𝓢(E, F)) :
                (a : 𝓢(E, F)) → 𝓢(E, F))
              f :
            𝓢(E, F)) :
          (a : E) → F)
        x :
      F)

Tactic:
simp [hg₁, hg₂, hg₁.sub hg₂, sub_smul]

Premises used: sub_smul, Function.HasTemperateGrowth.sub
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
𝕜 : Type u_2
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedAlgebra ℝ 𝕜
inst_6 : NormedSpace 𝕜 F
g : E → 𝕜
hg : Function.HasTemperateGrowth g
h :
  ∀ (f : 𝓢(E, F)) (x : E),
    Eq.{u_6 + 1} (α := F)
      (((((smulLeftCLM F (-g) : 𝓢(E, F) →L[𝕜] 𝓢(E, F)) : (a : 𝓢(E, F)) → 𝓢(E, F)) f : 𝓢(E, F)) : (a : E) → F) x : F)
      (((((-smulLeftCLM F g : 𝓢(E, F) →L[𝕜] 𝓢(E, F)) : (a : 𝓢(E, F)) → 𝓢(E, F)) f : 𝓢(E, F)) : (a : E) → F) x : F)
⊢ Eq (α := 𝓢(E, F) →L[𝕜] 𝓢(E, F)) (smulLeftCLM F (-g) : 𝓢(E, F) →L[𝕜] 𝓢(E, F))
    (-smulLeftCLM F g : 𝓢(E, F) →L[𝕜] 𝓢(E, F))

Tactic:
ext f x
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
𝕜 : Type u_2
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedAlgebra ℝ 𝕜
inst_6 : NormedSpace 𝕜 F
g : E → 𝕜
hg : Function.HasTemperateGrowth g
f : 𝓢(E, F)
x : E
⊢ Eq.{u_6 + 1} (α := F)
    (((((smulLeftCLM F (-g) : 𝓢(E, F) →L[𝕜] 𝓢(E, F)) : (a : 𝓢(E, F)) → 𝓢(E, F)) f : 𝓢(E, F)) : (a : E) → F) x : F)
    (((((-smulLeftCLM F g : 𝓢(E, F) →L[𝕜] 𝓢(E, F)) : (a : 𝓢(E, F)) → 𝓢(E, F)) f : 𝓢(E, F)) : (a : E) → F) x : F)

Tactic:
simp [hg, hg.neg, neg_smul]

Premises used: neg_smul, Function.HasTemperateGrowth.neg
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
𝕜 : Type u_2
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedAlgebra ℝ 𝕜
inst_6 : NormedSpace 𝕜 F
g : E → 𝕜
hg : Function.HasTemperateGrowth g
⊢ Eq (α := 𝓢(E, F) →L[𝕜] 𝓢(E, F)) (smulLeftCLM F fun (x : E) ↦ -g x : 𝓢(E, F) →L[𝕜] 𝓢(E, F))
    (-smulLeftCLM F g : 𝓢(E, F) →L[𝕜] 𝓢(E, F))

Tactic:
smulLeftCLM_neg hg

Premises used: SchwartzMap.smulLeftCLM_neg
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
ι : Type u_1
𝕜 : Type u_2
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedAlgebra ℝ 𝕜
inst_6 : NormedSpace 𝕜 F
g : ι → E → 𝕜
s : Finset ι
hg : ∀ i ∈ s, Function.HasTemperateGrowth (g i)
h :
  ∀ (f : 𝓢(E, F)) (x : E),
    Eq.{u_6 + 1} (α := F)
      (((((smulLeftCLM F fun (x : E) ↦ ∑ i ∈ s, g i x : 𝓢(E, F) →L[𝕜] 𝓢(E, F)) : (a : 𝓢(E, F)) → 𝓢(E, F)) f : 𝓢(E, F)) :
            (a : E) → F)
          x :
        F)
      ((((∑ i ∈ s, smulLeftCLM F (g i) : (a : 𝓢(E, F)) → 𝓢(E, F)) f : 𝓢(E, F)) : (a : E) → F) x : F)
⊢ Eq (α := 𝓢(E, F) →L[𝕜] 𝓢(E, F)) (smulLeftCLM F fun (x : E) ↦ ∑ i ∈ s, g i x : 𝓢(E, F) →L[𝕜] 𝓢(E, F))
    (∑ i ∈ s, smulLeftCLM F (g i) : 𝓢(E, F) →L[𝕜] 𝓢(E, F))

Tactic:
ext f x
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
ι : Type u_1
𝕜 : Type u_2
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedAlgebra ℝ 𝕜
inst_6 : NormedSpace 𝕜 F
g : ι → E → 𝕜
s : Finset ι
hg : ∀ i ∈ s, Function.HasTemperateGrowth (g i)
f : 𝓢(E, F)
x : E
⊢ Eq.{u_6 + 1} (α := F)
    (((((smulLeftCLM F fun (x : E) ↦ ∑ i ∈ s, g i x : 𝓢(E, F) →L[𝕜] 𝓢(E, F)) : (a : 𝓢(E, F)) → 𝓢(E, F)) f : 𝓢(E, F)) :
          (a : E) → F)
        x :
      F)
    ((((∑ i ∈ s, smulLeftCLM F (g i) : (a : 𝓢(E, F)) → 𝓢(E, F)) f : 𝓢(E, F)) : (a : E) → F) x : F)

Tactic:
simp +contextual [Function.HasTemperateGrowth.sum hg, Finset.sum_smul, hg]

Premises used: Finset.sum_smul, Function.HasTemperateGrowth.sum