awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Basic (goal)
Goal:
𝕜 : Type u_2
F : Type u_6
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : NormedField 𝕜
inst_3 : NormedSpace 𝕜 F
inst_4 : SMulCommClass ℝ 𝕜 F
k n : ℕ
f : 𝓢(ℝ, F)
M : ℝ
hMp : 0 ≤ M
hM : ∀ (x : ℝ), |x| ^ k * norm (E := F) (iteratedDeriv n (⇑f : (a : ℝ) → F) x) ≤ M
⊢ (SchwartzMap.seminorm 𝕜 k n : (a : 𝓢(ℝ, F)) → ℝ) f ≤ M
have refine : ∀ (x : ℝ),
  ‖x‖ ^ k * norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ ℝ) F) (iteratedFDeriv ℝ n (⇑f : (a : ℝ) → F) x) ≤ M
Tactic: refine seminorm_le_bound 𝕜 k n f hMp ?_
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Basic (hypothesis)
Goal:
𝕜 : Type u_2
F : Type u_6
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : NormedField 𝕜
inst_3 : NormedSpace 𝕜 F
inst_4 : SMulCommClass ℝ 𝕜 F
k n : ℕ
f : 𝓢(ℝ, F)
x : ℝ
⊢ |x| ^ k * norm (E := F) (iteratedDeriv n (⇑f : (a : ℝ) → F) x) ≤ (SchwartzMap.seminorm 𝕜 k n : (a : 𝓢(ℝ, F)) → ℝ) f
have this : ‖x‖ ^ k * norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ ℝ) F) (iteratedFDeriv ℝ n (⇑f : (a : ℝ) → F) x) ≤
  (SchwartzMap.seminorm 𝕜 k n : (a : 𝓢(ℝ, F)) → ℝ) f
Tactic: have := le_seminorm 𝕜 k n f x
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Basic (goal)
Goal:
𝕜 : Type u_2
F : Type u_6
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
inst_2 : NormedField 𝕜
inst_3 : NormedSpace 𝕜 F
inst_4 : SMulCommClass ℝ 𝕜 F
k n : ℕ
f : 𝓢(ℝ, F)
x : ℝ
this :
  ‖x‖ ^ k * norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin n) ↦ ℝ) F) (iteratedFDeriv ℝ n (⇑f : (a : ℝ) → F) x) ≤
    (SchwartzMap.seminorm 𝕜 k n : (a : 𝓢(ℝ, F)) → ℝ) f
⊢ |x| ^ k * norm (E := F) (iteratedDeriv n (⇑f : (a : ℝ) → F) x) ≤ (SchwartzMap.seminorm 𝕜 k n : (a : 𝓢(ℝ, F)) → ℝ) f
have rwa : ‖x‖ ^ k * norm (E := F) (iteratedDeriv n (⇑f : (a : ℝ) → F) x) ≤ (SchwartzMap.seminorm 𝕜 k n : (a : 𝓢(ℝ, F)) → ℝ) f
Tactic: rwa [← Real.norm_eq_abs, ← norm_iteratedFDeriv_eq_norm_iteratedDeriv]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Basic (hypothesis)
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 : NormedField 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
f : 𝓢(E, F)
n : ℕ
x₀ : E
⊢ norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
      (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x₀) ≤
    (SchwartzMap.seminorm 𝕜 0 n : (a : 𝓢(E, F)) → ℝ) f
have this : HPow.hPow (β := ℕ) ‖x₀‖ 0 *
    norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
      (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x₀) ≤
  (SchwartzMap.seminorm 𝕜 0 n : (a : 𝓢(E, F)) → ℝ) f
Tactic: have := SchwartzMap.le_seminorm 𝕜 0 n f x₀
-- 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 : NormedField 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
f : 𝓢(E, F)
n : ℕ
x₀ : E
this :
  HPow.hPow (β := ℕ) ‖x₀‖ 0 *
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
        (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x₀) ≤
    (SchwartzMap.seminorm 𝕜 0 n : (a : 𝓢(E, F)) → ℝ) f
