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)
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)) ≤
    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 *
        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) *
    (↑(n.choose i) : ℝ) ≤
  HMul.hMul (β := ℝ) (C * HPow.hPow (α := ℝ) 2 (l + k))
      (((Finset.Iic (l + k, n)).sup (schwartzSeminormFamily 𝕜 D E) : (a : 𝓢(D, E)) → ℝ) f : ℝ) *
    (↑(n.choose (n / 2)) : ℝ)
Tactic: move_mul [(Nat.choose n i : ℝ), (Nat.choose n (n / 2) : ℝ)]
-- 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 *
          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) *
      (↑(n.choose i) : ℝ) ≤
    HMul.hMul (β := ℝ) (C * HPow.hPow (α := ℝ) 2 (l + k))
        (((Finset.Iic (l + k, n)).sup (schwartzSeminormFamily 𝕜 D E) : (a : 𝓢(D, E)) → ℝ) f : ℝ) *
      (↑(n.choose (n / 2)) : ℝ)
have right : ‖x‖ ^ k *
      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 (β := ℝ) (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)
this : ∑ _x ∈ Finset.range (n + 1), 1 = HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
i : ℕ
hi : i ∈ Finset.range (n + 1)
right :
  ‖x‖ ^ k *
        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 (β := ℝ) (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_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) *
      (↑(n.choose i) : ℝ) ≤
    HMul.hMul (β := ℝ) (C * HPow.hPow (α := ℝ) 2 (l + k))
        (((Finset.Iic (l + k, n)).sup (schwartzSeminormFamily 𝕜 D E) : (a : 𝓢(D, E)) → ℝ) f : ℝ) *
      (↑(n.choose (n / 2)) : ℝ)
have right₁ : LE.le (α := ℝ) (↑(n.choose i) : ℝ) (↑(n.choose (n / 2)) : ℝ)
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)
this : ∑ _x ∈ Finset.range (n + 1), 1 = HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
i : ℕ
hi : i ∈ Finset.range (n + 1)
⊢ LE.le (α := ℝ) (↑(n.choose i) : ℝ) (↑(n.choose (n / 2)) : ℝ)
have right : n.choose i ≤ n.choose (n / 2)
Tactic: norm_cast
-- 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)
this : ∑ _x ∈ Finset.range (n + 1), 1 = HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
i : ℕ
hi : i ∈ Finset.range (n + 1)
⊢ ‖x‖ ^ k *
        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 (β := ℝ) (C * HPow.hPow (α := ℝ) 2 (l + k))
      (((Finset.Iic (l + k, n)).sup (schwartzSeminormFamily 𝕜 D E) : (a : 𝓢(D, E)) → ℝ) f : ℝ)
have hgrowth₁ : norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_6} ℝ (fun (i : Fin (n - i)) ↦ D) F) (iteratedFDeriv ℝ (n - i) g x) ≤
  C * (1 + ‖x‖) ^ l
Tactic: specialize hgrowth (n - i) (by simp only [tsub_le_self]) x
Cleared hypotheses: 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
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)
hgrowth :
  norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_6} ℝ (fun (i : Fin (n - i)) ↦ D) F) (iteratedFDeriv ℝ (n - i) g x) ≤
    C * (1 + ‖x‖) ^ l
⊢ ‖x‖ ^ k *
        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 (β := ℝ) (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_5} ℝ (fun (i : Fin i) ↦ D) E)
        (iteratedFDeriv ℝ i (⇑f : (a : D) → E) x) *
    (C * (1 + ‖x‖) ^ l) ≤
  HMul.hMul (β := ℝ) (C * HPow.hPow (α := ℝ) 2 (l + k))
    (((Finset.Iic (l + k, n)).sup (schwartzSeminormFamily 𝕜 D E) : (a : 𝓢(D, E)) → ℝ) f : ℝ)
Tactic: grw [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
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)
hgrowth :
  norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_6} ℝ (fun (i : Fin (n - i)) ↦ D) F) (iteratedFDeriv ℝ (n - i) g x) ≤
    C * (1 + ‖x‖) ^ l
