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 : RCLike 𝕜
inst_5 : NormedAddCommGroup D
inst_6 : NormedSpace ℝ D
inst_7 : NormedSpace 𝕜 F
g : D → E
hg : Function.HasTemperateGrowth g
k n l : ℕ
C : ℝ
hC : 0 ≤ C
hgrowth :
  ∀ N ≤ n,
    ∀ (x : D),
      norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_5} ℝ (fun (i : Fin N) ↦ D) E) (iteratedFDeriv ℝ N g x) ≤
        C * (1 + ‖x‖) ^ l
kg : ℕ
Cg : ℝ
hg_upper' : ∀ (x : D), ‖x‖ ≤ Cg * (1 + ‖g x‖) ^ kg
hCg : 1 ≤ 1 + Cg
k' : ℕ := kg * (k + l * n)
f : 𝓢(E, F)
x : D
seminorm_f : ℝ := ((Finset.Iic (k', n)).sup (schwartzSeminormFamily 𝕜 E F) : (a : 𝓢(E, F)) → ℝ) f
hg_upper'' : (1 + ‖x‖) ^ (k + l * n) ≤ (1 + Cg) ^ (k + l * n) * (1 + ‖g x‖) ^ k'
hbound :
  ∀ (i : ℕ) (hi : i ≤ n),
    norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin i) ↦ E) F)
        (iteratedFDeriv ℝ i (⇑f : (a : E) → F) (g x)) ≤
      HPow.hPow (α := ℝ) 2 k' * seminorm_f / (1 + ‖g x‖) ^ k'
hgrowth' :
  ∀ (N : ℕ) (hN₁ : 1 ≤ N) (hN₂ : N ≤ n),
    norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_5} ℝ (fun (i : Fin N) ↦ D) E) (iteratedFDeriv ℝ N g x) ≤
      ((C + 1) * (1 + ‖x‖) ^ l) ^ N
this :
  norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_6} ℝ (fun (i : Fin n) ↦ D) F)
      (iteratedFDeriv ℝ n ((⇑f : (a : E) → F) ∘ g) x) ≤
    (↑n ! : ℝ) * (HPow.hPow (α := ℝ) 2 k' * seminorm_f / (1 + ‖g x‖) ^ k') * ((C + 1) * (1 + ‖x‖) ^ l) ^ n
