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

Tactic:
exact DFunLike.coe_injective

Premises used: DFunLike.coe_injective
-- 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)
⊢ Eq (α := ℝ) ((SchwartzMap.seminorm 𝕜 k n : (a : 𝓢(E, F)) → ℝ) f : ℝ)
    (sInf
        {c : ℝ |
          0 ≤ 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:
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 : NormedField 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 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
⊢ (SchwartzMap.seminorm 𝕜 k n : (a : 𝓢(E, F)) → ℝ) f ≤ M

Tactic:
f.seminormAux_le_bound k n hMp hM

Premises used: _private.0.SchwartzMap.seminormAux_le_bound, _private.0.SchwartzMap.seminormAux
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
𝕜 : Type u_2
F : Type u_6
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : NormedField 𝕜
inst_3 : NormedSpace 𝕜 F
inst_4 : SMulCommClass ℝ 𝕜 F
k n : ℕ
f : 𝓢(ℝ, F)
M : ℝ
hMp : 0 ≤ M
hM : ∀ (x : ℝ), |x| ^ k * norm (E := F) (iteratedDeriv n (⇑f : (a : ℝ) → F) x) ≤ M
⊢ (SchwartzMap.seminorm 𝕜 k n : (a : 𝓢(ℝ, F)) → ℝ) f ≤ M

Tactic:
seminorm_le_bound 𝕜 k n f hMp ?_

Premises used: SchwartzMap.seminorm_le_bound
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
𝕜 : Type u_2
F : Type u_6
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : NormedField 𝕜
inst_3 : NormedSpace 𝕜 F
inst_4 : SMulCommClass ℝ 𝕜 F
k n : ℕ
f : 𝓢(ℝ, F)
M : ℝ
hMp : 0 ≤ M
hM : ∀ (x : ℝ), |x| ^ k * norm (E := F) (iteratedDeriv n (⇑f : (a : ℝ) → F) x) ≤ M
refine :
  ∀ (x : ℝ),
    ‖x‖ ^ k * norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ ℝ) F) (iteratedFDeriv ℝ n (⇑f : (a : ℝ) → F) x) ≤
      M
⊢ (SchwartzMap.seminorm 𝕜 k n : (a : 𝓢(ℝ, F)) → ℝ) f ≤ M

Tactic:
refine seminorm_le_bound 𝕜 k n f hMp ?_

Premises used: SchwartzMap.seminorm_le_bound
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
𝕜 : Type u_2
F : Type u_6
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : NormedField 𝕜
inst_3 : NormedSpace 𝕜 F
inst_4 : SMulCommClass ℝ 𝕜 F
k n : ℕ
f : 𝓢(ℝ, F)
M : ℝ
hMp : 0 ≤ M
hM : ∀ (x : ℝ), |x| ^ k * norm (E := F) (iteratedDeriv n (⇑f : (a : ℝ) → F) x) ≤ M
⊢ ∀ (x : ℝ),
    ‖x‖ ^ k * norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ ℝ) F) (iteratedFDeriv ℝ n (⇑f : (a : ℝ) → F) x) ≤
      M

Tactic:
simpa only [Real.norm_eq_abs, norm_iteratedFDeriv_eq_norm_iteratedDeriv]

Premises used: norm_iteratedFDeriv_eq_norm_iteratedDeriv, Real.norm_eq_abs
-- 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)
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) ≤
    (SchwartzMap.seminorm 𝕜 k n : (a : 𝓢(E, F)) → ℝ) f

Tactic:
f.le_seminormAux k n x

Premises used: _private.0.SchwartzMap.le_seminormAux, _private.0.SchwartzMap.seminormAux
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
𝕜 : Type u_2
F : Type u_6
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : NormedField 𝕜
inst_3 : NormedSpace 𝕜 F
inst_4 : SMulCommClass ℝ 𝕜 F
k n : ℕ
f : 𝓢(ℝ, F)
x : ℝ
⊢ ‖x‖ ^ k * norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ ℝ) F) (iteratedFDeriv ℝ n (⇑f : (a : ℝ) → F) x) ≤
    (SchwartzMap.seminorm 𝕜 k n : (a : 𝓢(ℝ, F)) → ℝ) f

