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 : NormedField 𝕜'
inst_6 : NormedAddCommGroup D
inst_7 : NormedSpace ℝ D
inst_8 : NormedSpace 𝕜 E
inst_9 : SMulCommClass ℝ 𝕜 E
inst_10 : NormedAddCommGroup G
inst_11 : NormedSpace ℝ G
inst_12 : NormedSpace 𝕜' G
inst_13 : SMulCommClass ℝ 𝕜' G
σ : 𝕜 →+* 𝕜'
inst_14 : RingHomIsometric σ
A : 𝓢(D, E) → G
hadd : ∀ (f g : 𝓢(D, E)), A (f + g) = A f + A g
hsmul : ∀ (a : 𝕜) (f : 𝓢(D, E)), A (a • f) = HSMul.hSMul.{u_3, u_7, u_7} (α := 𝕜') ((σ : (a : 𝕜) → 𝕜') a : 𝕜') (A f)
f : 𝓢(D, E) →ₛₗ[σ] G := { toFun := fun (x : 𝓢(D, E)) ↦ A x, map_add' := hadd, map_smul' := hsmul }
s : Finset (ℕ × ℕ)
C : ℝ
hC : 0 ≤ C
h : ∀ (f : 𝓢(D, E)), ‖A f‖ ≤ HMul.hMul (β := ℝ) C ((s.sup (schwartzSeminormFamily 𝕜 D E) : (a : 𝓢(D, E)) → ℝ) f : ℝ)
⊢ ∃ (s : Finset (ℕ × ℕ)) (C : ℝ≥0),
    Seminorm.comp (σ₁₂ := σ) (normSeminorm 𝕜' G)
        { toFun := fun (x : 𝓢(D, E)) ↦ A x, map_add' := hadd, map_smul' := hsmul } ≤
      HSMul.hSMul (β := Seminorm 𝕜 𝓢(D, E)) C (s.sup (schwartzSeminormFamily 𝕜 D E))

Tactic:
exact ⟨s, ⟨C, hC⟩, h⟩
-- 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 : NormedAddCommGroup G
inst_6 : NormedSpace ℝ G
inst_7 : NormedSpace 𝕜 G
inst_8 : SMulCommClass ℝ 𝕜 G
m : F
k n : ℕ
right :
  ∀ (f : 𝓢(E, F →L[ℝ] G)) (x : E),
    ‖x‖ ^ (k, n).1 *
        norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_7} ℝ (fun (i : Fin (k, n).2) ↦ E) G)
          (iteratedFDeriv ℝ (k, n).2
            ((fun (f : 𝓢(E, F →L[ℝ] G)) (x : E) ↦ ((((f : (a : E) → F →L[ℝ] G) x : F →L[ℝ] G) : (a : F) → G) m : G)) f)
            x) ≤
      HMul.hMul (β := ℝ) ‖m‖
        ((Finset.sup {(k, n)} (schwartzSeminormFamily 𝕜 E (F →L[ℝ] G)) : (a : 𝓢(E, F →L[ℝ] G)) → ℝ) f : ℝ)
⊢ ∃ (s : Finset (ℕ × ℕ)) (C : ℝ),
    0 ≤ C ∧
      ∀ (f : 𝓢(E, F →L[ℝ] G)) (x : E),
        ‖x‖ ^ (k, n).1 *
            norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_7} ℝ (fun (i : Fin (k, n).2) ↦ E) G)
              (iteratedFDeriv ℝ (k, n).2
                ((fun (f : 𝓢(E, F →L[ℝ] G)) (x : E) ↦ ((((f : (a : E) → F →L[ℝ] G) x : F →L[ℝ] G) : (a : F) → G) m : G))
                  f)
                x) ≤
          HMul.hMul (β := ℝ) C ((s.sup (schwartzSeminormFamily 𝕜 E (F →L[ℝ] G)) : (a : 𝓢(E, F →L[ℝ] G)) → ℝ) f : ℝ)

Tactic:
use {(k, n)}, ‖m‖, norm_nonneg _