hxk : ‖x‖ ^ k ≤ (1 + ‖x‖) ^ k
⊢ ‖x‖ ^ (k, n).1 *
      norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_6} ℝ (fun (i : Fin (k, n).2) ↦ D) F)
        (iteratedFDeriv ℝ (k, n).2 ((fun (f : 𝓢(E, F)) ↦ ((⇑f : (a : E) → F) ∘ g : D → F)) f) x) ≤
    HMul.hMul (β := ℝ) ((1 + Cg) ^ (k + l * n) * ((C + 1) ^ n * (↑n ! : ℝ) * HPow.hPow (α := ℝ) 2 k'))
      (((Finset.Iic (k', n)).sup (schwartzSeminormFamily 𝕜 E F) : (a : 𝓢(E, F)) → ℝ) f : ℝ)
have right : (1 + ‖x‖) ^ k *
    ((↑n ! : ℝ) * (HPow.hPow (α := ℝ) 2 k' * seminorm_f / (1 + ‖g x‖) ^ k') * ((C + 1) * (1 + ‖x‖) ^ l) ^ n) ≤
  HMul.hMul (β := ℝ) ((1 + Cg) ^ (k + l * n) * ((C + 1) ^ n * (↑n ! : ℝ) * HPow.hPow (α := ℝ) 2 k'))
    (((Finset.Iic (k', n)).sup (schwartzSeminormFamily 𝕜 E F) : (a : 𝓢(E, F)) → ℝ) f : ℝ)
Tactic: grw [hxk, this]
-- 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 : RCLike 𝕜
inst_5 : NormedAddCommGroup D
inst_6 : NormedSpace ℝ D
inst_7 : NormedSpace 𝕜 F
g : D → E
hg : Function.HasTemperateGrowth g
k n l : ℕ
C : ℝ
hC : 0 ≤ C
hgrowth :
  ∀ N ≤ n,
    ∀ (x : D),
      norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_5} ℝ (fun (i : Fin N) ↦ D) E) (iteratedFDeriv ℝ N g x) ≤
        C * (1 + ‖x‖) ^ l
kg : ℕ
Cg : ℝ
hg_upper' : ∀ (x : D), ‖x‖ ≤ Cg * (1 + ‖g x‖) ^ kg
hCg : 1 ≤ 1 + Cg
k' : ℕ := kg * (k + l * n)
f : 𝓢(E, F)
x : D
seminorm_f : ℝ := ((Finset.Iic (k', n)).sup (schwartzSeminormFamily 𝕜 E F) : (a : 𝓢(E, F)) → ℝ) f
hg_upper'' : (1 + ‖x‖) ^ (k + l * n) ≤ (1 + Cg) ^ (k + l * n) * (1 + ‖g x‖) ^ k'
hbound :
  ∀ (i : ℕ) (hi : i ≤ n),
    norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin i) ↦ E) F)
        (iteratedFDeriv ℝ i (⇑f : (a : E) → F) (g x)) ≤
      HPow.hPow (α := ℝ) 2 k' * seminorm_f / (1 + ‖g x‖) ^ k'
hgrowth' :
  ∀ (N : ℕ) (hN₁ : 1 ≤ N) (hN₂ : N ≤ n),
    norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_5} ℝ (fun (i : Fin N) ↦ D) E) (iteratedFDeriv ℝ N g x) ≤
      ((C + 1) * (1 + ‖x‖) ^ l) ^ N
this :
  norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_6} ℝ (fun (i : Fin n) ↦ D) F)
      (iteratedFDeriv ℝ n ((⇑f : (a : E) → F) ∘ g) x) ≤
    (↑n ! : ℝ) * (HPow.hPow (α := ℝ) 2 k' * seminorm_f / (1 + ‖g x‖) ^ k') * ((C + 1) * (1 + ‖x‖) ^ l) ^ n
hxk : ‖x‖ ^ k ≤ (1 + ‖x‖) ^ k
⊢ (1 + ‖x‖) ^ k *
      ((↑n ! : ℝ) * (HPow.hPow (α := ℝ) 2 k' * seminorm_f / (1 + ‖g x‖) ^ k') * ((C + 1) * (1 + ‖x‖) ^ l) ^ n) =
    (1 + ‖x‖) ^ (k + l * n) / (1 + ‖g x‖) ^ k' * ((C + 1) ^ n * (↑n ! : ℝ) * HPow.hPow (α := ℝ) 2 k' * seminorm_f)
have rw : (1 + ‖x‖) ^ k *
    ((↑n ! : ℝ) * (HPow.hPow (α := ℝ) 2 k' * seminorm_f / (1 + ‖g x‖) ^ k') * ((C + 1) ^ n * (1 + ‖x‖) ^ (l * n))) =
  (1 + ‖x‖) ^ k * (1 + ‖x‖) ^ (l * n) / (1 + ‖g x‖) ^ k' *
    ((C + 1) ^ n * (↑n ! : ℝ) * HPow.hPow (α := ℝ) 2 k' * seminorm_f)
Tactic: rw [mul_pow, pow_add, ← pow_mul]
-- 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 : RCLike 𝕜
inst_5 : NormedAddCommGroup D
inst_6 : NormedSpace ℝ D
inst_7 : NormedSpace 𝕜 F
g : D → E
hg : Function.HasTemperateGrowth g
k n l : ℕ
C : ℝ
hC : 0 ≤ C
hgrowth :
  ∀ N ≤ n,
    ∀ (x : D),
      norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_5} ℝ (fun (i : Fin N) ↦ D) E) (iteratedFDeriv ℝ N g x) ≤
        C * (1 + ‖x‖) ^ l
kg : ℕ
Cg : ℝ
hg_upper' : ∀ (x : D), ‖x‖ ≤ Cg * (1 + ‖g x‖) ^ kg
hCg : 1 ≤ 1 + Cg
k' : ℕ := kg * (k + l * n)
f : 𝓢(E, F)
x : D
seminorm_f : ℝ := ((Finset.Iic (k', n)).sup (schwartzSeminormFamily 𝕜 E F) : (a : 𝓢(E, F)) → ℝ) f
hg_upper'' : (1 + ‖x‖) ^ (k + l * n) ≤ (1 + Cg) ^ (k + l * n) * (1 + ‖g x‖) ^ k'
hbound :
  ∀ (i : ℕ) (hi : i ≤ n),
    norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin i) ↦ E) F)
        (iteratedFDeriv ℝ i (⇑f : (a : E) → F) (g x)) ≤
      HPow.hPow (α := ℝ) 2 k' * seminorm_f / (1 + ‖g x‖) ^ k'
hgrowth' :
  ∀ (N : ℕ) (hN₁ : 1 ≤ N) (hN₂ : N ≤ n),
    norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_5} ℝ (fun (i : Fin N) ↦ D) E) (iteratedFDeriv ℝ N g x) ≤
      ((C + 1) * (1 + ‖x‖) ^ l) ^ N
this :
  norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_6} ℝ (fun (i : Fin n) ↦ D) F)
      (iteratedFDeriv ℝ n ((⇑f : (a : E) → F) ∘ g) x) ≤
    (↑n ! : ℝ) * (HPow.hPow (α := ℝ) 2 k' * seminorm_f / (1 + ‖g x‖) ^ k') * ((C + 1) * (1 + ‖x‖) ^ l) ^ n
