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

Tactic:
have hnorm_mul :=
    ContinuousLinearMap.norm_iteratedFDeriv_le_of_bilinear (B.bilinearRestrictScalars ℝ)
    (f.smooth ⊤) hg.1 x (n := n) (mod_cast le_top)
-- 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
hnorm_mul :
  norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_7} ℝ (fun (i : Fin n) ↦ D) G)
      (iteratedFDeriv ℝ n
        (fun (y : D) ↦
          (((ContinuousLinearMap.bilinearRestrictScalars ℝ B : (a : E) → F →L[ℝ] G) ((f : (a : D) → E) y) : F →L[ℝ] G) :
              (a : F) → G)
            (g y))
        x) ≤
    norm (E := E →L[ℝ] F →L[ℝ] G) (ContinuousLinearMap.bilinearRestrictScalars ℝ B) *
      ∑ i ∈ Finset.range (n + 1),
        (↑(n.choose i) : ℝ) *
            norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_5} ℝ (fun (i : Fin i) ↦ D) E)
              (iteratedFDeriv ℝ i (⇑f : (a : D) → E) x) *
          norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_6} ℝ (fun (i : Fin (n - i)) ↦ D) F)
            (iteratedFDeriv ℝ (n - i) g x)
right :
  ‖x‖ ^ k *
      (norm (E := E →L[ℝ] F →L[ℝ] G) (ContinuousLinearMap.bilinearRestrictScalars ℝ B) *
        ∑ i ∈ Finset.range (n + 1),
          (↑(n.choose i) : ℝ) *
              norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_5} ℝ (fun (i : Fin i) ↦ D) E)
                (iteratedFDeriv ℝ i (⇑f : (a : D) → E) x) *
            norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_6} ℝ (fun (i : Fin (n - i)) ↦ D) F)
              (iteratedFDeriv ℝ (n - i) g x)) ≤
    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 *
      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 : ℝ)

Tactic:
grw [hnorm_mul]
-- 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
hnorm_mul :
  norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_7} ℝ (fun (i : Fin n) ↦ D) G)
      (iteratedFDeriv ℝ n
        (fun (y : D) ↦
          (((ContinuousLinearMap.bilinearRestrictScalars ℝ B : (a : E) → F →L[ℝ] G) ((f : (a : D) → E) y) : F →L[ℝ] G) :
              (a : F) → G)
            (g y))
        x) ≤
    norm (E := E →L[ℝ] F →L[ℝ] G) (ContinuousLinearMap.bilinearRestrictScalars ℝ B) *
      ∑ i ∈ Finset.range (n + 1),
        (↑(n.choose i) : ℝ) *
            norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_5} ℝ (fun (i : Fin i) ↦ D) E)
              (iteratedFDeriv ℝ i (⇑f : (a : D) → E) x) *
          norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_6} ℝ (fun (i : Fin (n - i)) ↦ D) F)
            (iteratedFDeriv ℝ (n - i) g x)
right :
  ‖x‖ ^ k *
      (‖B‖ *
        ∑ i ∈ Finset.range (n + 1),
          (↑(n.choose i) : ℝ) *
              norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_5} ℝ (fun (i : Fin i) ↦ D) E)
                (iteratedFDeriv ℝ i (⇑f : (a : D) → E) x) *
            norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_6} ℝ (fun (i : Fin (n - i)) ↦ D) F)
              (iteratedFDeriv ℝ (n - i) g x)) ≤
    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 *
      (norm (E := E →L[ℝ] F →L[ℝ] G) (ContinuousLinearMap.bilinearRestrictScalars ℝ B) *
        ∑ i ∈ Finset.range (n + 1),
          (↑(n.choose i) : ℝ) *
              norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_5} ℝ (fun (i : Fin i) ↦ D) E)
                (iteratedFDeriv ℝ i (⇑f : (a : D) → E) x) *
            norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_6} ℝ (fun (i : Fin (n - i)) ↦ D) F)
              (iteratedFDeriv ℝ (n - i) g x)) ≤
    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:
rw [ContinuousLinearMap.norm_bilinearRestrictScalars]

