awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
k n : ℕ
f g : 𝓢(E, F)
x : E
hbc :
  ‖HAdd.hAdd (α := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
        (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x) (iteratedFDeriv ℝ n (⇑g : (a : E) → F) x)‖ ≤
    norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
        (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x) +
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
        (iteratedFDeriv ℝ n (⇑g : (a : E) → F) x)
⊢ norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
      (iteratedFDeriv ℝ n (HAdd.hAdd (α := (a : E) → F) (⇑f : (a : E) → F) (⇑g : (a : E) → F)) x) ≤
    norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
        (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x) +
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
        (iteratedFDeriv ℝ n (⇑g : (a : E) → F) x)

Tactic:
rw [iteratedFDeriv_add_apply (f.smooth _).contDiffAt (g.smooth _).contDiffAt]

Premises used: iteratedFDeriv_add_apply, SchwartzMap.smooth, ContDiff.contDiffAt
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
k n : ℕ
f g : 𝓢(E, F)
x : E
⊢ ‖HAdd.hAdd (α := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
        (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x) (iteratedFDeriv ℝ n (⇑g : (a : E) → F) x)‖ ≤
    norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
        (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x) +
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
        (iteratedFDeriv ℝ n (⇑g : (a : E) → F) x)

Tactic:
norm_add_le _ _

Premises used: norm_add_le
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
k n : ℕ
f g : 𝓢(E, F)
x : E
⊢ ‖HAdd.hAdd (α := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
        (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x) (iteratedFDeriv ℝ n (⇑g : (a : E) → F) x)‖ ≤
    norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
        (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x) +
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
        (iteratedFDeriv ℝ n (⇑g : (a : E) → F) x)

Tactic:
exact norm_add_le _ _

Premises used: norm_add_le
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
k n : ℕ
f : 𝓢(E, F)
x : E
rw :
  ‖x‖ ^ k *
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
        (-iteratedFDeriv ℝ n (⇑f : (a : E) → F) x) =
    ‖x‖ ^ k *
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
        (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x)
rw₁ rw₂ :
  ‖x‖ ^ k *
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
        (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x) =
    ‖x‖ ^ k *
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
        (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x)
⊢ ‖x‖ ^ k *
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
        (iteratedFDeriv ℝ n (-(⇑f : (a : E) → F)) x) =
    ‖x‖ ^ k *
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
        (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x)

Tactic:
rw [iteratedFDeriv_neg_apply, norm_neg]

Premises used: iteratedFDeriv_neg_apply, norm_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 : NormedField 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
k n : ℕ
f : 𝓢(E, F)
c : 𝕜
x : E
rw :
  ‖x‖ ^ k *
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
        (iteratedFDeriv ℝ n (HSMul.hSMul (β := (a : E) → F) c (⇑f : (a : E) → F)) x) =
    ‖x‖ ^ k * ‖c‖ *
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
        (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x)
rw₁ :
  ‖x‖ ^ k *
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
        (iteratedFDeriv ℝ n (HSMul.hSMul (β := (a : E) → F) c (⇑f : (a : E) → F)) x) =
    ‖x‖ ^ k *
      (‖c‖ *
        norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
          (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x))
rw₂ :
  ‖x‖ ^ k *
      ‖HSMul.hSMul (β := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F) c
          (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x)‖ =
    ‖x‖ ^ k *
      (‖c‖ *
        norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
          (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x))
rw₃ rw₄ :
  ‖x‖ ^ k *
      (‖c‖ *
        norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
          (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x)) =
    ‖x‖ ^ k *
      (‖c‖ *
        norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
          (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x))
⊢ ‖x‖ ^ k *
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
        (iteratedFDeriv ℝ n (HSMul.hSMul (β := (a : E) → F) c (⇑f : (a : E) → F)) x) =
    ‖c‖ * ‖x‖ ^ k *
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
        (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x)

Tactic:
rw [mul_comm ‖c‖, mul_assoc, iteratedFDeriv_const_smul_apply (f.smooth _).contDiffAt,
    norm_smul c (iteratedFDeriv ℝ n (⇑f) x)]

Premises used: Norm.norm, Real, norm_smul, mul_assoc, iteratedFDeriv_const_smul_apply, mul_comm, iteratedFDeriv, DFunLike.coe, SchwartzMap.smooth, ContDiff.contDiffAt
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
k n : ℕ
f : 𝓢(E, F)
⊢ 0 ≤ seminormAux k n f

Tactic:
le_csInf (bounds_nonempty k n f) fun _ ⟨hx, _⟩ => hx

Premises used: _private.0.SchwartzMap.bounds_bddBelow.match_1, le_csInf, LE.le, _private.0.SchwartzMap.bounds_nonempty, OfNat.ofNat, _private.0.SchwartzMap.seminormAux
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
k n : ℕ
f : 𝓢(E, F)
x : E
⊢ ‖x‖ ^ k *
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
        (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x) ≤
    seminormAux k n f

Tactic:
le_csInf (bounds_nonempty k n f) fun _ ⟨_, h⟩ => h x

Premises used: Norm.norm, Real, HMul.hMul, _private.0.SchwartzMap.bounds_bddBelow.match_1, le_csInf, LE.le, _private.0.SchwartzMap.bounds_nonempty, HPow.hPow, iteratedFDeriv, DFunLike.coe, _private.0.SchwartzMap.seminormAux
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
k n : ℕ
f : 𝓢(E, F)
M : ℝ
hMp : 0 ≤ M
hM :
  ∀ (x : E),
    ‖x‖ ^ k *
        norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
          (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x) ≤
      M
⊢ seminormAux k n f ≤ M

Tactic:
csInf_le (bounds_bddBelow k n f) ⟨hMp, hM⟩

Premises used: And.intro, _private.0.SchwartzMap.bounds_bddBelow, csInf_le, _private.0.SchwartzMap.seminormAux
-- 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 : NormedField 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
inst_7 : NormedField 𝕜'
inst_8 : NormedSpace 𝕜' F
inst_9 : SMulCommClass ℝ 𝕜' F
c : 𝕜
f : 𝓢(E, F)
⊢ ContDiff ℝ ∞ (HSMul.hSMul (β := (a : E) → F) c (⇑f : (a : E) → F))

Tactic:
(f.smooth _).const_smul c

Premises used: SchwartzMap.smooth, ContDiff.const_smul
-- 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 : NormedField 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
inst_7 : NormedField 𝕜'
inst_8 : NormedSpace 𝕜' F
inst_9 : SMulCommClass ℝ 𝕜' F
c : 𝕜
f : 𝓢(E, F)
⊢ ContDiff ℝ ∞ (HSMul.hSMul (β := (a : E) → F) c (⇑f : (a : E) → F))

Tactic:
exact (f.smooth _).const_smul c

Premises used: SchwartzMap.smooth, ContDiff.const_smul
-- 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 : NormedField 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
inst_7 : NormedField 𝕜'
inst_8 : NormedSpace 𝕜' F
inst_9 : SMulCommClass ℝ 𝕜' F
c : 𝕜
f : 𝓢(E, F)
k n : ℕ
h :
  ∀ (x : E),
    ‖x‖ ^ k *
        norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
          (iteratedFDeriv ℝ n (HSMul.hSMul (β := (a : E) → F) c (⇑f : (a : E) → F)) x) ≤
      seminormAux k n f * ‖c‖
⊢ ∃ (C : ℝ),
    ∀ (x : E),
      ‖x‖ ^ k *
          norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
            (iteratedFDeriv ℝ n (HSMul.hSMul (β := (a : E) → F) c (⇑f : (a : E) → F)) x) ≤
        C

Tactic:
use f.seminormAux k n * ‖c‖

Premises used: _private.0.SchwartzMap.seminormAux
-- 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 : NormedField 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
inst_7 : NormedField 𝕜'
inst_8 : NormedSpace 𝕜' F
inst_9 : SMulCommClass ℝ 𝕜' F
c : 𝕜
f : 𝓢(E, F)
k n : ℕ
x : E
rw :
  ‖x‖ ^ k *
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
        (iteratedFDeriv ℝ n (HSMul.hSMul (β := (a : E) → F) c (⇑f : (a : E) → F)) x) =
    ‖c‖ * ‖x‖ ^ k *
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
        (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x)
⊢ ‖x‖ ^ k *
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
        (iteratedFDeriv ℝ n (HSMul.hSMul (β := (a : E) → F) c (⇑f : (a : E) → F)) x) =
    ‖x‖ ^ k *
        norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
          (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x) *
      ‖c‖

Tactic:
rw [mul_comm _ ‖c‖, ← mul_assoc]

Premises used: Norm.norm, mul_assoc, mul_comm
-- 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 : NormedField 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
inst_7 : NormedField 𝕜'
inst_8 : NormedSpace 𝕜' F
inst_9 : SMulCommClass ℝ 𝕜' F
c : 𝕜
f : 𝓢(E, F)
k n : ℕ
x : E
⊢ ‖x‖ ^ k *
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
        (iteratedFDeriv ℝ n (HSMul.hSMul (β := (a : E) → F) c (⇑f : (a : E) → F)) x) =
    ‖c‖ * ‖x‖ ^ k *
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
        (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x)

Tactic:
decay_smul_aux k n f c x

Premises used: _private.0.SchwartzMap.decay_smul_aux
-- 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 : NormedField 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
inst_7 : NormedField 𝕜'
inst_8 : NormedSpace 𝕜' F
inst_9 : SMulCommClass ℝ 𝕜' F
c : 𝕜
f : 𝓢(E, F)
k n : ℕ
x : E
⊢ ‖x‖ ^ k *
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
        (iteratedFDeriv ℝ n (HSMul.hSMul (β := (a : E) → F) c (⇑f : (a : E) → F)) x) =
    ‖c‖ * ‖x‖ ^ k *
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
        (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x)

Tactic:
exact decay_smul_aux k n f c x

Premises used: _private.0.SchwartzMap.decay_smul_aux
-- 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 : NormedField 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
inst_7 : NormedField 𝕜'
inst_8 : NormedSpace 𝕜' F
inst_9 : SMulCommClass ℝ 𝕜' F
c : 𝕜
f : 𝓢(E, F)
k n : ℕ
x : E
hbc :
  ‖x‖ ^ k *
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
        (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x) ≤
    seminormAux k n f
⊢ ‖x‖ ^ k *
        norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
          (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x) *
      ‖c‖ ≤
    seminormAux k n f * ‖c‖

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 : NormedField 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
inst_7 : NormedField 𝕜'
inst_8 : NormedSpace 𝕜' F
inst_9 : SMulCommClass ℝ 𝕜' F
c : 𝕜
f : 𝓢(E, F)
k n : ℕ
x : E
⊢ ‖x‖ ^ k *
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
        (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x) ≤
    seminormAux k n f

Tactic:
apply f.le_seminormAux

Premises used: _private.0.SchwartzMap.le_seminormAux
-- 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 : NormedField 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
inst_7 : NormedField 𝕜'
inst_8 : NormedSpace 𝕜' F
inst_9 : SMulCommClass ℝ 𝕜' F
c : 𝕜
f : 𝓢(E, F)
k n : ℕ
x : E
k₁ :
  ‖x‖ ^ k *
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
        (iteratedFDeriv ℝ n (HSMul.hSMul (β := (a : E) → F) c (⇑f : (a : E) → F)) x) =
    ‖x‖ ^ k *
        norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
          (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x) *
      ‖c‖
k₂ :
  ‖x‖ ^ k *
        norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
          (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x) *
      ‖c‖ ≤
    seminormAux k n f * ‖c‖
⊢ ‖x‖ ^ k *
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
        (iteratedFDeriv ℝ n (HSMul.hSMul (β := (a : E) → F) c (⇑f : (a : E) → F)) x) ≤
    seminormAux k n f * ‖c‖

Tactic:
calc
          ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (c • ⇑f) x‖ = ‖x‖ ^ k * ‖iteratedFDeriv ℝ n f x‖ * ‖c‖ := by
            rw [mul_comm _ ‖c‖, ← mul_assoc]
            exact decay_smul_aux k n f c x
          _ ≤ SchwartzMap.seminormAux k n f * ‖c‖ := by
            gcongr
            apply f.le_seminormAux

Premises used: Real, HSMul.hSMul, iteratedFDeriv, DFunLike.coe, _private.0.SchwartzMap.seminormAux
-- 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 : NormedField 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
f : 𝓢(E, F)
c : 𝕜
x : E
⊢ (c • f : (a : E) → F) x = HSMul.hSMul (β := F) c ((f : (a : E) → F) x : F)

Tactic:
rfl

Premises used: rfl
-- 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 : NormedField 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
inst_7 : NormedField 𝕜'
inst_8 : NormedSpace 𝕜' F
inst_9 : SMulCommClass ℝ 𝕜' F
inst_10 : SMul 𝕜 𝕜'
inst_11 : IsScalarTower 𝕜 𝕜' F
⊢ IsScalarTower 𝕜 𝕜' 𝓢(E, F)

Tactic:
⟨fun a b f => ext fun x => smul_assoc a b (f x)⟩

Premises used: smul_assoc, IsScalarTower.mk, DFunLike.coe, SchwartzMap.ext
-- 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 : NormedField 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
inst_7 : NormedField 𝕜'
inst_8 : NormedSpace 𝕜' F
inst_9 : SMulCommClass ℝ 𝕜' F
inst_10 : SMulCommClass 𝕜 𝕜' F
⊢ SMulCommClass 𝕜 𝕜' 𝓢(E, F)

Tactic:
⟨fun a b f => ext fun x => smul_comm a b (f x)⟩

Premises used: SMulCommClass.smul_comm, SMulCommClass.mk, DFunLike.coe, SchwartzMap.ext
-- 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 : NormedField 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
k n : ℕ
c : 𝕜
f : 𝓢(E, F)
⊢ seminormAux k n (c • f) ≤ ‖c‖ * seminormAux k n f

Tactic:
(c • f).seminormAux_le_bound k n (mul_nonneg (norm_nonneg _) (seminormAux_nonneg _ _ _))
      fun x => (decay_smul_aux k n f c x).trans_le ?_

Premises used: mul_nonneg, _private.0.SchwartzMap.decay_smul_aux, _private.0.SchwartzMap.seminormAux_le_bound, _private.0.SchwartzMap.seminormAux_nonneg, Eq.trans_le, HSMul.hSMul, norm_nonneg
-- 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 : NormedField 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
k n : ℕ
c : 𝕜
f : 𝓢(E, F)
refine :
  ∀ (x : E),
    ‖c‖ * ‖x‖ ^ k *
        norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
          (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x) ≤
      ‖c‖ * seminormAux k n f
⊢ seminormAux k n (c • f) ≤ ‖c‖ * seminormAux k n f

Tactic:
refine (c • f).seminormAux_le_bound k n (mul_nonneg (norm_nonneg _) (seminormAux_nonneg _ _ _))
      fun x => (decay_smul_aux k n f c x).trans_le ?_

Premises used: mul_nonneg, _private.0.SchwartzMap.decay_smul_aux, _private.0.SchwartzMap.seminormAux_le_bound, _private.0.SchwartzMap.seminormAux_nonneg, Eq.trans_le, HSMul.hSMul, norm_nonneg
-- 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 : NormedField 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
k n : ℕ
c : 𝕜
f : 𝓢(E, F)
x : E
rw :
  ‖c‖ *
      (‖x‖ ^ k *
        norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
          (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x)) ≤
    ‖c‖ * seminormAux k n f
⊢ ‖c‖ * ‖x‖ ^ k *
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
        (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x) ≤
    ‖c‖ * seminormAux k n f

Tactic:
rw [mul_assoc]

Premises used: mul_assoc
-- 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 : NormedField 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
k n : ℕ
c : 𝕜
f : 𝓢(E, F)
x : E
hbc :
  ‖x‖ ^ k *
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
        (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x) ≤
    seminormAux k n f
⊢ ‖c‖ *
      (‖x‖ ^ k *
        norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
          (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x)) ≤
    ‖c‖ * seminormAux k n f

Tactic:
gcongr
-- 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 : NormedField 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
k n : ℕ
c : 𝕜
f : 𝓢(E, F)
x : E
⊢ ‖x‖ ^ k *
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
        (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x) ≤
    seminormAux k n f

Tactic:
f.le_seminormAux k n x

Premises used: _private.0.SchwartzMap.le_seminormAux
-- 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 : NormedField 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
k n : ℕ
c : 𝕜
f : 𝓢(E, F)
x : E
⊢ ‖x‖ ^ k *
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
        (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x) ≤
    seminormAux k n f

Tactic:
exact f.le_seminormAux k n x

Premises used: _private.0.SchwartzMap.le_seminormAux
-- 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 : NormedField 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
inst_7 : NormedField 𝕜'
inst_8 : NormedSpace 𝕜' F
inst_9 : SMulCommClass ℝ 𝕜' F
c : ℕ
f : 𝓢(E, F)
⊢ ContDiff ℝ ∞ (HSMul.hSMul (β := (a : E) → F) c (⇑f : (a : E) → F))

Tactic:
(f.smooth _).const_smul c

Premises used: SchwartzMap.smooth, ContDiff.const_smul
-- 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 : NormedField 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
inst_7 : NormedField 𝕜'
inst_8 : NormedSpace 𝕜' F
inst_9 : SMulCommClass ℝ 𝕜' F
c : ℕ
f : 𝓢(E, F)
⊢ ContDiff ℝ ∞ (HSMul.hSMul (β := (a : E) → F) c (⇑f : (a : E) → F))

Tactic:
exact (f.smooth _).const_smul c

Premises used: SchwartzMap.smooth, ContDiff.const_smul