hxk : ‖x‖ ^ k ≤ (1 + ‖x‖) ^ k
⊢ (1 + ‖x‖) ^ k *
      ((↑n ! : ℝ) * (HPow.hPow (α := ℝ) 2 k' * seminorm_f / (1 + ‖g x‖) ^ k') * ((C + 1) * (1 + ‖x‖) ^ l) ^ n) ≤
    HMul.hMul (β := ℝ) ((1 + Cg) ^ (k + l * n) * ((C + 1) ^ n * (↑n ! : ℝ) * HPow.hPow (α := ℝ) 2 k'))
      (((Finset.Iic (k', n)).sup (schwartzSeminormFamily 𝕜 E F) : (a : 𝓢(E, F)) → ℝ) f : ℝ)
have rearrange : (1 + ‖x‖) ^ k *
    ((↑n ! : ℝ) * (HPow.hPow (α := ℝ) 2 k' * seminorm_f / (1 + ‖g x‖) ^ k') * ((C + 1) * (1 + ‖x‖) ^ l) ^ n) =
  (1 + ‖x‖) ^ (k + l * n) / (1 + ‖g x‖) ^ k' * ((C + 1) ^ n * (↑n ! : ℝ) * HPow.hPow (α := ℝ) 2 k' * seminorm_f)
Tactic: have rearrange :
    (1 + ‖x‖) ^ k *
        (n ! * (2 ^ k' * seminorm_f / (1 + ‖g x‖) ^ k') * ((C + 1) * (1 + ‖x‖) ^ l) ^ n) =
      (1 + ‖x‖) ^ (k + l * n) / (1 + ‖g x‖) ^ k' *
        ((C + 1) ^ n * n ! * 2 ^ k' * seminorm_f) := by
    rw [mul_pow, pow_add, ← pow_mul]
    ring
-- 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 : RCLike 𝕜
inst_5 : NormedAddCommGroup D
inst_6 : NormedSpace ℝ D
inst_7 : NormedSpace 𝕜 F
g : D → E
hg : Function.HasTemperateGrowth g
k n l : ℕ
C : ℝ
hC : 0 ≤ C
hgrowth :
  ∀ N ≤ n,
    ∀ (x : D),
      norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_5} ℝ (fun (i : Fin N) ↦ D) E) (iteratedFDeriv ℝ N g x) ≤
        C * (1 + ‖x‖) ^ l
kg : ℕ
Cg : ℝ
hg_upper' : ∀ (x : D), ‖x‖ ≤ Cg * (1 + ‖g x‖) ^ kg
hCg : 1 ≤ 1 + Cg
k' : ℕ := kg * (k + l * n)
f : 𝓢(E, F)
x : D
seminorm_f : ℝ := ((Finset.Iic (k', n)).sup (schwartzSeminormFamily 𝕜 E F) : (a : 𝓢(E, F)) → ℝ) f
hg_upper'' : (1 + ‖x‖) ^ (k + l * n) ≤ (1 + Cg) ^ (k + l * n) * (1 + ‖g x‖) ^ k'
hbound :
  ∀ (i : ℕ) (hi : i ≤ n),
    norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin i) ↦ E) F)
        (iteratedFDeriv ℝ i (⇑f : (a : E) → F) (g x)) ≤
      HPow.hPow (α := ℝ) 2 k' * seminorm_f / (1 + ‖g x‖) ^ k'
hgrowth' :
  ∀ (N : ℕ) (hN₁ : 1 ≤ N) (hN₂ : N ≤ n),
    norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_5} ℝ (fun (i : Fin N) ↦ D) E) (iteratedFDeriv ℝ N g x) ≤
      ((C + 1) * (1 + ‖x‖) ^ l) ^ N
this :
  norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_6} ℝ (fun (i : Fin n) ↦ D) F)
      (iteratedFDeriv ℝ n ((⇑f : (a : E) → F) ∘ g) x) ≤
    (↑n ! : ℝ) * (HPow.hPow (α := ℝ) 2 k' * seminorm_f / (1 + ‖g x‖) ^ k') * ((C + 1) * (1 + ‖x‖) ^ l) ^ n
hxk : ‖x‖ ^ k ≤ (1 + ‖x‖) ^ k
rearrange :
  (1 + ‖x‖) ^ k *
      ((↑n ! : ℝ) * (HPow.hPow (α := ℝ) 2 k' * seminorm_f / (1 + ‖g x‖) ^ k') * ((C + 1) * (1 + ‖x‖) ^ l) ^ n) =
    (1 + ‖x‖) ^ (k + l * n) / (1 + ‖g x‖) ^ k' * ((C + 1) ^ n * (↑n ! : ℝ) * HPow.hPow (α := ℝ) 2 k' * seminorm_f)
