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 : 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
simp :
  HMul.hMul (β := ℝ) (‖L‖ * (↑(max 1 n) : ℝ))
        (max ((SchwartzMap.seminorm 𝕜 (k + 1) n : (a : 𝓢(E, F)) → ℝ) f)
            ((SchwartzMap.seminorm 𝕜 k (n - 1) : (a : 𝓢(E, F)) → ℝ) f) :
          ℝ) +
      HMul.hMul (β := ℝ) (‖L‖ * (↑(max 1 n) : ℝ))
        (max ((SchwartzMap.seminorm 𝕜 (k + 1) n : (a : 𝓢(E, F)) → ℝ) f)
            ((SchwartzMap.seminorm 𝕜 k (n - 1) : (a : 𝓢(E, F)) → ℝ) f) :
          ℝ) =
    HMul.hMul (β := ℝ) (2 * ‖L‖ * (↑(max 1 n) : ℝ))
      (max ((SchwartzMap.seminorm 𝕜 (k + 1) n : (a : 𝓢(E, F)) → ℝ) f)
          ((SchwartzMap.seminorm 𝕜 k (n - 1) : (a : 𝓢(E, F)) → ℝ) f) :
        ℝ)
⊢ HMul.hMul (β := ℝ) (‖L‖ * (↑(max 1 n) : ℝ))
        (max ((SchwartzMap.seminorm 𝕜 (k + 1) n : (a : 𝓢(E, F)) → ℝ) f)
            ((SchwartzMap.seminorm 𝕜 k (n - 1) : (a : 𝓢(E, F)) → ℝ) f) :
          ℝ) +
      HMul.hMul (β := ℝ) (‖L‖ * (↑(max 1 n) : ℝ))
        (max ((SchwartzMap.seminorm 𝕜 (k + 1) n : (a : 𝓢(E, F)) → ℝ) f)
            ((SchwartzMap.seminorm 𝕜 k (n - 1) : (a : 𝓢(E, F)) → ℝ) f) :
          ℝ) =
    HMul.hMul (β := ℝ) (2 * ‖L‖ * (↑(max 1 n) : ℝ))
      ((Finset.sup {(k + 1, n), (k, n - 1)} (schwartzSeminormFamily 𝕜 E F) : (a : 𝓢(E, F)) → ℝ) f : ℝ)

Tactic:
simp only [Finset.sup_insert, schwartzSeminormFamily_apply, Finset.sup_singleton,
            Seminorm.coe_sup, Pi.sup_apply]

Premises used: Finset.sup_insert, Finset.sup_singleton, Seminorm.coe_sup, Pi.sup_apply, SchwartzMap.schwartzSeminormFamily_apply
-- 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 : 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
⊢ HMul.hMul (β := ℝ) (‖L‖ * (↑(max 1 n) : ℝ))
        (max ((SchwartzMap.seminorm 𝕜 (k + 1) n : (a : 𝓢(E, F)) → ℝ) f)
            ((SchwartzMap.seminorm 𝕜 k (n - 1) : (a : 𝓢(E, F)) → ℝ) f) :
          ℝ) +
      HMul.hMul (β := ℝ) (‖L‖ * (↑(max 1 n) : ℝ))
        (max ((SchwartzMap.seminorm 𝕜 (k + 1) n : (a : 𝓢(E, F)) → ℝ) f)
            ((SchwartzMap.seminorm 𝕜 k (n - 1) : (a : 𝓢(E, F)) → ℝ) f) :
          ℝ) =
    HMul.hMul (β := ℝ) (2 * ‖L‖ * (↑(max 1 n) : ℝ))
      (max ((SchwartzMap.seminorm 𝕜 (k + 1) n : (a : 𝓢(E, F)) → ℝ) f)
          ((SchwartzMap.seminorm 𝕜 k (n - 1) : (a : 𝓢(E, F)) → ℝ) f) :
        ℝ)