⊢ norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
      (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x₀) ≤
    (SchwartzMap.seminorm 𝕜 0 n : (a : 𝓢(E, F)) → ℝ) f
have rwa : ∀
  (this :
    1 *
        norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
          (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x₀) ≤
      (SchwartzMap.seminorm 𝕜 0 n : (a : 𝓢(E, F)) → ℝ) f),
  norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
      (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x₀) ≤
    (SchwartzMap.seminorm 𝕜 0 n : (a : 𝓢(E, F)) → ℝ) f
Tactic: rwa [pow_zero, one_mul] at this
Cleared hypotheses: this
-- 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 : NormedField 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
f : 𝓢(E, F)
n : ℕ
x₀ : E
this :
  HPow.hPow (β := ℕ) ‖x₀‖ 0 *
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
        (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x₀) ≤
    (SchwartzMap.seminorm 𝕜 0 n : (a : 𝓢(E, F)) → ℝ) f
rwa :
  ∀
    (this :
      1 *
          norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
            (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x₀) ≤
        (SchwartzMap.seminorm 𝕜 0 n : (a : 𝓢(E, F)) → ℝ) f),
    norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
        (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x₀) ≤
      (SchwartzMap.seminorm 𝕜 0 n : (a : 𝓢(E, F)) → ℝ) f
⊢ norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
      (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x₀) ≤
    (SchwartzMap.seminorm 𝕜 0 n : (a : 𝓢(E, F)) → ℝ) f
have rwa₁ : ∀
  (this :
    norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
        (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x₀) ≤
      (SchwartzMap.seminorm 𝕜 0 n : (a : 𝓢(E, F)) → ℝ) f),
  norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
      (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x₀) ≤
    (SchwartzMap.seminorm 𝕜 0 n : (a : 𝓢(E, F)) → ℝ) f
Tactic: rwa [pow_zero, one_mul] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Basic (hypothesis)
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 : NormedField 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
f : 𝓢(E, F)
k : ℕ
x₀ : E
⊢ ‖x₀‖ ^ k * norm.{u_6} (E := F) ((f : (a : E) → F) x₀ : F) ≤ (SchwartzMap.seminorm 𝕜 k 0 : (a : 𝓢(E, F)) → ℝ) f
have this : ‖x₀‖ ^ k *
    norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin 0) ↦ E) F)
      (iteratedFDeriv ℝ 0 (⇑f : (a : E) → F) x₀) ≤
  (SchwartzMap.seminorm 𝕜 k 0 : (a : 𝓢(E, F)) → ℝ) f
Tactic: have := SchwartzMap.le_seminorm 𝕜 k 0 f x₀
-- 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 : NormedField 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
f : 𝓢(E, F)
k : ℕ
x₀ : E
this :
  ‖x₀‖ ^ k *
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin 0) ↦ E) F)
        (iteratedFDeriv ℝ 0 (⇑f : (a : E) → F) x₀) ≤
    (SchwartzMap.seminorm 𝕜 k 0 : (a : 𝓢(E, F)) → ℝ) f
⊢ ‖x₀‖ ^ k * norm.{u_6} (E := F) ((f : (a : E) → F) x₀ : F) ≤ (SchwartzMap.seminorm 𝕜 k 0 : (a : 𝓢(E, F)) → ℝ) f
have rwa : ∀
  (this :
    ‖x₀‖ ^ k * norm.{u_6} (E := F) ((f : (a : E) → F) x₀ : F) ≤ (SchwartzMap.seminorm 𝕜 k 0 : (a : 𝓢(E, F)) → ℝ) f),
  ‖x₀‖ ^ k * norm.{u_6} (E := F) ((f : (a : E) → F) x₀ : F) ≤ (SchwartzMap.seminorm 𝕜 k 0 : (a : 𝓢(E, F)) → ℝ) f