⊢ (1 + ‖x‖) ^ k *
      ((↑n ! : ℝ) * (HPow.hPow (α := ℝ) 2 k' * seminorm_f / (1 + ‖g x‖) ^ k') * ((C + 1) * (1 + ‖x‖) ^ l) ^ n) ≤
    HMul.hMul (β := ℝ) ((1 + Cg) ^ (k + l * n) * ((C + 1) ^ n * (↑n ! : ℝ) * HPow.hPow (α := ℝ) 2 k'))
      (((Finset.Iic (k', n)).sup (schwartzSeminormFamily 𝕜 E F) : (a : 𝓢(E, F)) → ℝ) f : ℝ)
have right : (1 + ‖x‖) ^ (k + l * n) / (1 + ‖g x‖) ^ k' * ((C + 1) ^ n * (↑n ! : ℝ) * HPow.hPow (α := ℝ) 2 k' * seminorm_f) ≤
  HMul.hMul (β := ℝ) ((1 + Cg) ^ (k + l * n) * ((C + 1) ^ n * (↑n ! : ℝ) * HPow.hPow (α := ℝ) 2 k'))
    (((Finset.Iic (k', n)).sup (schwartzSeminormFamily 𝕜 E F) : (a : 𝓢(E, F)) → ℝ) f : ℝ)
Tactic: rw [rearrange]
-- 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 : RCLike 𝕜
inst_5 : NormedAddCommGroup D
inst_6 : NormedSpace ℝ D
inst_7 : NormedSpace 𝕜 F
g : D → E
hg : Function.HasTemperateGrowth g
k n l : ℕ
C : ℝ
hC : 0 ≤ C
hgrowth :
  ∀ N ≤ n,
    ∀ (x : D),
      norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_5} ℝ (fun (i : Fin N) ↦ D) E) (iteratedFDeriv ℝ N g x) ≤
        C * (1 + ‖x‖) ^ l
kg : ℕ
Cg : ℝ
hg_upper' : ∀ (x : D), ‖x‖ ≤ Cg * (1 + ‖g x‖) ^ kg
hCg : 1 ≤ 1 + Cg
k' : ℕ := kg * (k + l * n)
f : 𝓢(E, F)
x : D
seminorm_f : ℝ := ((Finset.Iic (k', n)).sup (schwartzSeminormFamily 𝕜 E F) : (a : 𝓢(E, F)) → ℝ) f
hg_upper'' : (1 + ‖x‖) ^ (k + l * n) ≤ (1 + Cg) ^ (k + l * n) * (1 + ‖g x‖) ^ k'
hbound :
  ∀ (i : ℕ) (hi : i ≤ n),
    norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin i) ↦ E) F)
        (iteratedFDeriv ℝ i (⇑f : (a : E) → F) (g x)) ≤
      HPow.hPow (α := ℝ) 2 k' * seminorm_f / (1 + ‖g x‖) ^ k'
hgrowth' :
  ∀ (N : ℕ) (hN₁ : 1 ≤ N) (hN₂ : N ≤ n),
    norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_5} ℝ (fun (i : Fin N) ↦ D) E) (iteratedFDeriv ℝ N g x) ≤
      ((C + 1) * (1 + ‖x‖) ^ l) ^ N
this :
  norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_6} ℝ (fun (i : Fin n) ↦ D) F)
      (iteratedFDeriv ℝ n ((⇑f : (a : E) → F) ∘ g) x) ≤
    (↑n ! : ℝ) * (HPow.hPow (α := ℝ) 2 k' * seminorm_f / (1 + ‖g x‖) ^ k') * ((C + 1) * (1 + ‖x‖) ^ l) ^ n
hxk : ‖x‖ ^ k ≤ (1 + ‖x‖) ^ k
rearrange :
  (1 + ‖x‖) ^ k *
      ((↑n ! : ℝ) * (HPow.hPow (α := ℝ) 2 k' * seminorm_f / (1 + ‖g x‖) ^ k') * ((C + 1) * (1 + ‖x‖) ^ l) ^ n) =
    (1 + ‖x‖) ^ (k + l * n) / (1 + ‖g x‖) ^ k' * ((C + 1) ^ n * (↑n ! : ℝ) * HPow.hPow (α := ℝ) 2 k' * seminorm_f)
⊢ (1 + ‖x‖) ^ (k + l * n) / (1 + ‖g x‖) ^ k' * ((C + 1) ^ n * (↑n ! : ℝ) * HPow.hPow (α := ℝ) 2 k' * seminorm_f) ≤
    HMul.hMul (β := ℝ) ((1 + Cg) ^ (k + l * n) * ((C + 1) ^ n * (↑n ! : ℝ) * HPow.hPow (α := ℝ) 2 k'))
      (((Finset.Iic (k', n)).sup (schwartzSeminormFamily 𝕜 E F) : (a : 𝓢(E, F)) → ℝ) f : ℝ)
have hgxk' : 0 < (1 + ‖g x‖) ^ k'
Tactic: have hgxk' : 0 < (1 + ‖g x‖) ^ 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 : RCLike 𝕜
inst_5 : NormedAddCommGroup D
inst_6 : NormedSpace ℝ D
inst_7 : NormedSpace 𝕜 F
g : D → E
hg : Function.HasTemperateGrowth g
k n l : ℕ
C : ℝ
hC : 0 ≤ C
hgrowth :
  ∀ N ≤ n,
    ∀ (x : D),
      norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_5} ℝ (fun (i : Fin N) ↦ D) E) (iteratedFDeriv ℝ N g x) ≤
        C * (1 + ‖x‖) ^ l
kg : ℕ
Cg : ℝ
hg_upper' : ∀ (x : D), ‖x‖ ≤ Cg * (1 + ‖g x‖) ^ kg
hCg : 1 ≤ 1 + Cg
k' : ℕ := kg * (k + l * n)
f : 𝓢(E, F)
x : D
seminorm_f : ℝ := ((Finset.Iic (k', n)).sup (schwartzSeminormFamily 𝕜 E F) : (a : 𝓢(E, F)) → ℝ) f
hg_upper'' : (1 + ‖x‖) ^ (k + l * n) ≤ (1 + Cg) ^ (k + l * n) * (1 + ‖g x‖) ^ k'
hbound :
  ∀ (i : ℕ) (hi : i ≤ n),
    norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin i) ↦ E) F)
        (iteratedFDeriv ℝ i (⇑f : (a : E) → F) (g x)) ≤
      HPow.hPow (α := ℝ) 2 k' * seminorm_f / (1 + ‖g x‖) ^ k'
hgrowth' :
  ∀ (N : ℕ) (hN₁ : 1 ≤ N) (hN₂ : N ≤ n),
    norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_5} ℝ (fun (i : Fin N) ↦ D) E) (iteratedFDeriv ℝ N g x) ≤
      ((C + 1) * (1 + ‖x‖) ^ l) ^ N
this :
  norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_6} ℝ (fun (i : Fin n) ↦ D) F)
      (iteratedFDeriv ℝ n ((⇑f : (a : E) → F) ∘ g) x) ≤
    (↑n ! : ℝ) * (HPow.hPow (α := ℝ) 2 k' * seminorm_f / (1 + ‖g x‖) ^ k') * ((C + 1) * (1 + ‖x‖) ^ l) ^ n
hxk : ‖x‖ ^ k ≤ (1 + ‖x‖) ^ k
rearrange :
  (1 + ‖x‖) ^ k *
      ((↑n ! : ℝ) * (HPow.hPow (α := ℝ) 2 k' * seminorm_f / (1 + ‖g x‖) ^ k') * ((C + 1) * (1 + ‖x‖) ^ l) ^ n) =
    (1 + ‖x‖) ^ (k + l * n) / (1 + ‖g x‖) ^ k' * ((C + 1) ^ n * (↑n ! : ℝ) * HPow.hPow (α := ℝ) 2 k' * seminorm_f)
hgxk' : 0 < (1 + ‖g x‖) ^ k'
⊢ (1 + ‖x‖) ^ (k + l * n) / (1 + ‖g x‖) ^ k' * ((C + 1) ^ n * (↑n ! : ℝ) * HPow.hPow (α := ℝ) 2 k' * seminorm_f) ≤
    HMul.hMul (β := ℝ) ((1 + Cg) ^ (k + l * n) * ((C + 1) ^ n * (↑n ! : ℝ) * HPow.hPow (α := ℝ) 2 k'))
      (((Finset.Iic (k', n)).sup (schwartzSeminormFamily 𝕜 E F) : (a : 𝓢(E, F)) → ℝ) f : ℝ)
have hg_upper''₁ : (1 + ‖x‖) ^ (k + l * n) / (1 + ‖g x‖) ^ k' ≤ (1 + Cg) ^ (k + l * n)
Tactic: rw [← div_le_iff₀ hgxk'] at hg_upper''
Cleared hypotheses: hg_upper'', hbound, hgrowth', this, hxk, rearrange, hgxk'
-- 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 : RCLike 𝕜
inst_5 : NormedAddCommGroup D
inst_6 : NormedSpace ℝ D
inst_7 : NormedSpace 𝕜 F
g : D → E
hg : Function.HasTemperateGrowth g
k n l : ℕ
C : ℝ
hC : 0 ≤ C
hgrowth :
  ∀ N ≤ n,
    ∀ (x : D),
      norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_5} ℝ (fun (i : Fin N) ↦ D) E) (iteratedFDeriv ℝ N g x) ≤
        C * (1 + ‖x‖) ^ l
kg : ℕ
Cg : ℝ
hg_upper' : ∀ (x : D), ‖x‖ ≤ Cg * (1 + ‖g x‖) ^ kg
hCg : 1 ≤ 1 + Cg
k' : ℕ := kg * (k + l * n)
f : 𝓢(E, F)
x : D
seminorm_f : ℝ := ((Finset.Iic (k', n)).sup (schwartzSeminormFamily 𝕜 E F) : (a : 𝓢(E, F)) → ℝ) f
hg_upper'' : (1 + ‖x‖) ^ (k + l * n) / (1 + ‖g x‖) ^ k' ≤ (1 + Cg) ^ (k + l * n)
hbound :
  ∀ (i : ℕ) (hi : i ≤ n),
    norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin i) ↦ E) F)
        (iteratedFDeriv ℝ i (⇑f : (a : E) → F) (g x)) ≤
      HPow.hPow (α := ℝ) 2 k' * seminorm_f / (1 + ‖g x‖) ^ k'
hgrowth' :
  ∀ (N : ℕ) (hN₁ : 1 ≤ N) (hN₂ : N ≤ n),
    norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_5} ℝ (fun (i : Fin N) ↦ D) E) (iteratedFDeriv ℝ N g x) ≤
      ((C + 1) * (1 + ‖x‖) ^ l) ^ N
this :
  norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_6} ℝ (fun (i : Fin n) ↦ D) F)
      (iteratedFDeriv ℝ n ((⇑f : (a : E) → F) ∘ g) x) ≤
    (↑n ! : ℝ) * (HPow.hPow (α := ℝ) 2 k' * seminorm_f / (1 + ‖g x‖) ^ k') * ((C + 1) * (1 + ‖x‖) ^ l) ^ n
hxk : ‖x‖ ^ k ≤ (1 + ‖x‖) ^ k
rearrange :
  (1 + ‖x‖) ^ k *
      ((↑n ! : ℝ) * (HPow.hPow (α := ℝ) 2 k' * seminorm_f / (1 + ‖g x‖) ^ k') * ((C + 1) * (1 + ‖x‖) ^ l) ^ n) =
    (1 + ‖x‖) ^ (k + l * n) / (1 + ‖g x‖) ^ k' * ((C + 1) ^ n * (↑n ! : ℝ) * HPow.hPow (α := ℝ) 2 k' * seminorm_f)
hgxk' : 0 < (1 + ‖g x‖) ^ k'
⊢ (1 + ‖x‖) ^ (k + l * n) / (1 + ‖g x‖) ^ k' * ((C + 1) ^ n * (↑n ! : ℝ) * HPow.hPow (α := ℝ) 2 k' * seminorm_f) ≤
    HMul.hMul (β := ℝ) ((1 + Cg) ^ (k + l * n) * ((C + 1) ^ n * (↑n ! : ℝ) * HPow.hPow (α := ℝ) 2 k'))
      (((Finset.Iic (k', n)).sup (schwartzSeminormFamily 𝕜 E F) : (a : 𝓢(E, F)) → ℝ) f : ℝ)
have h₁ : 0 ≤ (C + 1) ^ n * (↑n ! : ℝ) * HPow.hPow (α := ℝ) 2 k' * seminorm_f
Tactic: grw [hg_upper'', ← mul_assoc]
-- 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 : RCLike 𝕜
inst_5 : NormedAddCommGroup D
inst_6 : NormedSpace ℝ D
inst_7 : NormedSpace 𝕜 F
g : D → E
hg : Function.HasTemperateGrowth g
k n l : ℕ
C : ℝ
hC : 0 ≤ C
hgrowth :
  ∀ N ≤ n,
    ∀ (x : D),
      norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_5} ℝ (fun (i : Fin N) ↦ D) E) (iteratedFDeriv ℝ N g x) ≤
        C * (1 + ‖x‖) ^ l
kg : ℕ
Cg : ℝ
hg_upper' : ∀ (x : D), ‖x‖ ≤ Cg * (1 + ‖g x‖) ^ kg
hCg : 1 ≤ 1 + Cg
k' : ℕ := kg * (k + l * n)
f : 𝓢(E, F)
x : D
seminorm_f : ℝ := ((Finset.Iic (k', n)).sup (schwartzSeminormFamily 𝕜 E F) : (a : 𝓢(E, F)) → ℝ) f
hg_upper'' : (1 + ‖x‖) ^ (k + l * n) / (1 + ‖g x‖) ^ k' ≤ (1 + Cg) ^ (k + l * n)
hbound :
  ∀ (i : ℕ) (hi : i ≤ n),
    norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin i) ↦ E) F)
        (iteratedFDeriv ℝ i (⇑f : (a : E) → F) (g x)) ≤
      HPow.hPow (α := ℝ) 2 k' * seminorm_f / (1 + ‖g x‖) ^ k'
hgrowth' :
  ∀ (N : ℕ) (hN₁ : 1 ≤ N) (hN₂ : N ≤ n),
    norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_5} ℝ (fun (i : Fin N) ↦ D) E) (iteratedFDeriv ℝ N g x) ≤
      ((C + 1) * (1 + ‖x‖) ^ l) ^ N
this :
  norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_6} ℝ (fun (i : Fin n) ↦ D) F)
      (iteratedFDeriv ℝ n ((⇑f : (a : E) → F) ∘ g) x) ≤
    (↑n ! : ℝ) * (HPow.hPow (α := ℝ) 2 k' * seminorm_f / (1 + ‖g x‖) ^ k') * ((C + 1) * (1 + ‖x‖) ^ l) ^ n
