awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Basic (goal)
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‖ ^ 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 : ℝ)
have 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‖
Tactic: move_mul [‖B‖, ‖B‖]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Basic (goal)
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‖ ^ 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‖
have 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 : ℝ)
Tactic: gcongr ?_ * _
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Basic (goal)
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‖ ^ 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 : ℝ)
have 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 : ℝ)
Tactic: rw [Finset.mul_sum]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Basic (hypothesis)
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)
⊢ ∑ 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 : ℝ)
have this : ∑ _x ∈ Finset.range (n + 1), 1 = HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
Tactic: have : (∑ _x ∈ Finset.range (n + 1), (1 : ℝ)) = n + 1 := by simp
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Basic (goal)
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
⊢ ∑ 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 : ℝ)
have 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 : ℝ)
Tactic: simp_rw [mul_assoc ((n : ℝ) + 1)]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Basic (goal)
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
⊢ ∑ 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 : ℝ)
have right : LE.le (α := ℝ)
  (∑ 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)))
  (∑ i ∈ Finset.range (n + 1),
    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 : ℝ))
Tactic: rw [← this, Finset.sum_mul]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Basic (goal)
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
⊢ LE.le (α := ℝ)
    (∑ 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)))
    (∑ i ∈ Finset.range (n + 1),
      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 : ℝ))
have right : ∀ (i : ℕ) (hi : 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)) ≤
    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 : ℝ)
Tactic: refine Finset.sum_le_sum fun i hi => ?_
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Basic (goal)
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
i : ℕ
hi : 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)) ≤
    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 : ℝ)
have right : ‖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 (β := ℝ) ((↑(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 only [one_mul]