Premises used: ContinuousLinearMap.norm_bilinearRestrictScalars
-- 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
hnorm_mul :
  norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_7} ℝ (fun (i : Fin n) ↦ D) G)
      (iteratedFDeriv ℝ n
        (fun (y : D) ↦
          (((ContinuousLinearMap.bilinearRestrictScalars ℝ B : (a : E) → F →L[ℝ] G) ((f : (a : D) → E) y) : F →L[ℝ] G) :
              (a : F) → G)
            (g y))
        x) ≤
    norm (E := E →L[ℝ] F →L[ℝ] G) (ContinuousLinearMap.bilinearRestrictScalars ℝ B) *
      ∑ i ∈ Finset.range (n + 1),
        (↑(n.choose i) : ℝ) *
            norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_5} ℝ (fun (i : Fin i) ↦ D) E)
              (iteratedFDeriv ℝ i (⇑f : (a : D) → E) x) *
          norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_6} ℝ (fun (i : Fin (n - i)) ↦ D) F)
            (iteratedFDeriv ℝ (n - i) g x)
right :
  (‖x‖ ^ k *
        ∑ i ∈ Finset.range (n + 1),
          (↑(n.choose i) : ℝ) *
              norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_5} ℝ (fun (i : Fin i) ↦ D) E)
                (iteratedFDeriv ℝ i (⇑f : (a : D) → E) x) *
            norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_6} ℝ (fun (i : Fin (n - i)) ↦ D) F)
              (iteratedFDeriv ℝ (n - i) g x)) *
      ‖B‖ ≤
    HMul.hMul (β := ℝ) (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 : ℝ) *
      ‖B‖
⊢ ‖x‖ ^ k *
      (‖B‖ *
        ∑ i ∈ Finset.range (n + 1),
          (↑(n.choose i) : ℝ) *
              norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_5} ℝ (fun (i : Fin i) ↦ D) E)
                (iteratedFDeriv ℝ i (⇑f : (a : D) → E) x) *
            norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_6} ℝ (fun (i : Fin (n - i)) ↦ D) F)
              (iteratedFDeriv ℝ (n - i) g x)) ≤
    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:
move_mul [‖B‖, ‖B‖]
-- 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
hnorm_mul :
  norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_7} ℝ (fun (i : Fin n) ↦ D) G)
      (iteratedFDeriv ℝ n
        (fun (y : D) ↦
          (((ContinuousLinearMap.bilinearRestrictScalars ℝ B : (a : E) → F →L[ℝ] G) ((f : (a : D) → E) y) : F →L[ℝ] G) :
              (a : F) → G)
            (g y))
        x) ≤
    norm (E := E →L[ℝ] F →L[ℝ] G) (ContinuousLinearMap.bilinearRestrictScalars ℝ B) *
      ∑ i ∈ Finset.range (n + 1),
        (↑(n.choose i) : ℝ) *
            norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_5} ℝ (fun (i : Fin i) ↦ D) E)
              (iteratedFDeriv ℝ i (⇑f : (a : D) → E) x) *
          norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_6} ℝ (fun (i : Fin (n - i)) ↦ D) F)
            (iteratedFDeriv ℝ (n - i) g x)
right :
  ‖x‖ ^ k *
      ∑ i ∈ Finset.range (n + 1),
        (↑(n.choose i) : ℝ) *
            norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_5} ℝ (fun (i : Fin i) ↦ D) E)
              (iteratedFDeriv ℝ i (⇑f : (a : D) → E) x) *
          norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_6} ℝ (fun (i : Fin (n - i)) ↦ D) F)
            (iteratedFDeriv ℝ (n - i) g x) ≤
    HMul.hMul (β := ℝ) (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 *
        ∑ i ∈ Finset.range (n + 1),
          (↑(n.choose i) : ℝ) *
              norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_5} ℝ (fun (i : Fin i) ↦ D) E)
                (iteratedFDeriv ℝ i (⇑f : (a : D) → E) x) *
            norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_6} ℝ (fun (i : Fin (n - i)) ↦ D) F)
              (iteratedFDeriv ℝ (n - i) g x)) *
      ‖B‖ ≤
    HMul.hMul (β := ℝ) (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 : ℝ) *
      ‖B‖