Tactic: rwa [norm_iteratedFDeriv_zero] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Basic (hypothesis)
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 : NormedField 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
f : 𝓢(E, F)
x₀ : E
⊢ norm.{u_6} (E := F) ((f : (a : E) → F) x₀ : F) ≤ (SchwartzMap.seminorm 𝕜 0 0 : (a : 𝓢(E, F)) → ℝ) f
have this : HPow.hPow (β := ℕ) ‖x₀‖ 0 * norm.{u_6} (E := F) ((f : (a : E) → F) x₀ : F) ≤
  (SchwartzMap.seminorm 𝕜 0 0 : (a : 𝓢(E, F)) → ℝ) f
Tactic: have := norm_pow_mul_le_seminorm 𝕜 f 0 x₀
-- 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 : NormedField 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
f : 𝓢(E, F)
x₀ : E
this :
  HPow.hPow (β := ℕ) ‖x₀‖ 0 * norm.{u_6} (E := F) ((f : (a : E) → F) x₀ : F) ≤
    (SchwartzMap.seminorm 𝕜 0 0 : (a : 𝓢(E, F)) → ℝ) f
⊢ norm.{u_6} (E := F) ((f : (a : E) → F) x₀ : F) ≤ (SchwartzMap.seminorm 𝕜 0 0 : (a : 𝓢(E, F)) → ℝ) f
have rwa : ∀ (this : 1 * norm.{u_6} (E := F) ((f : (a : E) → F) x₀ : F) ≤ (SchwartzMap.seminorm 𝕜 0 0 : (a : 𝓢(E, F)) → ℝ) f),
  norm.{u_6} (E := F) ((f : (a : E) → F) x₀ : F) ≤ (SchwartzMap.seminorm 𝕜 0 0 : (a : 𝓢(E, F)) → ℝ) f
Tactic: rwa [pow_zero, one_mul] at this
Cleared hypotheses: this
-- 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 : NormedField 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
f : 𝓢(E, F)
x₀ : E
this :
  HPow.hPow (β := ℕ) ‖x₀‖ 0 * norm.{u_6} (E := F) ((f : (a : E) → F) x₀ : F) ≤
    (SchwartzMap.seminorm 𝕜 0 0 : (a : 𝓢(E, F)) → ℝ) f
rwa :
  ∀ (this : 1 * norm.{u_6} (E := F) ((f : (a : E) → F) x₀ : F) ≤ (SchwartzMap.seminorm 𝕜 0 0 : (a : 𝓢(E, F)) → ℝ) f),
    norm.{u_6} (E := F) ((f : (a : E) → F) x₀ : F) ≤ (SchwartzMap.seminorm 𝕜 0 0 : (a : 𝓢(E, F)) → ℝ) f
⊢ norm.{u_6} (E := F) ((f : (a : E) → F) x₀ : F) ≤ (SchwartzMap.seminorm 𝕜 0 0 : (a : 𝓢(E, F)) → ℝ) f
have rwa₁ : ∀ (this : norm.{u_6} (E := F) ((f : (a : E) → F) x₀ : F) ≤ (SchwartzMap.seminorm 𝕜 0 0 : (a : 𝓢(E, F)) → ℝ) f),
  norm.{u_6} (E := F) ((f : (a : E) → F) x₀ : F) ≤ (SchwartzMap.seminorm 𝕜 0 0 : (a : 𝓢(E, F)) → ℝ) f
Tactic: rwa [pow_zero, one_mul] at this
Cleared hypotheses: this
-- 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 : NormedField 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
m : ℕ × ℕ
k n : ℕ
hk : k ≤ m.1
hn : n ≤ m.2
f : 𝓢(E, F)
x : E
⊢ (1 + ‖x‖) ^ k *
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
        (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x) ≤
    HMul.hMul (β := ℝ) (HPow.hPow (α := ℝ) 2 m.1)
      (((Finset.Iic m).sup fun (m : ℕ × ℕ) ↦ SchwartzMap.seminorm 𝕜 m.1 m.2 : (a : 𝓢(E, F)) → ℝ) f : ℝ)