Tactic:
ring
-- Module: Mathlib.Analysis.Distribution.SchwartzSpace.Basic
Goal:
𝕜 : Type u_2
E : Type u_5
F : Type u_6
G : Type u_7
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NontriviallyNormedField 𝕜
inst_5 : NormedAlgebra ℝ 𝕜
inst_6 : NormedAddCommGroup G
inst_7 : NormedSpace ℝ G
inst_8 : NormedSpace 𝕜 F
L : ContinuousLinearMap.{0, 0, u_5, u_7} (RingHom.id ℝ) E (G →L[ℝ] ℝ)
f : 𝓢(E, F)
x : E
⊢ Eq (α := G →L[ℝ] F)
    (((((smulRightCLM 𝕜 F L : 𝓢(E, F) →L[𝕜] 𝓢(E, G →L[ℝ] F)) : (a : 𝓢(E, F)) → 𝓢(E, G →L[ℝ] F)) f : 𝓢(E, G →L[ℝ] F)) :
          (a : E) → G →L[ℝ] F)
        x :
      G →L[ℝ] F)
    (smulRight (S := ℝ) ((L : (a : E) → G →L[ℝ] ℝ) x) ((f : (a : E) → F) x) : G →L[ℝ] F)

Tactic:
rfl

Premises used: ContinuousLinearMap.smulRight, rfl
-- 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
hg_upper : ∃ (k : ℕ) (C : ℝ), ∀ (x : D), ‖x‖ ≤ C * (1 + ‖g x‖) ^ k
x x_1 : 𝓢(E, F)
x_2 : D
⊢ (fun (f : 𝓢(E, F)) ↦ ((⇑f : (a : E) → F) ∘ g : D → F)) (x + x_1) x_2 =
    HAdd.hAdd (α := F) ((fun (f : 𝓢(E, F)) ↦ ((⇑f : (a : E) → F) ∘ g : D → F)) x x_2)
      ((fun (f : 𝓢(E, F)) ↦ ((⇑f : (a : E) → F) ∘ g : D → F)) x_1 x_2)

Tactic:
simp
-- 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
hg_upper : ∃ (k : ℕ) (C : ℝ), ∀ (x : D), ‖x‖ ≤ C * (1 + ‖g x‖) ^ k
k n : ℕ
rcases :
  ∀ (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),
    ∃ (s : Finset (ℕ × ℕ)) (C : ℝ),
      0 ≤ C ∧
        ∀ (f : 𝓢(E, F)) (x : D),
          ‖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 (β := ℝ) C ((s.sup (schwartzSeminormFamily 𝕜 E F) : (a : 𝓢(E, F)) → ℝ) f : ℝ)
⊢ ∃ (s : Finset (ℕ × ℕ)) (C : ℝ),
    0 ≤ C ∧
      ∀ (f : 𝓢(E, F)) (x : D),
        ‖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 (β := ℝ) C ((s.sup (schwartzSeminormFamily 𝕜 E F) : (a : 𝓢(E, F)) → ℝ) f : ℝ)

Tactic:
rcases hg.norm_iteratedFDeriv_le_uniform n with ⟨l, C, hC, hgrowth⟩

Premises used: Function.HasTemperateGrowth.norm_iteratedFDeriv_le_uniform
-- 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
hg_upper : ∃ (k : ℕ) (C : ℝ), ∀ (x : D), ‖x‖ ≤ C * (1 + ‖g x‖) ^ k
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
rcases :
  ∀ (kg : ℕ) (Cg : ℝ) (hg_upper' : ∀ (x : D), ‖x‖ ≤ Cg * (1 + ‖g x‖) ^ kg),
    ∃ (s : Finset (ℕ × ℕ)) (C : ℝ),
      0 ≤ C ∧
        ∀ (f : 𝓢(E, F)) (x : D),
          ‖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 (β := ℝ) C ((s.sup (schwartzSeminormFamily 𝕜 E F) : (a : 𝓢(E, F)) → ℝ) f : ℝ)
⊢ ∃ (s : Finset (ℕ × ℕ)) (C : ℝ),
    0 ≤ C ∧
      ∀ (f : 𝓢(E, F)) (x : D),
        ‖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 (β := ℝ) C ((s.sup (schwartzSeminormFamily 𝕜 E F) : (a : 𝓢(E, F)) → ℝ) f : ℝ)

Tactic:
rcases hg_upper with ⟨kg, Cg, hg_upper'⟩
-- 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
⊢ 1 ≤ 1 + Cg

Tactic:
le_add_of_nonneg_right ?_

Premises used: le_add_of_nonneg_right
-- 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
refine : 0 ≤ Cg
⊢ 1 ≤ 1 + Cg

Tactic:
refine le_add_of_nonneg_right ?_

Premises used: le_add_of_nonneg_right
-- 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
⊢ norm.{u_4} (E := D) 0 ≤ Cg * (1 + ‖g 0‖) ^ kg

Tactic:
specialize hg_upper' 0

Premises used: OfNat.ofNat
-- 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' : norm.{u_4} (E := D) 0 ≤ Cg * (1 + ‖g 0‖) ^ kg
⊢ 0 ≤ Cg * (1 + ‖g 0‖) ^ kg

Tactic:
rw [norm_zero] at hg_upper'

Premises used: norm_zero
-- 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' : 0 ≤ Cg * (1 + ‖g 0‖) ^ kg
⊢ 0 < (1 + ‖g 0‖) ^ kg

Tactic:
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' : 0 ≤ Cg * (1 + ‖g 0‖) ^ kg
⊢ 0 ≤ Cg

Tactic:
exact nonneg_of_mul_nonneg_left hg_upper' (by positivity)

Premises used: nonneg_of_mul_nonneg_left
-- 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
⊢ 1 ≤ 1 + Cg

Tactic:
have hCg : 1 ≤ 1 + Cg := by
    refine le_add_of_nonneg_right ?_
    specialize hg_upper' 0
    rw [norm_zero] at hg_upper'
    exact nonneg_of_mul_nonneg_left hg_upper' (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)
⊢ 0 ≤ (1 + Cg) ^ (k + l * n) * ((C + 1) ^ n * (↑n ! : ℝ) * HPow.hPow (α := ℝ) 2 k')

Tactic:
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)
right :
  ∀ (f : 𝓢(E, F)) (x : D),
    ‖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 : ℝ)
