awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Basic (goal)
Goal:
E : Type u_5
F : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
𝕜' : Type u_10
inst_4 : RCLike 𝕜'
inst_5 : NormedSpace 𝕜' F
g : E → 𝕜'
hg : Function.HasTemperateGrowth g
c : ℝ
rw :
  smulLeftCLM F (HSMul.hSMul (α := 𝕜') (↑c : 𝕜') g) =
    HSMul.hSMul (β := 𝓢(E, F) →L[𝕜'] 𝓢(E, F)) c (smulLeftCLM F g : 𝓢(E, F) →L[𝕜'] 𝓢(E, F))
rw₁ :
  HSMul.hSMul (α := 𝕜') (β := 𝓢(E, F) →L[𝕜'] 𝓢(E, F)) (↑c : 𝕜') (smulLeftCLM F g : 𝓢(E, F) →L[𝕜'] 𝓢(E, F)) =
    HSMul.hSMul (β := 𝓢(E, F) →L[𝕜'] 𝓢(E, F)) c (smulLeftCLM F g : 𝓢(E, F) →L[𝕜'] 𝓢(E, F))
⊢ smulLeftCLM F (c • g) = HSMul.hSMul (β := 𝓢(E, F) →L[𝕜'] 𝓢(E, F)) c (smulLeftCLM F g : 𝓢(E, F) →L[𝕜'] 𝓢(E, F))
have rw₂ : HSMul.hSMul (β := 𝓢(E, F) →L[𝕜'] 𝓢(E, F)) c (smulLeftCLM F g : 𝓢(E, F) →L[𝕜'] 𝓢(E, F)) =
  HSMul.hSMul (β := 𝓢(E, F) →L[𝕜'] 𝓢(E, F)) c (smulLeftCLM F g : 𝓢(E, F) →L[𝕜'] 𝓢(E, F))
Tactic: rw [RCLike.real_smul_eq_coe_smul (K := 𝕜') c, smulLeftCLM_smul hg,
    ← RCLike.real_smul_eq_coe_smul c]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Basic (goal)
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 : NontriviallyNormedField 𝕜
inst_5 : NormedAlgebra ℝ 𝕜
inst_6 : NormedSpace 𝕜 F
g : E → 𝕜
f : 𝓢(E, F)
⊢ tsupport.{u_5, u_6} (α := F)
      (⇑(((smulLeftCLM F g : 𝓢(E, F) →L[𝕜] 𝓢(E, F)) : (a : 𝓢(E, F)) → 𝓢(E, F)) f : 𝓢(E, F)) : (a : E) → F) ⊆
    tsupport.{u_5, u_6} (α := F) (⇑f : (a : E) → F) ∩ tsupport g
have pos : ∀ (hg : Function.HasTemperateGrowth g),
  tsupport.{u_5, u_6} (α := F)
      (⇑(((smulLeftCLM F g : 𝓢(E, F) →L[𝕜] 𝓢(E, F)) : (a : 𝓢(E, F)) → 𝓢(E, F)) f : 𝓢(E, F)) : (a : E) → F) ⊆
    tsupport.{u_5, u_6} (α := F) (⇑f : (a : E) → F) ∩ tsupport g
Tactic: by_cases hg : g.HasTemperateGrowth
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Basic (goal)
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 : NontriviallyNormedField 𝕜
inst_5 : NormedAlgebra ℝ 𝕜
inst_6 : NormedSpace 𝕜 F
g : E → 𝕜
f : 𝓢(E, F)
pos :
  ∀ (hg : Function.HasTemperateGrowth g),
    tsupport.{u_5, u_6} (α := F)
        (⇑(((smulLeftCLM F g : 𝓢(E, F) →L[𝕜] 𝓢(E, F)) : (a : 𝓢(E, F)) → 𝓢(E, F)) f : 𝓢(E, F)) : (a : E) → F) ⊆
      tsupport.{u_5, u_6} (α := F) (⇑f : (a : E) → F) ∩ tsupport g
⊢ tsupport.{u_5, u_6} (α := F)
      (⇑(((smulLeftCLM F g : 𝓢(E, F) →L[𝕜] 𝓢(E, F)) : (a : 𝓢(E, F)) → 𝓢(E, F)) f : 𝓢(E, F)) : (a : E) → F) ⊆
    tsupport.{u_5, u_6} (α := F) (⇑f : (a : E) → F) ∩ tsupport g
have neg : ∀ (hg : ¬Function.HasTemperateGrowth g),
  tsupport.{u_5, u_6} (α := F)
      (⇑(((smulLeftCLM F g : 𝓢(E, F) →L[𝕜] 𝓢(E, F)) : (a : 𝓢(E, F)) → 𝓢(E, F)) f : 𝓢(E, F)) : (a : E) → F) ⊆
    tsupport.{u_5, u_6} (α := F) (⇑f : (a : E) → F) ∩ tsupport g
Tactic: by_cases hg : g.HasTemperateGrowth
-- 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
x x_1 : 𝓢(D, E)
⊢ bilinLeftCLM B.flip ⋯ =
    HAdd.hAdd (α := 𝓢(D, F) →L[𝕜] 𝓢(D, G)) (β := 𝓢(D, F) →L[𝕜] 𝓢(D, G)) (bilinLeftCLM B.flip ⋯ : 𝓢(D, F) →L[𝕜] 𝓢(D, G))
      (bilinLeftCLM B.flip ⋯ : 𝓢(D, F) →L[𝕜] 𝓢(D, G))
have h : ∀ (x_2 : 𝓢(D, F)) (x_3 : D),
  Eq.{u_7 + 1} (α := G)
    (((((bilinLeftCLM B.flip sorry : 𝓢(D, F) →L[𝕜] 𝓢(D, G)) : (a : 𝓢(D, F)) → 𝓢(D, G)) x_2 : 𝓢(D, G)) : (a : D) → G) x_3 :
      G)
    ((((HAdd.hAdd (α := 𝓢(D, F) →L[𝕜] 𝓢(D, G)) (β := 𝓢(D, F) →L[𝕜] 𝓢(D, G))
                  (bilinLeftCLM B.flip sorry : 𝓢(D, F) →L[𝕜] 𝓢(D, G)) (bilinLeftCLM B.flip sorry : 𝓢(D, F) →L[𝕜] 𝓢(D, G)) :
                (a : 𝓢(D, F)) → 𝓢(D, G))
              x_2 :
            𝓢(D, G)) :
          (a : D) → G)
        x_3 :
      G)
Tactic: ext
-- 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
x : 𝕜
x_1 : 𝓢(D, E)
⊢ bilinLeftCLM B.flip ⋯ =
    HSMul.hSMul (α := 𝕜) (β := 𝓢(D, F) →L[𝕜] 𝓢(D, G)) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) x : 𝕜)
      (bilinLeftCLM B.flip ⋯ : 𝓢(D, F) →L[𝕜] 𝓢(D, G))
