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 : 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 : ℕ),
    ∃ (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:
simpa [← Nat.cast_smul_eq_nsmul ℝ] using ((c : ℝ) • f).decay'

Premises used: Real, SchwartzMap.decay', Nat.cast, Nat.cast_smul_eq_nsmul, HSMul.hSMul
-- 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 : ℕ),
    ∃ (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:
simpa [← Int.cast_smul_eq_zsmul ℝ] using ((c : ℝ) • f).decay'

Premises used: Int.cast, Real, SchwartzMap.decay', HSMul.hSMul, Int.cast_smul_eq_zsmul
-- 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
⊢ ContDiff.{0, u_5, u_6} ℝ (F := F) ∞ fun (x : E) ↦ 0

Tactic:
contDiff_const

Premises used: contDiff_const
-- 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
⊢ ContDiff.{0, u_5, u_6} ℝ (F := F) ∞ fun (x : E) ↦ 0

Tactic:
exact contDiff_const

Premises used: contDiff_const
-- 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
x x_1 : ℕ
x_2 : E
⊢ ‖x_2‖ ^ x *
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin x_1) ↦ E) F)
        (iteratedFDeriv ℝ x_1 (fun (x : E) ↦ 0) x_2) ≤
    1

Tactic:
simp
-- 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
⊢ Eq (α := (a : E) → F) (⇑0 : (a : E) → F) 0

Tactic:
rfl

Premises used: rfl
-- 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
x : E
⊢ Eq.{u_6 + 1} (α := F) ((0 : (a : E) → F) x : F) (0 : F)

Tactic:
rfl

Premises used: rfl
-- 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 : ℕ
x : E
⊢ ‖x‖ ^ k *
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
        (iteratedFDeriv ℝ n (⇑0 : (a : E) → F) x) ≤
    0

Tactic:
simp [Pi.zero_def]

Premises used: Pi.zero_def
-- 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
f : 𝓢(E, F)
⊢ ContDiff.{0, u_5, u_6} ℝ (E := E) (F := F) ∞ (-(⇑f : (a : E) → F))

Tactic:
(f.smooth _).neg

Premises used: ContDiff.neg, SchwartzMap.smooth
-- 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
f : 𝓢(E, F)
⊢ ContDiff.{0, u_5, u_6} ℝ (E := E) (F := F) ∞ (-(⇑f : (a : E) → F))

Tactic:
exact (f.smooth _).neg

Premises used: ContDiff.neg, SchwartzMap.smooth
-- 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
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 (-(⇑f : (a : E) → F)) x) ≤
      seminormAux k n f
⊢ ∃ (C : ℝ),
    ∀ (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) ≤
        C

Tactic:
use f.seminormAux k n

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
f : 𝓢(E, F)
k n : ℕ
x : E
h :
  ‖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
h₁ h₂ : seminormAux k n f ≤ 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) ≤
    seminormAux k n f

Tactic:
grw [f.decay_neg_aux k n x, f.le_seminormAux k n x]

Premises used: _private.0.SchwartzMap.decay_neg_aux, _private.0.SchwartzMap.le_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
f : 𝓢(E, F)
x : E
⊢ Eq.{u_6 + 1} (α := F) ((-f : (a : E) → F) x : F) (-(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
f g : 𝓢(E, F)
⊢ ContDiff ℝ ∞ (HAdd.hAdd (α := (a : E) → F) (⇑f : (a : E) → F) (⇑g : (a : E) → F))

Tactic:
(f.smooth _).add (g.smooth _)

Premises used: ContDiff.add, SchwartzMap.smooth
-- 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
f g : 𝓢(E, F)
⊢ ContDiff ℝ ∞ (HAdd.hAdd (α := (a : E) → F) (⇑f : (a : E) → F) (⇑g : (a : E) → F))

Tactic:
exact (f.smooth _).add (g.smooth _)

Premises used: ContDiff.add, SchwartzMap.smooth
-- 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
f g : 𝓢(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 (HAdd.hAdd (α := (a : E) → F) (⇑f : (a : E) → F) (⇑g : (a : E) → F)) x) ≤
      seminormAux k n f + seminormAux k n g
⊢ ∃ (C : ℝ),
    ∀ (x : E),
      ‖x‖ ^ k *
          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) ≤
        C

Tactic:
use f.seminormAux k n + g.seminormAux k n

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
f g : 𝓢(E, F)
k n : ℕ
x : E
h :
  ‖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 (⇑g : (a : E) → F) x) ≤
    seminormAux k n f + seminormAux k n g