Premises used: Prod.mk, norm_nonneg
-- 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 : NormedAddCommGroup G
inst_6 : NormedSpace ℝ G
inst_7 : NormedSpace 𝕜 G
inst_8 : SMulCommClass ℝ 𝕜 G
m : F
k n : ℕ
f : 𝓢(E, F →L[ℝ] G)
x : E
right :
  ‖x‖ ^ k *
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_7} ℝ (fun (i : Fin n) ↦ E) G)
        (iteratedFDeriv ℝ n (fun (x : E) ↦ (((f : (a : E) → F →L[ℝ] G) x : F →L[ℝ] G) : (a : F) → G) m) x) ≤
    HMul.hMul (β := ℝ) ‖m‖ ((SchwartzMap.seminorm 𝕜 k n : (a : 𝓢(E, F →L[ℝ] G)) → ℝ) f : ℝ)
⊢ ‖x‖ ^ (k, n).1 *
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_7} ℝ (fun (i : Fin (k, n).2) ↦ E) G)
        (iteratedFDeriv ℝ (k, n).2
          ((fun (f : 𝓢(E, F →L[ℝ] G)) (x : E) ↦ ((((f : (a : E) → F →L[ℝ] G) x : F →L[ℝ] G) : (a : F) → G) m : G)) f)
          x) ≤
    HMul.hMul (β := ℝ) ‖m‖
      ((Finset.sup {(k, n)} (schwartzSeminormFamily 𝕜 E (F →L[ℝ] G)) : (a : 𝓢(E, F →L[ℝ] G)) → ℝ) f : ℝ)

Tactic:
simp only [Finset.sup_singleton, schwartzSeminormFamily_apply]

Premises used: Finset.sup_singleton, SchwartzMap.schwartzSeminormFamily_apply
-- 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 : NormedAddCommGroup G
inst_6 : NormedSpace ℝ G
inst_7 : NormedSpace 𝕜 G
inst_8 : SMulCommClass ℝ 𝕜 G
m : F
k n : ℕ
f : 𝓢(E, F →L[ℝ] G)
x : E
hbc :
  norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_7} ℝ (fun (i : Fin n) ↦ E) G)
      (iteratedFDeriv ℝ n (fun (x : E) ↦ (((f : (a : E) → F →L[ℝ] G) x : F →L[ℝ] G) : (a : F) → G) m) x) ≤
    ‖m‖ *
      norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ E) (F →L[ℝ] G))
        (iteratedFDeriv ℝ n (⇑f : (a : E) → F →L[ℝ] G) x)
⊢ ‖x‖ ^ k *
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_7} ℝ (fun (i : Fin n) ↦ E) G)
        (iteratedFDeriv ℝ n (fun (x : E) ↦ (((f : (a : E) → F →L[ℝ] G) x : F →L[ℝ] G) : (a : F) → G) m) x) ≤
    ‖x‖ ^ k *
      (‖m‖ *
        norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ E) (F →L[ℝ] G))
          (iteratedFDeriv ℝ n (⇑f : (a : E) → F →L[ℝ] G) x))

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 : NormedAddCommGroup G
inst_6 : NormedSpace ℝ G
inst_7 : NormedSpace 𝕜 G
inst_8 : SMulCommClass ℝ 𝕜 G
m : F
k n : ℕ
f : 𝓢(E, F →L[ℝ] G)
x : E
⊢ norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_7} ℝ (fun (i : Fin n) ↦ E) G)
      (iteratedFDeriv ℝ n (fun (x : E) ↦ (((f : (a : E) → F →L[ℝ] G) x : F →L[ℝ] G) : (a : F) → G) m) x) ≤
    ‖m‖ *
      norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ E) (F →L[ℝ] G))
        (iteratedFDeriv ℝ n (⇑f : (a : E) → F →L[ℝ] G) x)

Tactic:
norm_iteratedFDeriv_clm_apply_const (f.smooth _).contDiffAt le_rfl