have h : ∀ (x_2 : 𝓢(D, F)) (x_3 : D),
  Eq.{u_7 + 1} (α := G)
    (((((bilinLeftCLM B.flip sorry : 𝓢(D, F) →L[𝕜] 𝓢(D, G)) : (a : 𝓢(D, F)) → 𝓢(D, G)) x_2 : 𝓢(D, G)) : (a : D) → G) x_3 :
      G)
    ((((HSMul.hSMul (α := 𝕜) (β := 𝓢(D, F) →L[𝕜] 𝓢(D, G)) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) x : 𝕜)
                  (bilinLeftCLM B.flip sorry : 𝓢(D, F) →L[𝕜] 𝓢(D, G)) :
                (a : 𝓢(D, F)) → 𝓢(D, G))
              x_2 :
            𝓢(D, G)) :
          (a : D) → G)
        x_3 :
      G)
Tactic: ext
-- 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
L : ContinuousLinearMap.{0, 0, u_5, u_7} (RingHom.id ℝ) E (G →L[ℝ] ℝ)
f g : 𝓢(E, F)
x : E
⊢ (fun (f : 𝓢(E, F)) (x : E) ↦ (smulRight (S := ℝ) ((L : (a : E) → G →L[ℝ] ℝ) x) ((f : (a : E) → F) x) : G →L[ℝ] F))
      (f + g) x =
    HAdd.hAdd (α := G →L[ℝ] F)
      ((fun (f : 𝓢(E, F)) (x : E) ↦
          (smulRight (S := ℝ) ((L : (a : E) → G →L[ℝ] ℝ) x) ((f : (a : E) → F) x) : G →L[ℝ] F))
        f x)
      ((fun (f : 𝓢(E, F)) (x : E) ↦
          (smulRight (S := ℝ) ((L : (a : E) → G →L[ℝ] ℝ) x) ((f : (a : E) → F) x) : G →L[ℝ] F))
        g x)
