awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
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)
⊢ 0 < (1 + ‖g x‖) ^ k'

Tactic:
have hgxk' : 0 < (1 + ‖g x‖) ^ k' := by positivity
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
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' ≤ (1 + Cg) ^ (k + l * n)

Tactic:
rw [← div_le_iff₀ hgxk'] at hg_upper''

Premises used: div_le_iff₀
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
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'
hg_upper''₁ : (1 + ‖x‖) ^ (k + l * n) / (1 + ‖g x‖) ^ k' ≤ (1 + Cg) ^ (k + l * n)
⊢ ∀ (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'

Tactic:
rw [← div_le_iff₀ hgxk'] at hg_upper''

Premises used: div_le_iff₀
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
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'
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'
⊢ ∀ (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

Tactic:
rw [← div_le_iff₀ hgxk'] at hg_upper''

Premises used: div_le_iff₀
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
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'
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
⊢ 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

Tactic:
rw [← div_le_iff₀ hgxk'] at hg_upper''

Premises used: div_le_iff₀
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
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'
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
⊢ ‖x‖ ^ k ≤ (1 + ‖x‖) ^ k

Tactic:
rw [← div_le_iff₀ hgxk'] at hg_upper''

Premises used: div_le_iff₀
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
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'
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
⊢ (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:
rw [← div_le_iff₀ hgxk'] at hg_upper''

Premises used: div_le_iff₀
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
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'
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)
⊢ 0 < (1 + ‖g x‖) ^ k'

Tactic:
rw [← div_le_iff₀ hgxk'] at hg_upper''

Premises used: div_le_iff₀
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
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 : ℝ)
right₁ 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
⊢ (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:
grw [hg_upper'', ← mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
𝕜 : Type u_2
D : Type u_4
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 : RCLike 𝕜
inst_5 : NormedAddCommGroup D
inst_6 : NormedSpace ℝ D
inst_7 : NormedSpace 𝕜 F
g : D → E
hg : Function.HasTemperateGrowth g
hg_upper : ∃ (k : ℕ) (C : ℝ), ∀ (x : D), ‖x‖ ≤ C * (1 + ‖g x‖) ^ k
f : 𝓢(E, F)
⊢ Eq (α := (a : D) → F) (⇑((compCLM 𝕜 hg hg_upper : (a : 𝓢(E, F)) → 𝓢(D, F)) f : 𝓢(D, F)) : (a : D) → F)
    ((⇑f : (a : E) → F) ∘ g)

Tactic:
rfl

Premises used: rfl