Premises used: le_rfl, SchwartzMap.smooth, ContDiff.contDiffAt, norm_iteratedFDeriv_clm_apply_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
inst_4 : NormedField 𝕜
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace ℝ G
inst_7 : NormedSpace 𝕜 G
inst_8 : SMulCommClass ℝ 𝕜 G
m : F
k n : ℕ
f : 𝓢(E, F →L[ℝ] G)
x : E
⊢ norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_7} ℝ (fun (i : Fin n) ↦ E) G)
      (iteratedFDeriv ℝ n (fun (x : E) ↦ (((f : (a : E) → F →L[ℝ] G) x : F →L[ℝ] G) : (a : F) → G) m) x) ≤
    ‖m‖ *
      norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ E) (F →L[ℝ] G))
        (iteratedFDeriv ℝ n (⇑f : (a : E) → F →L[ℝ] G) x)

Tactic:
exact norm_iteratedFDeriv_clm_apply_const (f.smooth _).contDiffAt le_rfl

Premises used: le_rfl, SchwartzMap.smooth, ContDiff.contDiffAt, norm_iteratedFDeriv_clm_apply_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
inst_4 : NormedField 𝕜
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace ℝ G
inst_7 : NormedSpace 𝕜 G
inst_8 : SMulCommClass ℝ 𝕜 G
m : F
k n : ℕ
f : 𝓢(E, F →L[ℝ] G)
x : E
move_mul :
  ‖x‖ ^ k *
        norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ E) (F →L[ℝ] G))
          (iteratedFDeriv ℝ n (⇑f : (a : E) → F →L[ℝ] G) x) *
      ‖m‖ ≤
    HMul.hMul (α := ℝ) ((SchwartzMap.seminorm 𝕜 k n : (a : 𝓢(E, F →L[ℝ] G)) → ℝ) f : ℝ) ‖m‖
⊢ ‖x‖ ^ k *
      (‖m‖ *
        norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ E) (F →L[ℝ] G))
          (iteratedFDeriv ℝ n (⇑f : (a : E) → F →L[ℝ] G) x)) ≤
    HMul.hMul (β := ℝ) ‖m‖ ((SchwartzMap.seminorm 𝕜 k n : (a : 𝓢(E, F →L[ℝ] G)) → ℝ) f : ℝ)

Tactic:
move_mul [‖m‖]
-- 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 : NormedAddCommGroup G
inst_6 : NormedSpace ℝ G
inst_7 : NormedSpace 𝕜 G
inst_8 : SMulCommClass ℝ 𝕜 G
m : F
k n : ℕ
f : 𝓢(E, F →L[ℝ] G)
x : E
hbc :
  ‖x‖ ^ k *
      norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ E) (F →L[ℝ] G))
        (iteratedFDeriv ℝ n (⇑f : (a : E) → F →L[ℝ] G) x) ≤
    (SchwartzMap.seminorm 𝕜 k n : (a : 𝓢(E, F →L[ℝ] G)) → ℝ) f
⊢ ‖x‖ ^ k *
        norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ E) (F →L[ℝ] G))
          (iteratedFDeriv ℝ n (⇑f : (a : E) → F →L[ℝ] G) x) *
      ‖m‖ ≤
    HMul.hMul (α := ℝ) ((SchwartzMap.seminorm 𝕜 k n : (a : 𝓢(E, F →L[ℝ] G)) → ℝ) f : ℝ) ‖m‖

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 : NormedAddCommGroup G
inst_6 : NormedSpace ℝ G
inst_7 : NormedSpace 𝕜 G
inst_8 : SMulCommClass ℝ 𝕜 G
m : F
k n : ℕ
f : 𝓢(E, F →L[ℝ] G)
x : E
⊢ ‖x‖ ^ k *
      norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ E) (F →L[ℝ] G))
        (iteratedFDeriv ℝ n (⇑f : (a : E) → F →L[ℝ] G) x) ≤
    (SchwartzMap.seminorm 𝕜 k n : (a : 𝓢(E, F →L[ℝ] G)) → ℝ) f

Tactic:
apply le_seminorm

Premises used: SchwartzMap.le_seminorm
-- 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 : NormedAddCommGroup G
inst_6 : NormedSpace ℝ G
inst_7 : NormedSpace 𝕜 G
inst_8 : SMulCommClass ℝ 𝕜 G
m : F
k n : ℕ
f : 𝓢(E, F →L[ℝ] G)
x : E
k₁ :
  ‖x‖ ^ k *
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_7} ℝ (fun (i : Fin n) ↦ E) G)
        (iteratedFDeriv ℝ n (fun (x : E) ↦ (((f : (a : E) → F →L[ℝ] G) x : F →L[ℝ] G) : (a : F) → G) m) x) ≤
    ‖x‖ ^ k *
      (‖m‖ *
        norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ E) (F →L[ℝ] G))
          (iteratedFDeriv ℝ n (⇑f : (a : E) → F →L[ℝ] G) x))