have rw : (∑ m ∈ Finset.range (k + 1), ‖x‖ ^ m * HPow.hPow (α := ℝ) 1 (k - m) * (↑(k.choose m) : ℝ)) *
    norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
      (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x) ≤
  HMul.hMul (β := ℝ) (HPow.hPow (α := ℝ) 2 m.1)
    (((Finset.Iic m).sup fun (m : ℕ × ℕ) ↦ SchwartzMap.seminorm 𝕜 m.1 m.2 : (a : 𝓢(E, F)) → ℝ) f : ℝ)
Tactic: rw [add_comm, add_pow]
-- 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 : NormedField 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
m : ℕ × ℕ
k n : ℕ
hk : k ≤ m.1
hn : n ≤ m.2
f : 𝓢(E, F)
x : E
⊢ (∑ m ∈ Finset.range (k + 1), ‖x‖ ^ m * HPow.hPow (α := ℝ) 1 (k - m) * (↑(k.choose m) : ℝ)) *
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
        (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x) ≤
    HMul.hMul (β := ℝ) (HPow.hPow (α := ℝ) 2 m.1)
      (((Finset.Iic m).sup fun (m : ℕ × ℕ) ↦ SchwartzMap.seminorm 𝕜 m.1 m.2 : (a : 𝓢(E, F)) → ℝ) f : ℝ)
have simp : ∑ i ∈ Finset.range (k + 1),
    ‖x‖ ^ i * (↑(k.choose i) : ℝ) *
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
        (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x) ≤
  HMul.hMul (β := ℝ) (HPow.hPow (α := ℝ) 2 m.1)
    (((Finset.Iic m).sup fun (m : ℕ × ℕ) ↦ SchwartzMap.seminorm 𝕜 m.1 m.2 : (a : 𝓢(E, F)) → ℝ) f : ℝ)
Tactic: simp only [one_pow, mul_one, Finset.sum_mul]
-- 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 : NormedField 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
m : ℕ × ℕ
k n : ℕ
hk : k ≤ m.1
hn : n ≤ m.2
f : 𝓢(E, F)
x : E
⊢ ∑ i ∈ Finset.range (k + 1),
      ‖x‖ ^ i * (↑(k.choose i) : ℝ) *
        norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
          (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x) ≤
    HMul.hMul (β := ℝ) (HPow.hPow (α := ℝ) 2 m.1)
      (((Finset.Iic m).sup fun (m : ℕ × ℕ) ↦ SchwartzMap.seminorm 𝕜 m.1 m.2 : (a : 𝓢(E, F)) → ℝ) f : ℝ)
have norm_cast : ∑ i ∈ Finset.range (k + 1),
    ‖x‖ ^ i * (↑(k.choose i) : ℝ) *
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
        (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x) ≤
  HMul.hMul (α := ℝ) (β := ℝ) ((↑(HPow.hPow (α := ℕ) 2 m.1) : ℝ) : ℝ)
    (((Finset.Iic m).sup fun (m : ℕ × ℕ) ↦ SchwartzMap.seminorm 𝕜 m.1 m.2 : (a : 𝓢(E, F)) → ℝ) f : ℝ)
Tactic: norm_cast
-- 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 : NormedField 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
m : ℕ × ℕ
k n : ℕ
hk : k ≤ m.1
hn : n ≤ m.2
f : 𝓢(E, F)
x : E
⊢ ∑ i ∈ Finset.range (k + 1),
      ‖x‖ ^ i * (↑(k.choose i) : ℝ) *
        norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
          (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x) ≤
    HMul.hMul (α := ℝ) (β := ℝ) ((↑(HPow.hPow (α := ℕ) 2 m.1) : ℝ) : ℝ)
      (((Finset.Iic m).sup fun (m : ℕ × ℕ) ↦ SchwartzMap.seminorm 𝕜 m.1 m.2 : (a : 𝓢(E, F)) → ℝ) f : ℝ)