have h : ∀ (x_1 : G),
  Eq.{u_6 + 1} (α := F)
    (((fun (f : 𝓢(E, F)) (x : E) ↦ (smulRight (S := ℝ) ((L : (a : E) → G →L[ℝ] ℝ) x) ((f : (a : E) → F) x) : G →L[ℝ] F))
            (f + g) x :
          (a : G) → F)
        x_1 :
      F)
    ((HAdd.hAdd (α := G →L[ℝ] F)
            ((fun (f : 𝓢(E, F)) (x : E) ↦
                (smulRight (S := ℝ) ((L : (a : E) → G →L[ℝ] ℝ) x) ((f : (a : E) → F) x) : G →L[ℝ] F))
              f x)
            ((fun (f : 𝓢(E, F)) (x : E) ↦
                (smulRight (S := ℝ) ((L : (a : E) → G →L[ℝ] ℝ) x) ((f : (a : E) → F) x) : G →L[ℝ] F))
              g x) :
          (a : G) → F)
        x_1 :
      F)
Tactic: ext
-- 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
L : ContinuousLinearMap.{0, 0, u_5, u_7} (RingHom.id ℝ) E (G →L[ℝ] ℝ)
k n : ℕ
⊢ ∃ (s : Finset (ℕ × ℕ)) (C : ℝ),
    0 ≤ C ∧
      ∀ (f : 𝓢(E, F)) (x : E),
        ‖x‖ ^ (k, n).1 *
            norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin (k, n).2) ↦ E) (G →L[ℝ] F))
              (iteratedFDeriv ℝ (k, n).2
                ((fun (f : 𝓢(E, F)) (x : E) ↦
                    (smulRight (S := ℝ) ((L : (a : E) → G →L[ℝ] ℝ) x) ((f : (a : E) → F) x) : G →L[ℝ] F))
                  f)
                x) ≤
          HMul.hMul (β := ℝ) C ((s.sup (schwartzSeminormFamily 𝕜 E F) : (a : 𝓢(E, F)) → ℝ) f : ℝ)
have right : ∀ (f : 𝓢(E, F)) (x : E),
  ‖x‖ ^ (k, n).1 *
      norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin (k, n).2) ↦ E) (G →L[ℝ] F))
        (iteratedFDeriv ℝ (k, n).2
          ((fun (f : 𝓢(E, F)) (x : E) ↦
              (smulRight (S := ℝ) ((L : (a : E) → G →L[ℝ] ℝ) x) ((f : (a : E) → F) x) : G →L[ℝ] F))
            f)
          x) ≤
    HMul.hMul (β := ℝ) (2 * ‖L‖ * (↑(max 1 n) : ℝ))
      ((Finset.sup {(k + 1, n), (k, n - 1)} (schwartzSeminormFamily 𝕜 E F) : (a : 𝓢(E, F)) → ℝ) f : ℝ)
Tactic: use {(k + 1, n), (k, n - 1)}, 2 * ‖L‖ * (max 1 n), 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
L : ContinuousLinearMap.{0, 0, u_5, u_7} (RingHom.id ℝ) E (G →L[ℝ] ℝ)
k n : ℕ
f : 𝓢(E, F)
x : E
⊢ ‖x‖ ^ (k, n).1 *
      norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin (k, n).2) ↦ E) (G →L[ℝ] F))
        (iteratedFDeriv ℝ (k, n).2
          ((fun (f : 𝓢(E, F)) (x : E) ↦
              (smulRight (S := ℝ) ((L : (a : E) → G →L[ℝ] ℝ) x) ((f : (a : E) → F) x) : G →L[ℝ] F))
            f)
          x) ≤
    ‖x‖ ^ k *
      ∑ i ∈ Finset.range (n + 1),
        (↑(n.choose i) : ℝ) *
            norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_7} ℝ (fun (i : Fin i) ↦ E) (G →L[ℝ] ℝ))
              (iteratedFDeriv ℝ i (⇑L : (a : E) → G →L[ℝ] ℝ) x) *
          norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin (n - i)) ↦ E) F)
            (iteratedFDeriv ℝ (n - i) (⇑f : (a : E) → F) x)