k₂ :
  ‖x‖ ^ k *
      (‖m‖ *
        norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ E) (F →L[ℝ] G))
          (iteratedFDeriv ℝ n (⇑f : (a : E) → F →L[ℝ] G) x)) ≤
    HMul.hMul (β := ℝ) ‖m‖ ((SchwartzMap.seminorm 𝕜 k n : (a : 𝓢(E, F →L[ℝ] G)) → ℝ) f : ℝ)
⊢ ‖x‖ ^ k *
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_7} ℝ (fun (i : Fin n) ↦ E) G)
        (iteratedFDeriv ℝ n (fun (x : E) ↦ (((f : (a : E) → F →L[ℝ] G) x : F →L[ℝ] G) : (a : F) → G) m) x) ≤
    HMul.hMul (β := ℝ) ‖m‖ ((SchwartzMap.seminorm 𝕜 k n : (a : 𝓢(E, F →L[ℝ] G)) → ℝ) f : ℝ)

Tactic:
calc
    ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (f · m) x‖ ≤ ‖x‖ ^ k * (‖m‖ * ‖iteratedFDeriv ℝ n f x‖) := by
      gcongr
      exact norm_iteratedFDeriv_clm_apply_const (f.smooth _).contDiffAt le_rfl
    _ ≤ ‖m‖ * SchwartzMap.seminorm 𝕜 k n f := by
      move_mul [‖m‖]
      gcongr
      apply le_seminorm

Premises used: Norm.norm, Real, HMul.hMul, SchwartzMap.seminorm, iteratedFDeriv, DFunLike.coe
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
𝕜 : Type u_2
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 : NormedField 𝕜
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace ℝ G
inst_7 : NormedSpace 𝕜 G
inst_8 : SMulCommClass ℝ 𝕜 G
f : 𝓢(E, F →L[ℝ] G)
m : F
x : E
⊢ Eq.{u_7 + 1} (α := G)
    ((((SchwartzMap.evalCLM 𝕜 E G m : (a : 𝓢(E, F →L[ℝ] G)) → 𝓢(E, G)) f : 𝓢(E, G)) : (a : E) → G) x : G)
    ((((f : (a : E) → F →L[ℝ] G) x : F →L[ℝ] G) : (a : F) → G) m : G)

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 : 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
x x_1 : 𝓢(D, E)
x_2 : D
⊢ (fun (f : 𝓢(D, E)) (x : D) ↦
        ((((B : (a : E) → F →L[𝕜] G) ((f : (a : D) → E) x) : F →L[𝕜] G) : (a : F) → G) (g x) : G))
      (x + x_1) x_2 =
    HAdd.hAdd (α := G)
      ((fun (f : 𝓢(D, E)) (x : D) ↦
          ((((B : (a : E) → F →L[𝕜] G) ((f : (a : D) → E) x) : F →L[𝕜] G) : (a : F) → G) (g x) : G))
        x x_2)
      ((fun (f : 𝓢(D, E)) (x : D) ↦
          ((((B : (a : E) → F →L[𝕜] G) ((f : (a : D) → E) x) : F →L[𝕜] G) : (a : F) → G) (g x) : G))
        x_1 x_2)

Tactic:
simp
-- 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
x : 𝕜
x_1 : 𝓢(D, E)
x_2 : D
⊢ (fun (f : 𝓢(D, E)) (x : D) ↦
        ((((B : (a : E) → F →L[𝕜] G) ((f : (a : D) → E) x) : F →L[𝕜] G) : (a : F) → G) (g x) : G))
      (x • x_1) x_2 =
    HSMul.hSMul (α := 𝕜) (β := G) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) x : 𝕜)
      ((fun (f : 𝓢(D, E)) (x : D) ↦
          ((((B : (a : E) → F →L[𝕜] G) ((f : (a : D) → E) x) : F →L[𝕜] G) : (a : F) → G) (g x) : G))
        x_1 x_2)