Tactic:
have := le_seminorm 𝕜 k n f x
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
𝕜 : Type u_2
F : Type u_6
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : NormedField 𝕜
inst_3 : NormedSpace 𝕜 F
inst_4 : SMulCommClass ℝ 𝕜 F
k n : ℕ
f : 𝓢(ℝ, F)
x : ℝ
this :
  ‖x‖ ^ k * norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ ℝ) F) (iteratedFDeriv ℝ n (⇑f : (a : ℝ) → F) x) ≤
    (SchwartzMap.seminorm 𝕜 k n : (a : 𝓢(ℝ, F)) → ℝ) f
rwa :
  ‖x‖ ^ k * norm (E := F) (iteratedDeriv n (⇑f : (a : ℝ) → F) x) ≤ (SchwartzMap.seminorm 𝕜 k n : (a : 𝓢(ℝ, F)) → ℝ) f
rwa₁ rwa₂ rwa₃ rwa₄ :
  ‖x‖ ^ k * norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ ℝ) F) (iteratedFDeriv ℝ n (⇑f : (a : ℝ) → F) x) ≤
    (SchwartzMap.seminorm 𝕜 k n : (a : 𝓢(ℝ, F)) → ℝ) f
⊢ |x| ^ k * norm (E := F) (iteratedDeriv n (⇑f : (a : ℝ) → F) x) ≤ (SchwartzMap.seminorm 𝕜 k n : (a : 𝓢(ℝ, F)) → ℝ) f

Tactic:
rwa [← Real.norm_eq_abs, ← norm_iteratedFDeriv_eq_norm_iteratedDeriv]

Premises used: norm_iteratedFDeriv_eq_norm_iteratedDeriv, Real.norm_eq_abs
-- 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)
n : ℕ
x₀ : E
⊢ HPow.hPow (β := ℕ) ‖x₀‖ 0 *
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
        (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x₀) ≤
    (SchwartzMap.seminorm 𝕜 0 n : (a : 𝓢(E, F)) → ℝ) f

Tactic:
have := SchwartzMap.le_seminorm 𝕜 0 n 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 : NormedField 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
f : 𝓢(E, F)
n : ℕ
x₀ : E
this :
  HPow.hPow (β := ℕ) ‖x₀‖ 0 *
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
        (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x₀) ≤
    (SchwartzMap.seminorm 𝕜 0 n : (a : 𝓢(E, F)) → ℝ) f
rwa :
  ∀
    (this :
      1 *
          norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
            (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x₀) ≤
        (SchwartzMap.seminorm 𝕜 0 n : (a : 𝓢(E, F)) → ℝ) f),
    norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
        (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x₀) ≤
      (SchwartzMap.seminorm 𝕜 0 n : (a : 𝓢(E, F)) → ℝ) f
rwa₁ rwa₂ rwa₃ rwa₄ :
  ∀
    (this :
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
          (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x₀) ≤
        (SchwartzMap.seminorm 𝕜 0 n : (a : 𝓢(E, F)) → ℝ) f),
    norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
        (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x₀) ≤
      (SchwartzMap.seminorm 𝕜 0 n : (a : 𝓢(E, F)) → ℝ) f
⊢ norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
      (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x₀) ≤
    (SchwartzMap.seminorm 𝕜 0 n : (a : 𝓢(E, F)) → ℝ) f

Tactic:
rwa [pow_zero, one_mul] at this

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

Tactic:
have := SchwartzMap.le_seminorm 𝕜 k 0 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 : NormedField 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
f : 𝓢(E, F)
k : ℕ
x₀ : E
this :
  ‖x₀‖ ^ k *
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin 0) ↦ E) F)
        (iteratedFDeriv ℝ 0 (⇑f : (a : E) → F) x₀) ≤
    (SchwartzMap.seminorm 𝕜 k 0 : (a : 𝓢(E, F)) → ℝ) f
rwa rwa₁ rwa₂ rwa₃ :
  ∀
    (this :
      ‖x₀‖ ^ k * norm.{u_6} (E := F) ((f : (a : E) → F) x₀ : F) ≤ (SchwartzMap.seminorm 𝕜 k 0 : (a : 𝓢(E, F)) → ℝ) f),
    ‖x₀‖ ^ k * norm.{u_6} (E := F) ((f : (a : E) → F) x₀ : F) ≤ (SchwartzMap.seminorm 𝕜 k 0 : (a : 𝓢(E, F)) → ℝ) f
