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 : 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.{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))
have 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)
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 : 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 *
      (‖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 : ℝ)
have 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‖
Tactic: move_mul [‖m‖]
-- 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 : 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) *
      ‖m‖ ≤
    HMul.hMul (α := ℝ) ((SchwartzMap.seminorm 𝕜 k n : (a : 𝓢(E, F →L[ℝ] G)) → ℝ) f : ℝ) ‖m‖
have 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
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 : 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.{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 : ℝ)
have 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))
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
-- 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 : 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))
⊢ ‖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 : ℝ)
have 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 : ℝ)
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
-- 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 : ℕ
⊢ ∃ (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 : ℝ)
have 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 : ℝ)
Tactic: rcases hg.norm_iteratedFDeriv_le_uniform n with ⟨l, C, hC, hgrowth⟩
-- 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
⊢ ∃ (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 : ℝ)
have 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 : ℝ)
Tactic: use
    Finset.Iic (l + k, n), ‖B‖ * ((n : ℝ) + (1 : ℝ)) * n.choose (n / 2) * (C * 2 ^ (l + k)),
    by positivity
-- 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
⊢ ‖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 : ℝ)
have hxk : 0 ≤ ‖x‖ ^ k
Tactic: have hxk : 0 ≤ ‖x‖ ^ k := by positivity
-- 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
⊢ ‖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 : ℝ)
have 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 : ℝ)
Tactic: simp_rw [← ContinuousLinearMap.bilinearRestrictScalars_apply_apply ℝ B]
-- 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
⊢ ‖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 : ℝ)
have 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)
Tactic: have hnorm_mul :=
    ContinuousLinearMap.norm_iteratedFDeriv_le_of_bilinear (B.bilinearRestrictScalars ℝ)
    (f.smooth ⊤) hg.1 x (n := n) (mod_cast le_top)
-- 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 *
      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 : ℝ)
have 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 : ℝ)
Tactic: grw [hnorm_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)
⊢ ‖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 : ℝ)
have 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 : ℝ)
Tactic: rw [ContinuousLinearMap.norm_bilinearRestrictScalars]