Tactic:
simp
-- 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 : ℕ
rcases :
  ∀ (l : ℕ) (C : ℝ) (hC : 0 ≤ C)
    (hgrowth :
      ∀ N ≤ n,
        ∀ (x : D),
          norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_6} ℝ (fun (i : Fin N) ↦ D) F) (iteratedFDeriv ℝ N g x) ≤
            C * (1 + ‖x‖) ^ l),
    ∃ (s : Finset (ℕ × ℕ)) (C : ℝ),
      0 ≤ C ∧
        ∀ (f : 𝓢(D, E)) (x : D),
          ‖x‖ ^ (k, n).1 *
              norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_7} ℝ (fun (i : Fin (k, n).2) ↦ D) G)
                (iteratedFDeriv ℝ (k, n).2
                  ((fun (f : 𝓢(D, E)) (x : D) ↦
                      ((((B : (a : E) → F →L[𝕜] G) ((f : (a : D) → E) x) : F →L[𝕜] G) : (a : F) → G) (g x) : G))
                    f)
                  x) ≤
            HMul.hMul (β := ℝ) C ((s.sup (schwartzSeminormFamily 𝕜 D E) : (a : 𝓢(D, E)) → ℝ) f : ℝ)
⊢ ∃ (s : Finset (ℕ × ℕ)) (C : ℝ),
    0 ≤ C ∧
      ∀ (f : 𝓢(D, E)) (x : D),
        ‖x‖ ^ (k, n).1 *
            norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_7} ℝ (fun (i : Fin (k, n).2) ↦ D) G)
              (iteratedFDeriv ℝ (k, n).2
                ((fun (f : 𝓢(D, E)) (x : D) ↦
                    ((((B : (a : E) → F →L[𝕜] G) ((f : (a : D) → E) x) : F →L[𝕜] G) : (a : F) → G) (g x) : G))
                  f)
                x) ≤
          HMul.hMul (β := ℝ) C ((s.sup (schwartzSeminormFamily 𝕜 D E) : (a : 𝓢(D, E)) → ℝ) f : ℝ)

Tactic:
rcases hg.norm_iteratedFDeriv_le_uniform n with ⟨l, C, hC, hgrowth⟩

Premises used: Function.HasTemperateGrowth.norm_iteratedFDeriv_le_uniform
-- 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
hgrowth :
  ∀ N ≤ n,
    ∀ (x : D),
      norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_6} ℝ (fun (i : Fin N) ↦ D) F) (iteratedFDeriv ℝ N g x) ≤
        C * (1 + ‖x‖) ^ l
⊢ 0 ≤ ‖B‖ * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (↑(n.choose (n / 2)) : ℝ) * (C * HPow.hPow (α := ℝ) 2 (l + k))

Tactic:
positivity
-- 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
hgrowth :
  ∀ N ≤ n,
    ∀ (x : D),
      norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_6} ℝ (fun (i : Fin N) ↦ D) F) (iteratedFDeriv ℝ N g x) ≤
        C * (1 + ‖x‖) ^ l
right :
  ∀ (f : 𝓢(D, E)) (x : D),
    ‖x‖ ^ (k, n).1 *
        norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_7} ℝ (fun (i : Fin (k, n).2) ↦ D) G)
          (iteratedFDeriv ℝ (k, n).2
            ((fun (f : 𝓢(D, E)) (x : D) ↦
                ((((B : (a : E) → F →L[𝕜] G) ((f : (a : D) → E) x) : F →L[𝕜] G) : (a : F) → G) (g x) : G))
              f)
            x) ≤
      HMul.hMul (β := ℝ)
        (‖B‖ * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (↑(n.choose (n / 2)) : ℝ) * (C * HPow.hPow (α := ℝ) 2 (l + k)))
        (((Finset.Iic (l + k, n)).sup (schwartzSeminormFamily 𝕜 D E) : (a : 𝓢(D, E)) → ℝ) f : ℝ)