⊢ ‖x₀‖ ^ k * norm.{u_6} (E := F) ((f : (a : E) → F) x₀ : F) ≤ (SchwartzMap.seminorm 𝕜 k 0 : (a : 𝓢(E, F)) → ℝ) f

Tactic:
rwa [norm_iteratedFDeriv_zero] at this

Premises used: norm_iteratedFDeriv_zero
-- 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)
x₀ : E
⊢ HPow.hPow (β := ℕ) ‖x₀‖ 0 * norm.{u_6} (E := F) ((f : (a : E) → F) x₀ : F) ≤
    (SchwartzMap.seminorm 𝕜 0 0 : (a : 𝓢(E, F)) → ℝ) f

Tactic:
have := norm_pow_mul_le_seminorm 𝕜 f 0 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 : NormedField 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
f : 𝓢(E, F)
x₀ : E
this :
  HPow.hPow (β := ℕ) ‖x₀‖ 0 * norm.{u_6} (E := F) ((f : (a : E) → F) x₀ : F) ≤
    (SchwartzMap.seminorm 𝕜 0 0 : (a : 𝓢(E, F)) → ℝ) f
rwa :
  ∀ (this : 1 * norm.{u_6} (E := F) ((f : (a : E) → F) x₀ : F) ≤ (SchwartzMap.seminorm 𝕜 0 0 : (a : 𝓢(E, F)) → ℝ) f),
    norm.{u_6} (E := F) ((f : (a : E) → F) x₀ : F) ≤ (SchwartzMap.seminorm 𝕜 0 0 : (a : 𝓢(E, F)) → ℝ) f
rwa₁ rwa₂ rwa₃ rwa₄ :
  ∀ (this : norm.{u_6} (E := F) ((f : (a : E) → F) x₀ : F) ≤ (SchwartzMap.seminorm 𝕜 0 0 : (a : 𝓢(E, F)) → ℝ) f),
    norm.{u_6} (E := F) ((f : (a : E) → F) x₀ : F) ≤ (SchwartzMap.seminorm 𝕜 0 0 : (a : 𝓢(E, F)) → ℝ) f
⊢ norm.{u_6} (E := F) ((f : (a : E) → F) x₀ : F) ≤ (SchwartzMap.seminorm 𝕜 0 0 : (a : 𝓢(E, F)) → ℝ) f

Tactic:
rwa [pow_zero, one_mul] at this

Premises used: pow_zero, one_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 : NormedField 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
n k : ℕ
⊢ Eq (α := Seminorm 𝕜 𝓢(E, F)) (schwartzSeminormFamily 𝕜 E F (n, k)) (SchwartzMap.seminorm 𝕜 n k)

Tactic:
rfl

Premises used: SchwartzMap.seminorm, schwartzSeminormFamily, 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 : NormedField 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
⊢ Eq (α := Seminorm 𝕜 𝓢(E, F)) (schwartzSeminormFamily 𝕜 E F 0) (SchwartzMap.seminorm 𝕜 0 0)

Tactic:
rfl

Premises used: SchwartzMap.seminorm, schwartzSeminormFamily, 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 : NormedField 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
m : ℕ × ℕ
k n : ℕ
hk : k ≤ m.1
hn : n ≤ m.2
f : 𝓢(E, F)
x : E
rw :
  (∑ m ∈ Finset.range (k + 1), ‖x‖ ^ m * HPow.hPow (α := ℝ) 1 (k - m) * (↑(k.choose m) : ℝ)) *
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
        (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x) ≤
    HMul.hMul (β := ℝ) (HPow.hPow (α := ℝ) 2 m.1)
      (((Finset.Iic m).sup fun (m : ℕ × ℕ) ↦ SchwartzMap.seminorm 𝕜 m.1 m.2 : (a : 𝓢(E, F)) → ℝ) f : ℝ)