have rw : ∑ i ∈ Finset.range (k + 1),
    ‖x‖ ^ i * (↑(k.choose i) : ℝ) *
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
        (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x) ≤
  HMul.hMul (α := ℝ) (β := ℝ) ((↑(∑ m_1 ∈ Finset.range (m.1 + 1), m.1.choose m_1) : ℝ) : ℝ)
    (((Finset.Iic m).sup fun (m : ℕ × ℕ) ↦ SchwartzMap.seminorm 𝕜 m.1 m.2 : (a : 𝓢(E, F)) → ℝ) f : ℝ)
Tactic: rw [← Nat.sum_range_choose m.1]
-- 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 : NormedField 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
m : ℕ × ℕ
k n : ℕ
hk : k ≤ m.1
hn : n ≤ m.2
f : 𝓢(E, F)
x : E
⊢ ∑ i ∈ Finset.range (k + 1),
      ‖x‖ ^ i * (↑(k.choose i) : ℝ) *
        norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
          (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x) ≤
    HMul.hMul (α := ℝ) (β := ℝ) ((↑(∑ m_1 ∈ Finset.range (m.1 + 1), m.1.choose m_1) : ℝ) : ℝ)
      (((Finset.Iic m).sup fun (m : ℕ × ℕ) ↦ SchwartzMap.seminorm 𝕜 m.1 m.2 : (a : 𝓢(E, F)) → ℝ) f : ℝ)
have push_cast : ∑ i ∈ Finset.range (k + 1),
    ‖x‖ ^ i * (↑(k.choose i) : ℝ) *
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
        (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x) ≤
  HMul.hMul (α := ℝ) (β := ℝ) (∑ x ∈ Finset.range (m.1 + 1), (↑(m.1.choose x) : ℝ) : ℝ)
    (((Finset.Iic m).sup fun (m : ℕ × ℕ) ↦ SchwartzMap.seminorm 𝕜 m.1 m.2 : (a : 𝓢(E, F)) → ℝ) f : ℝ)
Tactic: push_cast
-- 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 : NormedField 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
m : ℕ × ℕ
k n : ℕ
hk : k ≤ m.1
hn : n ≤ m.2
f : 𝓢(E, F)
x : E
⊢ ∑ i ∈ Finset.range (k + 1),
      ‖x‖ ^ i * (↑(k.choose i) : ℝ) *
        norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
          (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x) ≤
    HMul.hMul (α := ℝ) (β := ℝ) (∑ x ∈ Finset.range (m.1 + 1), (↑(m.1.choose x) : ℝ) : ℝ)
      (((Finset.Iic m).sup fun (m : ℕ × ℕ) ↦ SchwartzMap.seminorm 𝕜 m.1 m.2 : (a : 𝓢(E, F)) → ℝ) f : ℝ)
have rw : LE.le (α := ℝ)
  (∑ i ∈ Finset.range (k + 1),
    ‖x‖ ^ i * (↑(k.choose i) : ℝ) *
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
        (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x))
  (∑ i ∈ Finset.range (m.1 + 1),
    HMul.hMul (α := ℝ) (β := ℝ) ((↑(m.1.choose i) : ℝ) : ℝ)
      (((Finset.Iic m).sup fun (m : ℕ × ℕ) ↦ SchwartzMap.seminorm 𝕜 m.1 m.2 : (a : 𝓢(E, F)) → ℝ) f : ℝ))