have hbc : norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin (k, n).2) ↦ E) (G →L[ℝ] F))
    (iteratedFDeriv ℝ (k, n).2
      ((fun (f : 𝓢(E, F)) (x : E) ↦
          (smulRight (S := ℝ) ((L : (a : E) → G →L[ℝ] ℝ) x) ((f : (a : E) → F) x) : G →L[ℝ] F))
        f)
      x) ≤
  ∑ i ∈ Finset.range (n + 1),
    (↑(n.choose i) : ℝ) *
        norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_7} ℝ (fun (i : Fin i) ↦ E) (G →L[ℝ] ℝ))
          (iteratedFDeriv ℝ i (⇑L : (a : E) → G →L[ℝ] ℝ) x) *
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin (n - i)) ↦ E) F)
        (iteratedFDeriv ℝ (n - i) (⇑f : (a : E) → F) x)
Tactic: gcongr 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
L : ContinuousLinearMap.{0, 0, u_5, u_7} (RingHom.id ℝ) E (G →L[ℝ] ℝ)
k n : ℕ
f : 𝓢(E, F)
x : E
⊢ ‖x‖ ^ k *
      ∑ i ∈ Finset.range (n + 1),
        (↑(n.choose i) : ℝ) *
            norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_7} ℝ (fun (i : Fin i) ↦ E) (G →L[ℝ] ℝ))
              (iteratedFDeriv ℝ i (⇑L : (a : E) → G →L[ℝ] ℝ) x) *
          norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin (n - i)) ↦ E) F)
            (iteratedFDeriv ℝ (n - i) (⇑f : (a : E) → F) x) ≤
    ‖x‖ ^ k *
      (norm.{u_7} (E := G →L[ℝ] ℝ) ((L : (a : E) → G →L[ℝ] ℝ) x : G →L[ℝ] ℝ) *
          norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
            (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x) +
        (↑n : ℝ) * ‖L‖ *
          norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin (n - 1)) ↦ E) F)
            (iteratedFDeriv ℝ (n - 1) (⇑f : (a : E) → F) x))
have hbc : ∑ i ∈ Finset.range (n + 1),
    (↑(n.choose i) : ℝ) *
        norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_7} ℝ (fun (i : Fin i) ↦ E) (G →L[ℝ] ℝ))
          (iteratedFDeriv ℝ i (⇑L : (a : E) → G →L[ℝ] ℝ) x) *
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin (n - i)) ↦ E) F)
        (iteratedFDeriv ℝ (n - i) (⇑f : (a : E) → F) x) ≤
  norm.{u_7} (E := G →L[ℝ] ℝ) ((L : (a : E) → G →L[ℝ] ℝ) x : G →L[ℝ] ℝ) *
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
        (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x) +
    (↑n : ℝ) * ‖L‖ *
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin (n - 1)) ↦ E) F)
        (iteratedFDeriv ℝ (n - 1) (⇑f : (a : E) → F) x)
Tactic: gcongr 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
L : ContinuousLinearMap.{0, 0, u_5, u_7} (RingHom.id ℝ) E (G →L[ℝ] ℝ)
k n : ℕ
f : 𝓢(E, F)
x : E
⊢ ∑ i ∈ Finset.range (n + 1),
      (↑(n.choose i) : ℝ) *
          norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_7} ℝ (fun (i : Fin i) ↦ E) (G →L[ℝ] ℝ))
            (iteratedFDeriv ℝ i (⇑L : (a : E) → G →L[ℝ] ℝ) x) *
        norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin (n - i)) ↦ E) F)
          (iteratedFDeriv ℝ (n - i) (⇑f : (a : E) → F) x) ≤
    norm.{u_7} (E := G →L[ℝ] ℝ) ((L : (a : E) → G →L[ℝ] ℝ) x : G →L[ℝ] ℝ) *
        norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
          (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x) +
      (↑n : ℝ) * ‖L‖ *
        norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin (n - 1)) ↦ E) F)
          (iteratedFDeriv ℝ (n - 1) (⇑f : (a : E) → F) x)