⊢ (1 + ‖x‖) ^ k *
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
        (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x) ≤
    HMul.hMul (β := ℝ) (HPow.hPow (α := ℝ) 2 m.1)
      (((Finset.Iic m).sup fun (m : ℕ × ℕ) ↦ SchwartzMap.seminorm 𝕜 m.1 m.2 : (a : 𝓢(E, F)) → ℝ) f : ℝ)

Tactic:
rw [add_comm, add_pow]

Premises used: add_comm, add_pow
-- 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
m : ℕ × ℕ
k n : ℕ
hk : k ≤ m.1
hn : n ≤ m.2
f : 𝓢(E, F)
x : E
simp :
  ∑ i ∈ Finset.range (k + 1),
      ‖x‖ ^ i * (↑(k.choose i) : ℝ) *
        norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
          (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x) ≤
    HMul.hMul (β := ℝ) (HPow.hPow (α := ℝ) 2 m.1)
      (((Finset.Iic m).sup fun (m : ℕ × ℕ) ↦ SchwartzMap.seminorm 𝕜 m.1 m.2 : (a : 𝓢(E, F)) → ℝ) f : ℝ)
⊢ (∑ m ∈ Finset.range (k + 1), ‖x‖ ^ m * HPow.hPow (α := ℝ) 1 (k - m) * (↑(k.choose m) : ℝ)) *
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
        (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x) ≤
    HMul.hMul (β := ℝ) (HPow.hPow (α := ℝ) 2 m.1)
      (((Finset.Iic m).sup fun (m : ℕ × ℕ) ↦ SchwartzMap.seminorm 𝕜 m.1 m.2 : (a : 𝓢(E, F)) → ℝ) f : ℝ)

Tactic:
simp only [one_pow, mul_one, Finset.sum_mul]

Premises used: one_pow, mul_one, Finset.sum_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 : NormedField 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
m : ℕ × ℕ
k n : ℕ
hk : k ≤ m.1
hn : n ≤ m.2
f : 𝓢(E, F)
x : E
norm_cast :
  ∑ i ∈ Finset.range (k + 1),
      ‖x‖ ^ i * (↑(k.choose i) : ℝ) *
        norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
          (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x) ≤
    HMul.hMul (α := ℝ) (β := ℝ) ((↑(HPow.hPow (α := ℕ) 2 m.1) : ℝ) : ℝ)
      (((Finset.Iic m).sup fun (m : ℕ × ℕ) ↦ SchwartzMap.seminorm 𝕜 m.1 m.2 : (a : 𝓢(E, F)) → ℝ) f : ℝ)
⊢ ∑ i ∈ Finset.range (k + 1),
      ‖x‖ ^ i * (↑(k.choose i) : ℝ) *
        norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
          (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x) ≤
    HMul.hMul (β := ℝ) (HPow.hPow (α := ℝ) 2 m.1)
      (((Finset.Iic m).sup fun (m : ℕ × ℕ) ↦ SchwartzMap.seminorm 𝕜 m.1 m.2 : (a : 𝓢(E, F)) → ℝ) f : ℝ)

Tactic:
norm_cast
-- 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
m : ℕ × ℕ
k n : ℕ
hk : k ≤ m.1
hn : n ≤ m.2
f : 𝓢(E, F)
x : E
rw :
  ∑ i ∈ Finset.range (k + 1),
      ‖x‖ ^ i * (↑(k.choose i) : ℝ) *
        norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
          (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x) ≤
    HMul.hMul (α := ℝ) (β := ℝ) ((↑(∑ m_1 ∈ Finset.range (m.1 + 1), m.1.choose m_1) : ℝ) : ℝ)
      (((Finset.Iic m).sup fun (m : ℕ × ℕ) ↦ SchwartzMap.seminorm 𝕜 m.1 m.2 : (a : 𝓢(E, F)) → ℝ) f : ℝ)
⊢ ∑ i ∈ Finset.range (k + 1),
      ‖x‖ ^ i * (↑(k.choose i) : ℝ) *
        norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
          (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x) ≤
    HMul.hMul (α := ℝ) (β := ℝ) ((↑(HPow.hPow (α := ℕ) 2 m.1) : ℝ) : ℝ)
      (((Finset.Iic m).sup fun (m : ℕ × ℕ) ↦ SchwartzMap.seminorm 𝕜 m.1 m.2 : (a : 𝓢(E, F)) → ℝ) f : ℝ)