⊢ ∃ (s : Finset (ℕ × ℕ)) (C : ℝ),
    0 ≤ C ∧
      ∀ (f : 𝓢(E, F)) (x : D),
        ‖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 (β := ℝ) C ((s.sup (schwartzSeminormFamily 𝕜 E F) : (a : 𝓢(E, F)) → ℝ) f : ℝ)

Tactic:
use Finset.Iic (k', n), (1 + Cg) ^ (k + l * n) * ((C + 1) ^ n * n ! * 2 ^ k'), by positivity

Premises used: HMul.hMul, Prod.mk, Nat.cast, HPow.hPow, HAdd.hAdd, Nat.factorial, Finset.Iic, OfNat.ofNat
-- 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
rw : (1 + ‖x‖) ^ (k + l * n) ≤ ((1 + Cg) * (1 + ‖g x‖) ^ kg) ^ (k + l * n)
⊢ (1 + ‖x‖) ^ (k + l * n) ≤ (1 + Cg) ^ (k + l * n) * (1 + ‖g x‖) ^ k'

Tactic:
rw [pow_mul, ← mul_pow]

Premises used: pow_mul, mul_pow
-- 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
hab : 1 + ‖x‖ ≤ (1 + Cg) * (1 + ‖g x‖) ^ kg
⊢ (1 + ‖x‖) ^ (k + l * n) ≤ ((1 + Cg) * (1 + ‖g x‖) ^ kg) ^ (k + l * n)

Tactic:
gcongr
-- 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
hab : 1 + ‖x‖ ≤ 1 * (1 + ‖g x‖) ^ kg + Cg * (1 + ‖g x‖) ^ kg
⊢ 1 + ‖x‖ ≤ (1 + Cg) * (1 + ‖g x‖) ^ kg

Tactic:
rw [add_mul]

Premises used: add_mul
-- 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
⊢ 1 + ‖x‖ ≤ 1 * (1 + ‖g x‖) ^ kg + Cg * (1 + ‖g x‖) ^ kg

Tactic:
add_le_add ?_ (hg_upper' x)

Premises used: add_le_add
-- 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
hab : 1 ≤ 1 * (1 + ‖g x‖) ^ kg
⊢ 1 + ‖x‖ ≤ 1 * (1 + ‖g x‖) ^ kg + Cg * (1 + ‖g x‖) ^ kg

Tactic:
refine add_le_add ?_ (hg_upper' x)

Premises used: add_le_add
-- 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
hab : HMul.hMul (α := ℝ) 1 1 ≤ 1 * (1 + ‖g x‖) ^ kg
⊢ 1 ≤ 1 * (1 + ‖g x‖) ^ kg

Tactic:
nth_rw 1 [← one_mul (1 : ℝ)]

Premises used: OfNat.ofNat, one_mul
-- 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
hab : 1 ≤ (1 + ‖g x‖) ^ kg
⊢ HMul.hMul (α := ℝ) 1 1 ≤ 1 * (1 + ‖g x‖) ^ kg

Tactic:
gcongr