h₁ :
  seminormAux k n f +
      ‖x‖ ^ k *
        norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
          (iteratedFDeriv ℝ n (⇑g : (a : E) → F) x) ≤
    seminormAux k n f + seminormAux k n g
h₂ h₃ : seminormAux k n f + seminormAux k n g ≤ seminormAux k n f + seminormAux k n g
⊢ ‖x‖ ^ k *
      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) ≤
    seminormAux k n f + seminormAux k n g

Tactic:
grw [decay_add_le_aux k n f g x, f.le_seminormAux k n x, g.le_seminormAux k n x]

Premises used: _private.0.SchwartzMap.decay_add_le_aux, _private.0.SchwartzMap.le_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
f g : 𝓢(E, F)
x : E
⊢ (f + g : (a : E) → F) x = HAdd.hAdd (α := F) (β := F) ((f : (a : E) → F) x : F) ((g : (a : E) → F) x : F)

Tactic:
rfl

Premises used: rfl
-- 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)
⊢ seminormAux k n (f + g) ≤ seminormAux k n f + seminormAux k n g

Tactic:
(f + g).seminormAux_le_bound k n
    (add_nonneg (seminormAux_nonneg _ _ _) (seminormAux_nonneg _ _ _)) fun x =>
    (decay_add_le_aux k n f g x).trans <|
      add_le_add (f.le_seminormAux k n x) (g.le_seminormAux k n x)

Premises used: _private.0.SchwartzMap.seminormAux_le_bound, add_le_add, _private.0.SchwartzMap.seminormAux_nonneg, add_nonneg, _private.0.SchwartzMap.decay_add_le_aux, HAdd.hAdd, _private.0.SchwartzMap.le_seminormAux, LE.le.trans
-- 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
f g : 𝓢(E, F)
⊢ ContDiff ℝ ∞ (HSub.hSub (α := (a : E) → F) (⇑f : (a : E) → F) (⇑g : (a : E) → F))

Tactic:
(f.smooth _).sub (g.smooth _)

Premises used: ContDiff.sub, SchwartzMap.smooth
-- 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
f g : 𝓢(E, F)
⊢ ContDiff ℝ ∞ (HSub.hSub (α := (a : E) → F) (⇑f : (a : E) → F) (⇑g : (a : E) → F))

Tactic:
exact (f.smooth _).sub (g.smooth _)

Premises used: ContDiff.sub, SchwartzMap.smooth
-- 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
f g : 𝓢(E, F)
k n : ℕ
⊢ ∃ (C : ℝ),
    ∀ (x : E),
      ‖x‖ ^ k *
          norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
            (iteratedFDeriv ℝ n (HSub.hSub (α := (a : E) → F) (⇑f : (a : E) → F) (⇑g : (a : E) → F)) x) ≤
        C

Tactic:
⟨f.seminormAux k n + g.seminormAux k n, fun x => ?_⟩

Premises used: HAdd.hAdd, Exists.intro, _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
f g : 𝓢(E, F)
k n : ℕ
refine :
  ∀ (x : E),
    ‖x‖ ^ k *
        norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
          (iteratedFDeriv ℝ n (HSub.hSub (α := (a : E) → F) (⇑f : (a : E) → F) (⇑g : (a : E) → F)) x) ≤
      seminormAux k n f + seminormAux k n g
⊢ ∃ (C : ℝ),
    ∀ (x : E),
      ‖x‖ ^ k *
          norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
            (iteratedFDeriv ℝ n (HSub.hSub (α := (a : E) → F) (⇑f : (a : E) → F) (⇑g : (a : E) → F)) x) ≤
        C