have hbc : (↑(n.choose 0) : ℝ) *
        norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_7} ℝ (fun (i : Fin 0) ↦ E) (G →L[ℝ] ℝ))
          (iteratedFDeriv ℝ 0 (⇑L : (a : E) → G →L[ℝ] ℝ) x) *
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin (n - 0)) ↦ E) F)
        (iteratedFDeriv ℝ (n - 0) (⇑f : (a : E) → F) x) +
    ∑ k ∈ Finset.range n,
      (↑(n.choose (k + 1)) : ℝ) *
          norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_7} ℝ (fun (i : Fin (k + 1)) ↦ E) (G →L[ℝ] ℝ))
            (iteratedFDeriv ℝ (k + 1) (⇑L : (a : E) → G →L[ℝ] ℝ) x) *
        norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin (n - (k + 1))) ↦ E) F)
          (iteratedFDeriv ℝ (n - (k + 1)) (⇑f : (a : E) → F) x) ≤
  norm.{u_7} (E := G →L[ℝ] ℝ) ((L : (a : E) → G →L[ℝ] ℝ) x : G →L[ℝ] ℝ) *
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
        (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x) +
    (↑n : ℝ) * ‖L‖ *
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin (n - 1)) ↦ E) F)
        (iteratedFDeriv ℝ (n - 1) (⇑f : (a : E) → F) x)
Tactic: rw [Finset.sum_range_succ', add_comm]
-- 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
L : ContinuousLinearMap.{0, 0, u_5, u_7} (RingHom.id ℝ) E (G →L[ℝ] ℝ)
k : ℕ
f : 𝓢(E, F)
x : E
n : ℕ
⊢ Eq (α := ℝ)
    (∑ k ∈ Finset.range n,
      (↑((n + 1).choose (k + 1 + 1)) : ℝ) *
          norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_7} ℝ (fun (i : Fin (k + 1 + 1)) ↦ E) (G →L[ℝ] ℝ))
            (iteratedFDeriv ℝ (k + 1 + 1) (⇑L : (a : E) → G →L[ℝ] ℝ) x) *
        norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin (n + 1 - (k + 1 + 1))) ↦ E) F)
          (iteratedFDeriv ℝ (n + 1 - (k + 1 + 1)) (⇑f : (a : E) → F) x))
    0
have h : ∀ x_1 ∈ Finset.range n,
  (↑((n + 1).choose (x_1 + 1 + 1)) : ℝ) *
        norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_7} ℝ (fun (i : Fin (x_1 + 1 + 1)) ↦ E) (G →L[ℝ] ℝ))
          (iteratedFDeriv ℝ (x_1 + 1 + 1) (⇑L : (a : E) → G →L[ℝ] ℝ) x) *
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin (n + 1 - (x_1 + 1 + 1))) ↦ E) F)
        (iteratedFDeriv ℝ (n + 1 - (x_1 + 1 + 1)) (⇑f : (a : E) → F) x) =
    0
Tactic: apply Finset.sum_eq_zero
-- 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
L : ContinuousLinearMap.{0, 0, u_5, u_7} (RingHom.id ℝ) E (G →L[ℝ] ℝ)
k : ℕ
f : 𝓢(E, F)
x : E
n : ℕ
⊢ (↑((n + 1).choose 0) : ℝ) *
          norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_7} ℝ (fun (i : Fin 0) ↦ E) (G →L[ℝ] ℝ))
            (iteratedFDeriv ℝ 0 (⇑L : (a : E) → G →L[ℝ] ℝ) x) *
        norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin (n + 1 - 0)) ↦ E) F)
          (iteratedFDeriv ℝ (n + 1 - 0) (⇑f : (a : E) → F) x) +
      ∑ k ∈ Finset.range (n + 1),
        (↑((n + 1).choose (k + 1)) : ℝ) *
            norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_7} ℝ (fun (i : Fin (k + 1)) ↦ E) (G →L[ℝ] ℝ))
              (iteratedFDeriv ℝ (k + 1) (⇑L : (a : E) → G →L[ℝ] ℝ) x) *
          norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin (n + 1 - (k + 1))) ↦ E) F)
            (iteratedFDeriv ℝ (n + 1 - (k + 1)) (⇑f : (a : E) → F) x) ≤
    norm.{u_7} (E := G →L[ℝ] ℝ) ((L : (a : E) → G →L[ℝ] ℝ) x : G →L[ℝ] ℝ) *
        norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin (n + 1)) ↦ E) F)
          (iteratedFDeriv ℝ (n + 1) (⇑f : (a : E) → F) x) +
      (↑(n + 1) : ℝ) * ‖L‖ *
        norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin (n + 1 - 1)) ↦ E) F)
          (iteratedFDeriv ℝ (n + 1 - 1) (⇑f : (a : E) → F) x)