Tactic: rw [Finset.sum_mul]
-- Lean 4 proof step from Mathlib.Analysis.Distribution.SchwartzSpace.Basic (hypothesis)
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 : NormedField 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
m : ℕ × ℕ
k n : ℕ
hk : k ≤ m.1
hn : n ≤ m.2
f : 𝓢(E, F)
x : E
⊢ LE.le (α := ℝ)
    (∑ i ∈ Finset.range (k + 1),
      ‖x‖ ^ i * (↑(k.choose i) : ℝ) *
        norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
          (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x))
    (∑ i ∈ Finset.range (m.1 + 1),
      HMul.hMul (α := ℝ) (β := ℝ) ((↑(m.1.choose i) : ℝ) : ℝ)
        (((Finset.Iic m).sup fun (m : ℕ × ℕ) ↦ SchwartzMap.seminorm 𝕜 m.1 m.2 : (a : 𝓢(E, F)) → ℝ) f : ℝ))
have hk' : Finset.range (k + 1) ⊆ Finset.range (m.1 + 1)
Tactic: have hk' : Finset.range (k + 1) ⊆ Finset.range (m.1 + 1) := by grind
-- 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 : NormedField 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
m : ℕ × ℕ
k n : ℕ
hk : k ≤ m.1
hn : n ≤ m.2
f : 𝓢(E, F)
x : E
hk' : Finset.range (k + 1) ⊆ Finset.range (m.1 + 1)
⊢ LE.le (α := ℝ)
    (∑ i ∈ Finset.range (k + 1),
      ‖x‖ ^ i * (↑(k.choose i) : ℝ) *
        norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
          (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x))
    (∑ i ∈ Finset.range (m.1 + 1),
      HMul.hMul (α := ℝ) (β := ℝ) ((↑(m.1.choose i) : ℝ) : ℝ)
        (((Finset.Iic m).sup fun (m : ℕ × ℕ) ↦ SchwartzMap.seminorm 𝕜 m.1 m.2 : (a : 𝓢(E, F)) → ℝ) f : ℝ))
have grw : LE.le (α := ℝ)
  (∑ i ∈ Finset.range (m.1 + 1),
    ‖x‖ ^ i * (↑(k.choose i) : ℝ) *
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
        (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x))
  (∑ i ∈ Finset.range (m.1 + 1),
    HMul.hMul (α := ℝ) (β := ℝ) ((↑(m.1.choose i) : ℝ) : ℝ)
      (((Finset.Iic m).sup fun (m : ℕ × ℕ) ↦ SchwartzMap.seminorm 𝕜 m.1 m.2 : (a : 𝓢(E, F)) → ℝ) f : ℝ))