Tactic:
refine ⟨f.seminormAux k n + g.seminormAux k n, fun x => ?_⟩
-- 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
f g : 𝓢(E, F)
k n : ℕ
x : E
grw :
  ‖x‖ ^ k *
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
        (iteratedFDeriv ℝ n (HSub.hSub (α := (a : E) → F) (⇑f : (a : E) → F) (⇑g : (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 (⇑g : (a : E) → F) x)
⊢ ‖x‖ ^ k *
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
        (iteratedFDeriv ℝ n (HSub.hSub (α := (a : E) → F) (⇑f : (a : E) → F) (⇑g : (a : E) → F)) x) ≤
    seminormAux k n f + seminormAux k n g

Tactic:
grw [← f.le_seminormAux k n x, ← g.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
f g : 𝓢(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 (HAdd.hAdd (α := (a : E) → F) (⇑f : (a : E) → F) (-(⇑g : (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 (⇑g : (a : E) → F) x)
⊢ ‖x‖ ^ k *
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
        (iteratedFDeriv ℝ n (HSub.hSub (α := (a : E) → F) (⇑f : (a : E) → F) (⇑g : (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 (⇑g : (a : E) → F) x)

Tactic:
rw [sub_eq_add_neg]

Premises used: sub_eq_add_neg
-- 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
f g : 𝓢(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 (HAdd.hAdd (α := (a : E) → F) (⇑f : (a : E) → F) (-(⇑g : (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 (-(⇑g : (a : E) → F)) x)
⊢ ‖x‖ ^ k *
      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) ≤
    ‖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 (⇑g : (a : E) → F) x)

Tactic:
rw [← decay_neg_aux k n g x]

Premises used: _private.0.SchwartzMap.decay_neg_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
f g : 𝓢(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 (HAdd.hAdd (α := (a : E) → F) (⇑f : (a : E) → F) (-(⇑g : (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 (-(⇑g : (a : E) → F)) x)

Tactic:
decay_add_le_aux k n f (-g) x

Premises used: _private.0.SchwartzMap.decay_add_le_aux, Neg.neg
-- 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
f g : 𝓢(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 (HAdd.hAdd (α := (a : E) → F) (⇑f : (a : E) → F) (-(⇑g : (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 (-(⇑g : (a : E) → F)) x)

Tactic:
exact decay_add_le_aux k n f (-g) x

Premises used: _private.0.SchwartzMap.decay_add_le_aux, Neg.neg
-- 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
f g : 𝓢(E, F)
x : E
⊢ (f - g : (a : E) → F) x = HSub.hSub (α := F) (β := F) ((f : (a : E) → F) x : F) ((g : (a : E) → F) x : F)

Tactic:
rfl

Premises used: rfl
-- 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
ι : Type u_10
f : ι → 𝓢(E, F)
x : E
⊢ Eq.{u_6 + 1} (α := F) ((∑ i ∈ ∅, f i : (a : E) → F) x : F) (∑ i ∈ ∅, (f i : (a : E) → F) x : F)

Tactic:
simp
-- 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
ι : Type u_10
f : ι → 𝓢(E, F)
x : E
i : ι
s : Finset ι
his : i ∉ s
h : Eq.{u_6 + 1} (α := F) ((∑ i ∈ s, f i : (a : E) → F) x : F) (∑ i ∈ s, (f i : (a : E) → F) x : F)
⊢ Eq.{u_6 + 1} (α := F) ((∑ i ∈ insert i s, f i : (a : E) → F) x : F) (∑ i ∈ insert i s, (f i : (a : E) → F) x : F)

Tactic:
simp [his, h]
-- 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
ι : Type u_10
s : Finset ι
f : ι → 𝓢(E, F)
x : E
empty : Eq.{u_6 + 1} (α := F) ((∑ i ∈ ∅, f i : (a : E) → F) x : F) (∑ i ∈ ∅, (f i : (a : E) → F) x : F)
insert :
  ∀ (i : ι) (s : Finset ι) (his : i ∉ s)
    (h : Eq.{u_6 + 1} (α := F) ((∑ i ∈ s, f i : (a : E) → F) x : F) (∑ i ∈ s, (f i : (a : E) → F) x : F)),
    Eq.{u_6 + 1} (α := F) ((∑ i ∈ Insert.insert i s, f i : (a : E) → F) x : F)
      (∑ i ∈ Insert.insert i s, (f i : (a : E) → F) x : F)
⊢ Eq.{u_6 + 1} (α := F) ((∑ i ∈ s, f i : (a : E) → F) x : F) (∑ i ∈ s, (f i : (a : E) → F) x : F)

Tactic:
induction s using Finset.induction_on with
  | empty => simp
  | insert i s his h => simp [his, h]

Premises used: Insert.insert
-- 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
⊢ Eq (α := (a : 𝓢(E, F)) → E → F) (⇑(coeHom E F) : (a : 𝓢(E, F)) → E → F) (DFunLike.coe (β := fun (a : E) ↦ F))

Tactic:
rfl

Premises used: rfl
-- 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
rw : Function.Injective (α := 𝓢(E, F)) (β := E → F) (DFunLike.coe (β := fun (a : E) ↦ F))
⊢ Function.Injective (α := 𝓢(E, F)) (β := E → F) (⇑(coeHom E F) : (a : 𝓢(E, F)) → E → F)

Tactic:
rw [coe_coeHom]

Premises used: SchwartzMap.coe_coeHom
-- 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
⊢ Function.Injective (α := 𝓢(E, F)) (β := E → F) (DFunLike.coe (β := fun (a : E) ↦ F))

Tactic:
DFunLike.coe_injective

Premises used: DFunLike.coe_injective