hxk : ‖x‖ ^ k ≤ (1 + ‖x‖) ^ k
rearrange :
  (1 + ‖x‖) ^ k *
      ((↑n ! : ℝ) * (HPow.hPow (α := ℝ) 2 k' * seminorm_f / (1 + ‖g x‖) ^ k') * ((C + 1) * (1 + ‖x‖) ^ l) ^ n) =
    (1 + ‖x‖) ^ (k + l * n) / (1 + ‖g x‖) ^ k' * ((C + 1) ^ n * (↑n ! : ℝ) * HPow.hPow (α := ℝ) 2 k' * seminorm_f)
hgxk' : 0 < (1 + ‖g x‖) ^ k'
h₁ : 0 ≤ (C + 1) ^ n * (↑n ! : ℝ) * HPow.hPow (α := ℝ) 2 k' * seminorm_f
⊢ (1 + ‖x‖) ^ (k + l * n) / (1 + ‖g x‖) ^ k' * ((C + 1) ^ n * (↑n ! : ℝ) * HPow.hPow (α := ℝ) 2 k' * seminorm_f) ≤
    HMul.hMul (β := ℝ) ((1 + Cg) ^ (k + l * n) * ((C + 1) ^ n * (↑n ! : ℝ) * HPow.hPow (α := ℝ) 2 k'))
      (((Finset.Iic (k', n)).sup (schwartzSeminormFamily 𝕜 E F) : (a : 𝓢(E, F)) → ℝ) f : ℝ)
have right : (1 + Cg) ^ (k + l * n) * ((C + 1) ^ n * (↑n ! : ℝ) * HPow.hPow (α := ℝ) 2 k' * seminorm_f) ≤
  HMul.hMul (β := ℝ) ((1 + Cg) ^ (k + l * n) * ((C + 1) ^ n * (↑n ! : ℝ) * HPow.hPow (α := ℝ) 2 k'))
    (((Finset.Iic (k', n)).sup (schwartzSeminormFamily 𝕜 E F) : (a : 𝓢(E, F)) → ℝ) f : ℝ)
Tactic: grw [hg_upper'', ← mul_assoc]
-- 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 : RCLike 𝕜
inst_5 : NormedAddCommGroup D
inst_6 : NormedSpace ℝ D
inst_7 : NormedSpace 𝕜 F
g : D → E
hg : Function.HasTemperateGrowth g
k n l : ℕ
C : ℝ
hC : 0 ≤ C
hgrowth :
  ∀ N ≤ n,
    ∀ (x : D),
      norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_5} ℝ (fun (i : Fin N) ↦ D) E) (iteratedFDeriv ℝ N g x) ≤
        C * (1 + ‖x‖) ^ l
kg : ℕ
Cg : ℝ
hg_upper' : ∀ (x : D), ‖x‖ ≤ Cg * (1 + ‖g x‖) ^ kg
hCg : 1 ≤ 1 + Cg
k' : ℕ := kg * (k + l * n)
f : 𝓢(E, F)
x : D
seminorm_f : ℝ := ((Finset.Iic (k', n)).sup (schwartzSeminormFamily 𝕜 E F) : (a : 𝓢(E, F)) → ℝ) f
hg_upper'' : (1 + ‖x‖) ^ (k + l * n) / (1 + ‖g x‖) ^ k' ≤ (1 + Cg) ^ (k + l * n)
hbound :
  ∀ (i : ℕ) (hi : i ≤ n),
    norm (E := ContinuousMultilinearMap.{0, 0, u_5, u_6} ℝ (fun (i : Fin i) ↦ E) F)
        (iteratedFDeriv ℝ i (⇑f : (a : E) → F) (g x)) ≤
      HPow.hPow (α := ℝ) 2 k' * seminorm_f / (1 + ‖g x‖) ^ k'
hgrowth' :
  ∀ (N : ℕ) (hN₁ : 1 ≤ N) (hN₂ : N ≤ n),
    norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_5} ℝ (fun (i : Fin N) ↦ D) E) (iteratedFDeriv ℝ N g x) ≤
      ((C + 1) * (1 + ‖x‖) ^ l) ^ N
this :
  norm (E := ContinuousMultilinearMap.{0, 0, u_4, u_6} ℝ (fun (i : Fin n) ↦ D) F)
      (iteratedFDeriv ℝ n ((⇑f : (a : E) → F) ∘ g) x) ≤
    (↑n ! : ℝ) * (HPow.hPow (α := ℝ) 2 k' * seminorm_f / (1 + ‖g x‖) ^ k') * ((C + 1) * (1 + ‖x‖) ^ l) ^ n
hxk : ‖x‖ ^ k ≤ (1 + ‖x‖) ^ k
rearrange :
  (1 + ‖x‖) ^ k *
      ((↑n ! : ℝ) * (HPow.hPow (α := ℝ) 2 k' * seminorm_f / (1 + ‖g x‖) ^ k') * ((C + 1) * (1 + ‖x‖) ^ l) ^ n) =
    (1 + ‖x‖) ^ (k + l * n) / (1 + ‖g x‖) ^ k' * ((C + 1) ^ n * (↑n ! : ℝ) * HPow.hPow (α := ℝ) 2 k' * seminorm_f)
hgxk' : 0 < (1 + ‖g x‖) ^ k'
h₁ : 0 ≤ (C + 1) ^ n * (↑n ! : ℝ) * HPow.hPow (α := ℝ) 2 k' * seminorm_f
right :
  (1 + Cg) ^ (k + l * n) * ((C + 1) ^ n * (↑n ! : ℝ) * HPow.hPow (α := ℝ) 2 k' * seminorm_f) ≤
    HMul.hMul (β := ℝ) ((1 + Cg) ^ (k + l * n) * ((C + 1) ^ n * (↑n ! : ℝ) * HPow.hPow (α := ℝ) 2 k'))
      (((Finset.Iic (k', n)).sup (schwartzSeminormFamily 𝕜 E F) : (a : 𝓢(E, F)) → ℝ) f : ℝ)
⊢ (1 + ‖x‖) ^ (k + l * n) / (1 + ‖g x‖) ^ k' * ((C + 1) ^ n * (↑n ! : ℝ) * HPow.hPow (α := ℝ) 2 k' * seminorm_f) ≤
    HMul.hMul (β := ℝ) ((1 + Cg) ^ (k + l * n) * ((C + 1) ^ n * (↑n ! : ℝ) * HPow.hPow (α := ℝ) 2 k'))
      (((Finset.Iic (k', n)).sup (schwartzSeminormFamily 𝕜 E F) : (a : 𝓢(E, F)) → ℝ) f : ℝ)
have right₁ : (1 + Cg) ^ (k + l * n) * ((C + 1) ^ n * (↑n ! : ℝ) * HPow.hPow (α := ℝ) 2 k') * seminorm_f ≤
  (1 + Cg) ^ (k + l * n) * ((C + 1) ^ n * (↑n ! : ℝ) * HPow.hPow (α := ℝ) 2 k') * seminorm_f
Tactic: grw [hg_upper'', ← mul_assoc]
-- 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 : RCLike 𝕜
inst_5 : NormedAddCommGroup D
inst_6 : NormedSpace ℝ D
inst_7 : NormedSpace 𝕜 F
K : ℝ≥0
g : D → E
hg : Function.HasTemperateGrowth g
h'g : AntilipschitzWith K g
⊢ 𝓢(E, F) →L[𝕜] 𝓢(D, F)
have refine : ∀ (x : D), ‖x‖ ≤ (↑K : ℝ) * max 1 ‖g 0‖ * HPow.hPow (β := ℕ) (1 + ‖g x‖) 1
Tactic: refine compCLM 𝕜 hg ⟨1, K * max 1 ‖g 0‖, fun 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 : RCLike 𝕜
inst_5 : NormedAddCommGroup D
inst_6 : NormedSpace ℝ D
inst_7 : NormedSpace 𝕜 F
K : ℝ≥0
g : D → E
hg : Function.HasTemperateGrowth g
h'g : AntilipschitzWith K g
x : D
⊢ ‖x‖ ≤ (↑K : ℝ) * ‖g x - g 0‖
have rw : dist x 0 ≤ (↑K : ℝ) * dist (g x) (g 0)
Tactic: rw [← dist_zero_right, ← dist_eq_norm]