Tactic: grw [hk']
-- 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 : NormedField 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
m : ℕ × ℕ
k n : ℕ
hk : k ≤ m.1
hn : n ≤ m.2
f : 𝓢(E, F)
x : E
hk' : Finset.range (k + 1) ⊆ Finset.range (m.1 + 1)
⊢ LE.le (α := ℝ)
    (∑ i ∈ Finset.range (m.1 + 1),
      ‖x‖ ^ i * (↑(k.choose i) : ℝ) *
        norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
          (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x))
    (∑ i ∈ Finset.range (m.1 + 1),
      HMul.hMul (α := ℝ) (β := ℝ) ((↑(m.1.choose i) : ℝ) : ℝ)
        (((Finset.Iic m).sup fun (m : ℕ × ℕ) ↦ SchwartzMap.seminorm 𝕜 m.1 m.2 : (a : 𝓢(E, F)) → ℝ) f : ℝ))
have h : ∀ (i : ℕ) (hi : i ∈ Finset.range (m.1 + 1)),
  ‖x‖ ^ i * (↑(k.choose i) : ℝ) *
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
        (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x) ≤
    HMul.hMul (α := ℝ) (β := ℝ) ((↑(m.1.choose i) : ℝ) : ℝ)
      (((Finset.Iic m).sup fun (m : ℕ × ℕ) ↦ SchwartzMap.seminorm 𝕜 m.1 m.2 : (a : 𝓢(E, F)) → ℝ) f : ℝ)
Tactic: gcongr ∑ _i ∈ Finset.range (m.1 + 1), ?_ with i hi
-- 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 : NormedField 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
m : ℕ × ℕ
k n : ℕ
hk : k ≤ m.1
hn : n ≤ m.2
f : 𝓢(E, F)
x : E
hk' : Finset.range (k + 1) ⊆ Finset.range (m.1 + 1)
i : ℕ
hi : i ∈ Finset.range (m.1 + 1)
⊢ ‖x‖ ^ i * (↑(k.choose i) : ℝ) *
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
        (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x) ≤
    HMul.hMul (α := ℝ) (β := ℝ) ((↑(m.1.choose i) : ℝ) : ℝ)
      (((Finset.Iic m).sup fun (m : ℕ × ℕ) ↦ SchwartzMap.seminorm 𝕜 m.1 m.2 : (a : 𝓢(E, F)) → ℝ) f : ℝ)
have h : ‖x‖ ^ i *
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
        (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x) *
    (↑(k.choose i) : ℝ) ≤
  HMul.hMul (α := ℝ) (β := ℝ)
    (((Finset.Iic m).sup fun (m : ℕ × ℕ) ↦ SchwartzMap.seminorm 𝕜 m.1 m.2 : (a : 𝓢(E, F)) → ℝ) f : ℝ)
    ((↑(m.1.choose i) : ℝ) : ℝ)
Tactic: move_mul [(Nat.choose k i : ℝ), (Nat.choose m.1 i : ℝ)]
-- 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 : NormedField 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
m : ℕ × ℕ
k n : ℕ
hk : k ≤ m.1
hn : n ≤ m.2
f : 𝓢(E, F)
x : E
hk' : Finset.range (k + 1) ⊆ Finset.range (m.1 + 1)
i : ℕ
hi : i ∈ Finset.range (m.1 + 1)
⊢ ‖x‖ ^ i *
        norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
          (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x) *
      (↑(k.choose i) : ℝ) ≤
    HMul.hMul (α := ℝ) (β := ℝ)
      (((Finset.Iic m).sup fun (m : ℕ × ℕ) ↦ SchwartzMap.seminorm 𝕜 m.1 m.2 : (a : 𝓢(E, F)) → ℝ) f : ℝ)
      ((↑(m.1.choose i) : ℝ) : ℝ)
have h : ‖x‖ ^ i *
    norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
      (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x) ≤
  ((Finset.Iic m).sup fun (m : ℕ × ℕ) ↦ SchwartzMap.seminorm 𝕜 m.1 m.2 : (a : 𝓢(E, F)) → ℝ) f
Tactic: gcongr
-- 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 : NormedField 𝕜
inst_5 : NormedSpace 𝕜 F
inst_6 : SMulCommClass ℝ 𝕜 F
m : ℕ × ℕ
k n : ℕ
hk : k ≤ m.1
hn : n ≤ m.2
f : 𝓢(E, F)
x : E
hk' : Finset.range (k + 1) ⊆ Finset.range (m.1 + 1)
i : ℕ
hi : i ∈ Finset.range (m.1 + 1)
⊢ ‖x‖ ^ i *
      norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin n) ↦ E) F)
        (iteratedFDeriv ℝ n (⇑f : (a : E) → F) x) ≤
    ((Finset.Iic m).sup fun (m : ℕ × ℕ) ↦ SchwartzMap.seminorm 𝕜 m.1 m.2 : (a : 𝓢(E, F)) → ℝ) f
have h : LE.le (α := ℝ) ((SchwartzMap.seminorm 𝕜 i n : (a : 𝓢(E, F)) → ℝ) f : ℝ)
  (((Finset.Iic m).sup fun (m : ℕ × ℕ) ↦ SchwartzMap.seminorm 𝕜 m.1 m.2 : (a : 𝓢(E, F)) → ℝ) f : ℝ)
Tactic: grw [le_seminorm 𝕜 i n f x]