⊢ ∃ (s : Finset (ℕ × ℕ)) (C : ℝ),
    0 ≤ C ∧
      ∀ (f : 𝓢(D, E)) (x : D),
        ‖x‖ ^ (k, n).1 *
            norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_7} ℝ (fun (i : Fin (k, n).2) ↦ D) G)
              (iteratedFDeriv ℝ (k, n).2
                ((fun (f : 𝓢(D, E)) (x : D) ↦
                    ((((B : (a : E) → F →L[𝕜] G) ((f : (a : D) → E) x) : F →L[𝕜] G) : (a : F) → G) (g x) : G))
                  f)
                x) ≤
          HMul.hMul (β := ℝ) C ((s.sup (schwartzSeminormFamily 𝕜 D E) : (a : 𝓢(D, E)) → ℝ) f : ℝ)

Tactic:
use
    Finset.Iic (l + k, n), ‖B‖ * ((n : ℝ) + (1 : ℝ)) * n.choose (n / 2) * (C * 2 ^ (l + k)),
    by positivity

Premises used: Nat.choose, HMul.hMul, HDiv.hDiv, Prod.mk, Nat.cast, HPow.hPow, HAdd.hAdd, Finset.Iic, OfNat.ofNat
-- 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
hgrowth :
  ∀ N ≤ n,
    ∀ (x : D),
      norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_6} ℝ (fun (i : Fin N) ↦ D) F) (iteratedFDeriv ℝ N g x) ≤
        C * (1 + ‖x‖) ^ l
f : 𝓢(D, E)
x : D
⊢ 0 ≤ ‖x‖ ^ k

Tactic:
positivity
-- 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
hgrowth :
  ∀ N ≤ n,
    ∀ (x : D),
      norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_6} ℝ (fun (i : Fin N) ↦ D) F) (iteratedFDeriv ℝ N g x) ≤
        C * (1 + ‖x‖) ^ l
f : 𝓢(D, E)
x : D
⊢ 0 ≤ ‖x‖ ^ k

Tactic:
have hxk : 0 ≤ ‖x‖ ^ k := by positivity
-- 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
hgrowth :
  ∀ N ≤ n,
    ∀ (x : D),
      norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_6} ℝ (fun (i : Fin N) ↦ D) F) (iteratedFDeriv ℝ N g x) ≤
        C * (1 + ‖x‖) ^ l
f : 𝓢(D, E)
x : D
hxk : 0 ≤ ‖x‖ ^ k
right :
  ‖x‖ ^ k *
      norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_7} ℝ (fun (i : Fin n) ↦ D) G)
        (iteratedFDeriv ℝ n
          (fun (x : D) ↦
            (((ContinuousLinearMap.bilinearRestrictScalars ℝ B : (a : E) → F →L[ℝ] G) ((f : (a : D) → E) x) :
                  F →L[ℝ] G) :
                (a : F) → G)
              (g x))
          x) ≤
    HMul.hMul (β := ℝ)
      (‖B‖ * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (↑(n.choose (n / 2)) : ℝ) * (C * HPow.hPow (α := ℝ) 2 (l + k)))
      (((Finset.Iic (l + k, n)).sup (schwartzSeminormFamily 𝕜 D E) : (a : 𝓢(D, E)) → ℝ) f : ℝ)
⊢ ‖x‖ ^ (k, n).1 *
      norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_7} ℝ (fun (i : Fin (k, n).2) ↦ D) G)
        (iteratedFDeriv ℝ (k, n).2
          ((fun (f : 𝓢(D, E)) (x : D) ↦
              ((((B : (a : E) → F →L[𝕜] G) ((f : (a : D) → E) x) : F →L[𝕜] G) : (a : F) → G) (g x) : G))
            f)
          x) ≤
    HMul.hMul (β := ℝ)
      (‖B‖ * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (↑(n.choose (n / 2)) : ℝ) * (C * HPow.hPow (α := ℝ) 2 (l + k)))
      (((Finset.Iic (l + k, n)).sup (schwartzSeminormFamily 𝕜 D E) : (a : 𝓢(D, E)) → ℝ) f : ℝ)

Tactic:
simp_rw [← ContinuousLinearMap.bilinearRestrictScalars_apply_apply ℝ B]

Premises used: Real, ContinuousLinearMap.bilinearRestrictScalars_apply_apply