⊢ ‖x‖ ^ k *
        norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_5} ℝ (fun (i : Fin i) ↦ D) E)
          (iteratedFDeriv ℝ i (⇑f : (a : D) → E) x) *
      (C * (1 + ‖x‖) ^ l) ≤
    HMul.hMul (β := ℝ) (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_5} ℝ (fun (i : Fin i) ↦ D) E)
          (iteratedFDeriv ℝ i (⇑f : (a : D) → E) x) *
      (1 + ‖x‖) ^ l *
    C ≤
  HMul.hMul (β := ℝ) (HPow.hPow (α := ℝ) 2 (l + k))
      (((Finset.Iic (l + k, n)).sup (schwartzSeminormFamily 𝕜 D E) : (a : 𝓢(D, E)) → ℝ) f : ℝ) *
    C
Tactic: move_mul [C]
-- 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
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)
hgrowth :
  norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_6} ℝ (fun (i : Fin (n - i)) ↦ D) F) (iteratedFDeriv ℝ (n - i) g x) ≤
    C * (1 + ‖x‖) ^ l
⊢ ‖x‖ ^ k *
          norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_5} ℝ (fun (i : Fin i) ↦ D) E)
            (iteratedFDeriv ℝ i (⇑f : (a : D) → E) x) *
        (1 + ‖x‖) ^ l *
      C ≤
    HMul.hMul (β := ℝ) (HPow.hPow (α := ℝ) 2 (l + k))
        (((Finset.Iic (l + k, n)).sup (schwartzSeminormFamily 𝕜 D E) : (a : 𝓢(D, E)) → ℝ) f : ℝ) *
      C
have right : ‖x‖ ^ k *
      norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_5} ℝ (fun (i : Fin i) ↦ D) E)
        (iteratedFDeriv ℝ i (⇑f : (a : D) → E) x) *
    (1 + ‖x‖) ^ l ≤
  HMul.hMul (β := ℝ) (HPow.hPow (α := ℝ) 2 (l + k))
    (((Finset.Iic (l + k, n)).sup (schwartzSeminormFamily 𝕜 D E) : (a : 𝓢(D, E)) → ℝ) f : ℝ)
Tactic: gcongr ?_ * C
-- 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
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)
hgrowth :
  norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_6} ℝ (fun (i : Fin (n - i)) ↦ D) F) (iteratedFDeriv ℝ (n - i) g x) ≤
    C * (1 + ‖x‖) ^ l
⊢ ‖x‖ ^ k *
        norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_5} ℝ (fun (i : Fin i) ↦ D) E)
          (iteratedFDeriv ℝ i (⇑f : (a : D) → E) x) *
      (1 + ‖x‖) ^ l ≤
    HMul.hMul (β := ℝ) (HPow.hPow (α := ℝ) 2 (l + k))
      (((Finset.Iic (l + k, n)).sup (schwartzSeminormFamily 𝕜 D E) : (a : 𝓢(D, E)) → ℝ) f : ℝ)
have hi₁ : i ≤ n
Tactic: rw [Finset.mem_range_succ_iff] at hi
Cleared hypotheses: hi, hgrowth
-- 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
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 ≤ n
hgrowth :
  norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_6} ℝ (fun (i : Fin (n - i)) ↦ D) F) (iteratedFDeriv ℝ (n - i) g x) ≤
    C * (1 + ‖x‖) ^ l
⊢ ‖x‖ ^ k *
        norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_5} ℝ (fun (i : Fin i) ↦ D) E)
          (iteratedFDeriv ℝ i (⇑f : (a : D) → E) x) *
      (1 + ‖x‖) ^ l ≤
    HMul.hMul (β := ℝ) (HPow.hPow (α := ℝ) 2 (l + k))
      (((Finset.Iic (l + k, n)).sup (schwartzSeminormFamily 𝕜 D E) : (a : 𝓢(D, E)) → ℝ) f : ℝ)
have hi₁ : i ≤ (l + k, n).2
Tactic: change i ≤ (l + k, n).snd at hi
Cleared hypotheses: hi