Tactic:
rw [← Nat.sum_range_choose m.1]

Premises used: Nat.sum_range_choose, Prod.fst
-- 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
m : ℕ × ℕ
k n : ℕ
hk : k ≤ m.1
hn : n ≤ m.2
f : 𝓢(E, F)
x : E
push_cast :
  ∑ i ∈ Finset.range (k + 1),
      ‖x‖ ^ i * (↑(k.choose i) : ℝ) *
        norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
          (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x) ≤
    HMul.hMul (α := ℝ) (β := ℝ) (∑ x ∈ Finset.range (m.1 + 1), (↑(m.1.choose x) : ℝ) : ℝ)
      (((Finset.Iic m).sup fun (m : ℕ × ℕ) ↦ SchwartzMap.seminorm 𝕜 m.1 m.2 : (a : 𝓢(E, F)) → ℝ) f : ℝ)
⊢ ∑ i ∈ Finset.range (k + 1),
      ‖x‖ ^ i * (↑(k.choose i) : ℝ) *
        norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
          (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x) ≤
    HMul.hMul (α := ℝ) (β := ℝ) ((↑(∑ m_1 ∈ Finset.range (m.1 + 1), m.1.choose m_1) : ℝ) : ℝ)
      (((Finset.Iic m).sup fun (m : ℕ × ℕ) ↦ SchwartzMap.seminorm 𝕜 m.1 m.2 : (a : 𝓢(E, F)) → ℝ) f : ℝ)

Tactic:
push_cast
-- 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
m : ℕ × ℕ
k n : ℕ
hk : k ≤ m.1
hn : n ≤ m.2
f : 𝓢(E, F)
x : E
rw :
  LE.le (α := ℝ)
    (∑ i ∈ Finset.range (k + 1),
      ‖x‖ ^ i * (↑(k.choose i) : ℝ) *
        norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
          (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x))
    (∑ i ∈ Finset.range (m.1 + 1),
      HMul.hMul (α := ℝ) (β := ℝ) ((↑(m.1.choose i) : ℝ) : ℝ)
        (((Finset.Iic m).sup fun (m : ℕ × ℕ) ↦ SchwartzMap.seminorm 𝕜 m.1 m.2 : (a : 𝓢(E, F)) → ℝ) f : ℝ))
⊢ ∑ i ∈ Finset.range (k + 1),
      ‖x‖ ^ i * (↑(k.choose i) : ℝ) *
        norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
          (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x) ≤
    HMul.hMul (α := ℝ) (β := ℝ) (∑ x ∈ Finset.range (m.1 + 1), (↑(m.1.choose x) : ℝ) : ℝ)
      (((Finset.Iic m).sup fun (m : ℕ × ℕ) ↦ SchwartzMap.seminorm 𝕜 m.1 m.2 : (a : 𝓢(E, F)) → ℝ) f : ℝ)

Tactic:
rw [Finset.sum_mul]

Premises used: Finset.sum_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 : NormedField 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
m : ℕ × ℕ
k n : ℕ
hk : k ≤ m.1
hn : n ≤ m.2
f : 𝓢(E, F)
x : E
⊢ Finset.range (k + 1) ⊆ Finset.range (m.1 + 1)

Tactic:
grind
-- 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
m : ℕ × ℕ
k n : ℕ
hk : k ≤ m.1
hn : n ≤ m.2
f : 𝓢(E, F)
x : E
⊢ Finset.range (k + 1) ⊆ Finset.range (m.1 + 1)

Tactic:
have hk' : Finset.range (k + 1) ⊆ Finset.range (m.1 + 1) := by grind
-- 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
m : ℕ × ℕ
k n : ℕ
hk : k ≤ m.1
hn : n ≤ m.2
f : 𝓢(E, F)
x : E
hk' : Finset.range (k + 1) ⊆ Finset.range (m.1 + 1)
grw :
  LE.le (α := ℝ)
    (∑ i ∈ Finset.range (m.1 + 1),
      ‖x‖ ^ i * (↑(k.choose i) : ℝ) *
        norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
          (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x))
    (∑ i ∈ Finset.range (m.1 + 1),
      HMul.hMul (α := ℝ) (β := ℝ) ((↑(m.1.choose i) : ℝ) : ℝ)
        (((Finset.Iic m).sup fun (m : ℕ × ℕ) ↦ SchwartzMap.seminorm 𝕜 m.1 m.2 : (a : 𝓢(E, F)) → ℝ) f : ℝ))