have this : Eq (α := ℝ)
  (∑ k ∈ Finset.range n,
    (↑((n + 1).choose (k + 1 + 1)) : ℝ) *
        norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_7} ℝ (fun (i : Fin (k + 1 + 1)) ↦ E) (G →L[ℝ] ℝ))
          (iteratedFDeriv ℝ (k + 1 + 1) (⇑L : (a : E) → G →L[ℝ] ℝ) x) *
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin (n + 1 - (k + 1 + 1))) ↦ E) F)
        (iteratedFDeriv ℝ (n + 1 - (k + 1 + 1)) (⇑f : (a : E) → F) x))
  0
Tactic: have : ∑ k ∈ Finset.range n,
                (((n + 1).choose (k + 1 + 1)) : ℝ) * ‖iteratedFDeriv ℝ (k + 1 + 1) L x‖ *
                ‖iteratedFDeriv ℝ (n + 1 - (k + 1 + 1)) f x‖ = 0 := by
              apply Finset.sum_eq_zero
              simp [iteratedFDeriv_succ_eq_comp_right, iteratedFDeriv_succ_const]
-- 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
L : ContinuousLinearMap.{0, 0, u_5, u_7} (RingHom.id ℝ) E (G →L[ℝ] ℝ)
k n : ℕ
f : 𝓢(E, F)
x : E
⊢ ‖x‖ ^ k * norm.{u_7} (E := G →L[ℝ] ℝ) ((L : (a : E) → G →L[ℝ] ℝ) x : G →L[ℝ] ℝ) *
        norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
          (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x) +
      ‖x‖ ^ k * (↑n : ℝ) * ‖L‖ *
        norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin (n - 1)) ↦ E) F)
          (iteratedFDeriv ℝ (n - 1) (⇑f : (a : E) → F) x) ≤
    HMul.hMul (β := ℝ) (‖L‖ * 1) ((SchwartzMap.seminorm 𝕜 (k + 1) n : (a : 𝓢(E, F)) → ℝ) f : ℝ) +
      HMul.hMul (β := ℝ) (‖L‖ * (↑n : ℝ)) ((SchwartzMap.seminorm 𝕜 k (n - 1) : (a : 𝓢(E, F)) → ℝ) f : ℝ)
have grw : ‖x‖ ^ k * (‖L‖ * ‖x‖) *
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
        (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x) +
    ‖x‖ ^ k * (↑n : ℝ) * ‖L‖ *
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin (n - 1)) ↦ E) F)
        (iteratedFDeriv ℝ (n - 1) (⇑f : (a : E) → F) x) ≤
  ‖L‖ * 1 *
      (‖x‖ ^ (k + 1) *
        norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
          (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x)) +
    ‖L‖ * (↑n : ℝ) *
      (‖x‖ ^ k *
        norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin (n - 1)) ↦ E) F)
          (iteratedFDeriv ℝ (n - 1) (⇑f : (a : E) → F) x))
Tactic: grw [le_opNorm, ← le_seminorm 𝕜 (k + 1) n f x, ← le_seminorm 𝕜 k (n - 1) f x]
-- 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
L : ContinuousLinearMap.{0, 0, u_5, u_7} (RingHom.id ℝ) E (G →L[ℝ] ℝ)
k n : ℕ
f : 𝓢(E, F)
x : E
⊢ ‖x‖ ^ k * (‖L‖ * ‖x‖) *
        norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
          (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x) +
      ‖x‖ ^ k * (↑n : ℝ) * ‖L‖ *
        norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin (n - 1)) ↦ E) F)
          (iteratedFDeriv ℝ (n - 1) (⇑f : (a : E) → F) x) ≤
    ‖L‖ * 1 *
        (‖x‖ ^ (k + 1) *
          norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
            (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x)) +
      ‖L‖ * (↑n : ℝ) *
        (‖x‖ ^ k *
          norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin (n - 1)) ↦ E) F)
            (iteratedFDeriv ℝ (n - 1) (⇑f : (a : E) → F) x))
have hab : ‖x‖ ^ k * (‖L‖ * ‖x‖) *
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
        (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x) +
    ‖x‖ ^ k * (↑n : ℝ) * ‖L‖ *
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin (n - 1)) ↦ E) F)
        (iteratedFDeriv ℝ (n - 1) (⇑f : (a : E) → F) x) =
  ‖L‖ * 1 *
      (‖x‖ ^ (k + 1) *
        norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
          (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x)) +
    ‖L‖ * (↑n : ℝ) *
      (‖x‖ ^ k *
        norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin (n - 1)) ↦ E) F)
          (iteratedFDeriv ℝ (n - 1) (⇑f : (a : E) → F) x))
Tactic: apply le_of_eq