Tactic:
gcongr ?_ * _
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
D : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
H : Type u_8
V : Type u_9
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedAlgebra ℝ 𝕜
inst_6 : NormedAddCommGroup D
inst_7 : NormedSpace ℝ D
inst_8 : NormedAddCommGroup G
inst_9 : NormedSpace ℝ G
inst_10 : NormedSpace 𝕜 F
inst_11 : NormedSpace 𝕜 E
inst_12 : NormedSpace 𝕜 G
B : E →L[𝕜] F →L[𝕜] G
g : D → F
hg : Function.HasTemperateGrowth g
k n l : ℕ
C : ℝ
hC : 0 ≤ C
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
hnorm_mul :
  norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_7} ℝ (fun (i : Fin n) ↦ D) G)
      (iteratedFDeriv ℝ n
        (fun (y : D) ↦
          (((ContinuousLinearMap.bilinearRestrictScalars ℝ B : (a : E) → F →L[ℝ] G) ((f : (a : D) → E) y) : F →L[ℝ] G) :
              (a : F) → G)
            (g y))
        x) ≤
    norm (E := E →L[ℝ] F →L[ℝ] G) (ContinuousLinearMap.bilinearRestrictScalars ℝ B) *
      ∑ i ∈ Finset.range (n + 1),
        (↑(n.choose i) : ℝ) *
            norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_5} ℝ (fun (i : Fin i) ↦ D) E)
              (iteratedFDeriv ℝ i (⇑f : (a : D) → E) x) *
          norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_6} ℝ (fun (i : Fin (n - i)) ↦ D) F)
            (iteratedFDeriv ℝ (n - i) g x)
right :
  ∑ i ∈ Finset.range (n + 1),
      ‖x‖ ^ k *
        ((↑(n.choose i) : ℝ) *
            norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_5} ℝ (fun (i : Fin i) ↦ D) E)
              (iteratedFDeriv ℝ i (⇑f : (a : D) → E) x) *
          norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_6} ℝ (fun (i : Fin (n - i)) ↦ D) F)
            (iteratedFDeriv ℝ (n - i) g x)) ≤
    HMul.hMul (β := ℝ) (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 *
      ∑ i ∈ Finset.range (n + 1),
        (↑(n.choose i) : ℝ) *
            norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_5} ℝ (fun (i : Fin i) ↦ D) E)
              (iteratedFDeriv ℝ i (⇑f : (a : D) → E) x) *
          norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_6} ℝ (fun (i : Fin (n - i)) ↦ D) F)
            (iteratedFDeriv ℝ (n - i) g x) ≤
    HMul.hMul (β := ℝ) (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:
rw [Finset.mul_sum]

Premises used: Finset.mul_sum
-- 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
hnorm_mul :
  norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_7} ℝ (fun (i : Fin n) ↦ D) G)
      (iteratedFDeriv ℝ n
        (fun (y : D) ↦
          (((ContinuousLinearMap.bilinearRestrictScalars ℝ B : (a : E) → F →L[ℝ] G) ((f : (a : D) → E) y) : F →L[ℝ] G) :
              (a : F) → G)
            (g y))
        x) ≤
    norm (E := E →L[ℝ] F →L[ℝ] G) (ContinuousLinearMap.bilinearRestrictScalars ℝ B) *
      ∑ i ∈ Finset.range (n + 1),
        (↑(n.choose i) : ℝ) *
            norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_5} ℝ (fun (i : Fin i) ↦ D) E)
              (iteratedFDeriv ℝ i (⇑f : (a : D) → E) x) *
          norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_6} ℝ (fun (i : Fin (n - i)) ↦ D) F)
            (iteratedFDeriv ℝ (n - i) g x)
⊢ ∑ _x ∈ Finset.range (n + 1), 1 = HAdd.hAdd (α := ℝ) (↑n : ℝ) 1

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 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
hnorm_mul :
  norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_7} ℝ (fun (i : Fin n) ↦ D) G)
      (iteratedFDeriv ℝ n
        (fun (y : D) ↦
          (((ContinuousLinearMap.bilinearRestrictScalars ℝ B : (a : E) → F →L[ℝ] G) ((f : (a : D) → E) y) : F →L[ℝ] G) :
              (a : F) → G)
            (g y))
        x) ≤
    norm (E := E →L[ℝ] F →L[ℝ] G) (ContinuousLinearMap.bilinearRestrictScalars ℝ B) *
      ∑ i ∈ Finset.range (n + 1),
        (↑(n.choose i) : ℝ) *
            norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_5} ℝ (fun (i : Fin i) ↦ D) E)
              (iteratedFDeriv ℝ i (⇑f : (a : D) → E) x) *
          norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_6} ℝ (fun (i : Fin (n - i)) ↦ D) F)
            (iteratedFDeriv ℝ (n - i) g x)
⊢ ∑ _x ∈ Finset.range (n + 1), 1 = HAdd.hAdd (α := ℝ) (↑n : ℝ) 1

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

Premises used: mul_assoc, Nat.cast, HAdd.hAdd, OfNat.ofNat