⊢ LE.le (α := ℝ)
    (∑ i ∈ Finset.range (k + 1),
      ‖x‖ ^ i * (↑(k.choose i) : ℝ) *
        norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
          (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x))
    (∑ i ∈ Finset.range (m.1 + 1),
      HMul.hMul (α := ℝ) (β := ℝ) ((↑(m.1.choose i) : ℝ) : ℝ)
        (((Finset.Iic m).sup fun (m : ℕ × ℕ) ↦ SchwartzMap.seminorm 𝕜 m.1 m.2 : (a : 𝓢(E, F)) → ℝ) f : ℝ))

Tactic:
grw [hk']
-- 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
m : ℕ × ℕ
k n : ℕ
hk : k ≤ m.1
hn : n ≤ m.2
f : 𝓢(E, F)
x : E
hk' : Finset.range (k + 1) ⊆ Finset.range (m.1 + 1)
h :
  ∀ (i : ℕ) (hi : i ∈ Finset.range (m.1 + 1)),
    ‖x‖ ^ i * (↑(k.choose i) : ℝ) *
        norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
          (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x) ≤
      HMul.hMul (α := ℝ) (β := ℝ) ((↑(m.1.choose i) : ℝ) : ℝ)
        (((Finset.Iic m).sup fun (m : ℕ × ℕ) ↦ SchwartzMap.seminorm 𝕜 m.1 m.2 : (a : 𝓢(E, F)) → ℝ) f : ℝ)
⊢ LE.le (α := ℝ)
    (∑ i ∈ Finset.range (m.1 + 1),
      ‖x‖ ^ i * (↑(k.choose i) : ℝ) *
        norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
          (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x))
    (∑ i ∈ Finset.range (m.1 + 1),
      HMul.hMul (α := ℝ) (β := ℝ) ((↑(m.1.choose i) : ℝ) : ℝ)
        (((Finset.Iic m).sup fun (m : ℕ × ℕ) ↦ SchwartzMap.seminorm 𝕜 m.1 m.2 : (a : 𝓢(E, F)) → ℝ) f : ℝ))

Tactic:
gcongr ∑ _i ∈ Finset.range (m.1 + 1), ?_ with i hi

Premises used: Prod.fst, Finset.range, HAdd.hAdd, OfNat.ofNat
-- 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
m : ℕ × ℕ
k n : ℕ
hk : k ≤ m.1
hn : n ≤ m.2
f : 𝓢(E, F)
x : E
hk' : Finset.range (k + 1) ⊆ Finset.range (m.1 + 1)
i : ℕ
hi : i ∈ Finset.range (m.1 + 1)
h :
  ‖x‖ ^ i *
        norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
          (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x) *
      (↑(k.choose i) : ℝ) ≤
    HMul.hMul (α := ℝ) (β := ℝ)
      (((Finset.Iic m).sup fun (m : ℕ × ℕ) ↦ SchwartzMap.seminorm 𝕜 m.1 m.2 : (a : 𝓢(E, F)) → ℝ) f : ℝ)
      ((↑(m.1.choose i) : ℝ) : ℝ)
⊢ ‖x‖ ^ i * (↑(k.choose i) : ℝ) *
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
        (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x) ≤
    HMul.hMul (α := ℝ) (β := ℝ) ((↑(m.1.choose i) : ℝ) : ℝ)
      (((Finset.Iic m).sup fun (m : ℕ × ℕ) ↦ SchwartzMap.seminorm 𝕜 m.1 m.2 : (a : 𝓢(E, F)) → ℝ) f : ℝ)

Tactic:
move_mul [(Nat.choose k i : ℝ), (Nat.choose m.1 i : ℝ)]

Premises used: Nat.choose, Nat.cast, Prod.fst